NYLL
Module

Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
105 declarations indexed from sourceView source ↗

Module documentation

Finsupp card le macaulay Pow card of forall sub single mem

Imports53
  • Batteries.Tactic.Init
  • Mathlib.Algebra.BigOperators.Group.Finset.Basic
  • Mathlib.Algebra.BigOperators.Group.Finset.Defs
  • Mathlib.Algebra.Group.Action.Defs
  • Mathlib.Algebra.Group.Finsupp
  • Mathlib.Algebra.Group.Hom.Defs
  • Mathlib.Algebra.Group.Monoid
  • Mathlib.Algebra.Group.Nat.Defs
  • Mathlib.Algebra.Group.Semigroup
  • Mathlib.Algebra.Notation.Pi.Defs
  • Mathlib.Algebra.Order.BigOperators.Group.Finset
  • Mathlib.Algebra.Order.Group.Nat
  • Mathlib.Algebra.Order.Sub.Defs
  • Mathlib.Algebra.Order.Sub.Unbundled.Basic
  • Mathlib.Basic.Finite.Defs
  • Mathlib.Basic.Logic.Basic
  • Mathlib.Data.Finset.Card
  • Mathlib.Data.Finset.Defs
  • Mathlib.Data.Finset.Disjoint
  • Mathlib.Data.Finset.Empty
  • Mathlib.Data.Finset.Erase
  • Mathlib.Data.Finset.Filter
  • Mathlib.Data.Finset.Image
  • Mathlib.Data.Finset.Insert
  • Mathlib.Data.Finset.Lattice.Basic
  • Mathlib.Data.Finset.Max
  • Mathlib.Data.Finset.Range
  • Mathlib.Data.Finset.Union
  • Mathlib.Data.Finsupp.Defs
  • Mathlib.Data.Finsupp.Order
  • Mathlib.Data.Finsupp.Single
  • Mathlib.Data.Finsupp.Weight
  • Mathlib.Data.Fintype.Basic
  • Mathlib.Data.Fintype.Defs
  • Mathlib.Data.Fintype.EquivFin
  • Mathlib.Data.Nat.Basic
  • Mathlib.Data.Nat.Choose.Basic
  • Mathlib.Data.Nat.Find
  • Mathlib.Data.Nat.Init
  • Mathlib.Data.Set.Defs
  • Mathlib.Data.Set.Finite.Basic
  • Mathlib.Data.Set.Insert
  • Mathlib.Data.Set.Operations
  • Mathlib.Order.Basic
  • Mathlib.Order.Defs.LinearOrder
  • Mathlib.Order.Defs.PartialOrder
  • Mathlib.Order.Disjoint
  • Mathlib.Order.Preorder.Finsupp
  • Mathlib.Tactic.Conv
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Set
  • Mathlib.Tactic.SplitIfs
  • Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow
Imported by2

Declarations

def

top

L80 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top
Documentation

The largest index up to a + d + 1 whose binomial coefficient of order d + 1 is at most a.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
def top (d a : ℕ) : ℕ
def

rem

L83 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.rem
Documentation

The remainder after subtracting the largest admissible binomial coefficient from a.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
def rem (d a : ℕ) : ℕ
theorem

macaulayPow_zero

L85 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_zero
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem macaulayPow_zero (a : ℕ) : Nat.macaulayPow 0 a = 0
theorem

macaulayPow_succ

L87 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_succ
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem macaulayPow_succ (d a : ℕ) :
    Nat.macaulayPow (d + 1) a = (top d a + 1).choose (d + 2) + Nat.macaulayPow d (rem d a)
theorem

sub_le_choose

L91 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sub_le_choose
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem sub_le_choose (d : ℕ) : ∀ k : ℕ, k - d ≤ k.choose (d + 1)
  | 0 => by simp
  | k + 1 => by
      rw [Nat.choose_succ_succ']
      have ih := sub_le_choose d k
      rcases lt_or_ge k d with h | h
      · have : k + 1 - d = 0 := by omega
        omega
      · have hpos : 1 ≤ k.choose d := Nat.choose_pos h
        omega
theorem

choose_top_le

L102 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.choose_top_le
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem choose_top_le (d a : ℕ) : (top d a).choose (d + 1) ≤ a
theorem

lt_choose_of_top_lt

L105 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.lt_choose_of_top_lt
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem lt_choose_of_top_lt (d a : ℕ) {k : ℕ} (hk : top d a < k) : a < k.choose (d + 1)
theorem

lt_choose_top_succ

L112 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.lt_choose_top_succ
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem lt_choose_top_succ (d a : ℕ) : a < (top d a + 1).choose (d + 1)
theorem

top_eq_of

L115 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top_eq_of
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem top_eq_of (d a k : ℕ) (h₁ : k.choose (d + 1) ≤ a) (h₂ : a < (k + 1).choose (d + 1)) :
    top d a = k
theorem

le_top_of_choose_le

L128 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.le_top_of_choose_le
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem le_top_of_choose_le (d a k : ℕ) (h : k.choose (d + 1) ≤ a) : k ≤ top d a
theorem

top_lt_of_lt_choose

L134 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top_lt_of_lt_choose
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem top_lt_of_lt_choose (d a k : ℕ) (h : a < k.choose (d + 1)) : top d a < k
theorem

d_le_top

L141 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.d_le_top
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem d_le_top (d a : ℕ) : d ≤ top d a
theorem

top_zero_right

L143 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top_zero_right
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem top_zero_right (d : ℕ) : top d 0 = d
theorem

d_lt_top_of_pos

L145 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.d_lt_top_of_pos
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem d_lt_top_of_pos (d a : ℕ) (ha : 0 < a) : d < top d a
theorem

top_zero_left

L149 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top_zero_left
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem top_zero_left (a : ℕ) : top 0 a = a
theorem

rem_zero_left

L151 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.rem_zero_left
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem rem_zero_left (a : ℕ) : rem 0 a = 0
theorem

rem_zero_right

L153 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.rem_zero_right
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem rem_zero_right (d : ℕ) : rem d 0 = 0
theorem

rem_add_choose

L155 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.rem_add_choose
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem rem_add_choose (d a : ℕ) : rem d a + (top d a).choose (d + 1) = a
theorem

rem_lt

L158 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.rem_lt
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem rem_lt (d a : ℕ) : rem d a < (top d a).choose d
theorem

macaulayPow_lt_choose

L163 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_lt_choose
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem macaulayPow_lt_choose : ∀ (d m r : ℕ), r < m.choose d →
    Nat.macaulayPow d r < (m + 1).choose (d + 1)
  | 0, m, r, _ => by simp [macaulayPow_zero]
  | d + 1, m, r, h => by
      rw [macaulayPow_succ]
      change _ < (m + 1).choose (d + 2)
      have hK : top d r < m := top_lt_of_lt_choose d r m h
      have hrem : Nat.macaulayPow d (rem d r) < (top d r + 1).choose (d + 1) :=
        macaulayPow_lt_choose d (top d r) (rem d r) (rem_lt d r)
      have h1 : (top d r + 1).choose (d + 2) + (top d r + 1).choose (d + 1) =
          (top d r + 2).choose (d + 2) := by
        rw [Nat.choose_succ_succ' (top d r + 1) (d + 1), add_comm]
      have h2 : (top d r + 2).choose (d + 2) ≤ (m + 1).choose (d + 2) :=
        Nat.choose_le_choose _ (by omega)
      omega
theorem

macaulayPow_mono

L179 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_mono
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem macaulayPow_mono : ∀ (d : ℕ) {a b : ℕ}, a ≤ b → Nat.macaulayPow d a ≤ Nat.macaulayPow d b
  | 0, a, b, _ => by simp [macaulayPow_zero]
  | d + 1, a, b, h => by
      have ht : top d a ≤ top d b := le_top_of_choose_le d b _ ((choose_top_le d a).trans h)
      rcases ht.eq_or_lt with ht | ht
      · rw [macaulayPow_succ, macaulayPow_succ, ht]
        have hr : rem d a ≤ rem d b := by
          have ha := rem_add_choose d a; have hb := rem_add_choose d b; rw [ht] at ha; omega
        have := macaulayPow_mono d hr
        omega
      · have h1 : Nat.macaulayPow (d + 1) a < (top d a + 1 + 1).choose (d + 1 + 1) :=
          macaulayPow_lt_choose (d + 1) (top d a + 1) a (lt_choose_top_succ d a)
        have h2 : (top d a + 1 + 1).choose (d + 1 + 1) ≤ (top d b + 1).choose (d + 1 + 1) :=
          Nat.choose_le_choose _ (by omega)
        have h3 : (top d b + 1).choose (d + 1 + 1) ≤ Nat.macaulayPow (d + 1) b := by
          rw [macaulayPow_succ]; exact Nat.le_add_right _ _
        omega
theorem

macaulayPow_one

L197 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_one
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem macaulayPow_one (a : ℕ) : Nat.macaulayPow 1 a = (a + 1).choose 2
theorem

macaulayPow_zero_right

L200 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_zero_right
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem macaulayPow_zero_right : ∀ d : ℕ, Nat.macaulayPow d 0 = 0
  | 0 => macaulayPow_zero 0
  | d + 1 => by
      rw [macaulayPow_succ, top_zero_right, rem_zero_right, macaulayPow_zero_right d,
        Nat.choose_eq_zero_of_lt (by omega)]
theorem

top_succ_of_le

L206 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.top_succ_of_le
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem top_succ_of_le (d a : ℕ) (ha : 1 ≤ a) (h : a ≤ d + 2) : top (d + 1) a = d + 2
theorem

macaulayPow_eq_self

L212 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_eq_self
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem macaulayPow_eq_self : ∀ (d a : ℕ), a ≤ d + 1 → Nat.macaulayPow (d + 1) a = a
  | d, 0, _ => macaulayPow_zero_right (d + 1)
  | 0, a + 1, h => by
      obtain rfl : a = 0 := by omega
      rw [macaulayPow_one]; rfl
  | d + 1, a + 1, h => by
      have ht : top (d + 1) (a + 1) = d + 2 := top_succ_of_le d (a + 1) (by omega) (by omega)
      have hr : rem (d + 1) (a + 1) = a := by simp [rem, ht]
      rw [macaulayPow_succ, ht, hr, macaulayPow_eq_self d a (by omega)]
      have : (d + 2 + 1).choose (d + 1 + 2) = 1 := by
        rw [show d + 1 + 2 = d + 2 + 1 by omega, Nat.choose_self]
      omega
def

low

L226 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low
Documentation

The recursive lower binomial sum associated with the Macaulay expansion.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
def low : ℕ → ℕ → ℕ
  | 0, _ => 0
  | d + 1, a => (top d a - 1).choose (d + 1) + low d (rem d a)
theorem

low_zero

L230 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low_zero
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem low_zero (a : ℕ) : low 0 a = 0
theorem

low_succ

L232 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low_succ
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem low_succ (d a : ℕ) : low (d + 1) a = (top d a - 1).choose (d + 1) + low d (rem d a)
theorem

low_zero_right

L234 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low_zero_right
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem low_zero_right : ∀ d : ℕ, low d 0 = 0
  | 0 => rfl
  | d + 1 => by
      rw [low_succ, top_zero_right, rem_zero_right, low_zero_right d, Nat.choose_eq_zero_of_lt
        (by omega)]
theorem

low_eq_zero

L240 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low_eq_zero
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem low_eq_zero : ∀ (d a : ℕ), a ≤ d + 1 → low (d + 1) a = 0
  | d, 0, _ => low_zero_right _
  | 0, a + 1, h => by
      obtain rfl : a = 0 := by omega
      rw [low_succ, top_zero_left, low_zero]; rfl
  | d + 1, a + 1, h => by
      have ht : top (d + 1) (a + 1) = d + 2 := top_succ_of_le d (a + 1) (by omega) (by omega)
      have hr : rem (d + 1) (a + 1) = a := by simp [rem, ht]
      rw [low_succ, ht, hr, low_eq_zero d a (by omega), Nat.choose_eq_zero_of_lt (by omega)]
theorem

low_lt_choose

L250 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.low_lt_choose
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem low_lt_choose : ∀ (d m r : ℕ), r < (m + 1).choose (d + 1) → d + 1 ≤ m →
    low (d + 1) r < m.choose (d + 1)
  | 0, m, r, h, hm => by
      rw [low_succ, top_zero_left, low_zero]
      simp only [zero_add, Nat.choose_one_right, add_zero] at h ⊢
      omega
  | d + 1, m, r, h, hm => by
      rw [low_succ]
      change (top (d + 1) r - 1).choose (d + 2) + low (d + 1) (rem (d + 1) r) < m.choose (d + 2)
      have hT : top (d + 1) r ≤ m := Nat.lt_succ_iff.1 (top_lt_of_lt_choose (d + 1) r (m + 1) h)
      rcases Nat.eq_zero_or_pos r with hr | hr
      · subst hr
        rw [top_zero_right, rem_zero_right, low_zero_right, Nat.choose_eq_zero_of_lt (by omega),
          zero_add]
        exact Nat.choose_pos (by omega)
      · have hT' : d + 1 < top (d + 1) r := d_lt_top_of_pos _ _ hr
        have hRlt : rem (d + 1) r < (top (d + 1) r - 1 + 1).choose (d + 1) := by
          rw [Nat.sub_add_cancel (by omega)]; exact rem_lt (d + 1) r
        have ih := low_lt_choose d (top (d + 1) r - 1) (rem (d + 1) r) hRlt (by omega)
        have h1 : (top (d + 1) r - 1).choose (d + 2) + (top (d + 1) r - 1).choose (d + 1) =
            (top (d + 1) r).choose (d + 2) := by
          have := Nat.choose_succ_succ' (top (d + 1) r - 1) (d + 1)
          rw [Nat.sub_add_cancel (show 1 ≤ top (d + 1) r by omega)] at this
          rw [add_comm]; exact this.symm
        have h2 : (top (d + 1) r).choose (d + 2) ≤ m.choose (d + 2) := Nat.choose_le_choose _ hT
        omega
theorem

macaulayPow_low_add

L277 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_low_add
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem macaulayPow_low_add : ∀ (d a : ℕ),
    Nat.macaulayPow (d + 1) (low (d + 1) a) + a = Nat.macaulayPow (d + 1) a
  | 0, a => by
      rw [low_succ, top_zero_left, low_zero, add_zero, macaulayPow_one, macaulayPow_one,
        Nat.choose_one_right]
      rcases Nat.eq_zero_or_pos a with rfl | ha
      · rfl
      · have h2 : (a + 1).choose 2 = a + a.choose 2 := by
          have := Nat.choose_succ_succ' a 1; rw [Nat.choose_one_right] at this; exact this
        rw [Nat.sub_add_cancel ha]; omega
  | d + 1, a => by
      rcases Nat.eq_zero_or_pos a with rfl | ha
      · rw [low_zero_right, add_zero]
      · set T := top (d + 1) a with hT
        set R := rem (d + 1) a with hR
        have hTd : d + 1 < T := d_lt_top_of_pos _ _ ha
        have hRa : R + T.choose (d + 2) = a := rem_add_choose (d + 1) a
        have hRlt : R < T.choose (d + 1) := rem_lt (d + 1) a
        have ih := macaulayPow_low_add d R
        rw [low_succ, macaulayPow_succ (d + 1) a]
        change Nat.macaulayPow (d + 2) ((T - 1).choose (d + 2) + low (d + 1) R) + a =
          (T + 1).choose (d + 3) + Nat.macaulayPow (d + 1) R
        rcases (show T = d + 2 ∨ d + 3 ≤ T by omega) with hT2 | hT3
        · have hC : (d + 2).choose (d + 1) = d + 2 := Nat.choose_succ_self_right (d + 1)
          have hR1 : R ≤ d + 1 := by rw [hT2] at hRlt; omega
          rw [hT2, show d + 2 - 1 = d + 1 from rfl, Nat.choose_succ_self, zero_add, low_eq_zero d R
            hR1,
            macaulayPow_zero_right, macaulayPow_eq_self d R hR1, Nat.choose_self]
          rw [hT2, Nat.choose_self] at hRa
          omega
        · have hlow : low (d + 1) R < (T - 1).choose (d + 1) :=
            low_lt_choose d (T - 1) R (by rw [Nat.sub_add_cancel (by omega)]; exact hRlt) (by omega)
          have hpasc : (T - 1).choose (d + 2) + (T - 1).choose (d + 1) = T.choose (d + 2) := by
            have := Nat.choose_succ_succ' (T - 1) (d + 1)
            rw [Nat.sub_add_cancel (show 1 ≤ T by omega)] at this
            rw [add_comm]; exact this.symm
          have hpasc' : T.choose (d + 3) + T.choose (d + 2) = (T + 1).choose (d + 3) := by
            rw [Nat.choose_succ_succ' T (d + 2), add_comm]
          have htop : top (d + 1) ((T - 1).choose (d + 2) + low (d + 1) R) = T - 1 :=
            top_eq_of (d + 1) _ (T - 1) (Nat.le_add_right _ _)
              (by rw [Nat.sub_add_cancel (show 1 ≤ T by omega)]; change _ < T.choose (d + 2); omega)
          have hrem : rem (d + 1) ((T - 1).choose (d + 2) + low (d + 1) R) = low (d + 1) R := by
            simp [rem, htop]
          rw [macaulayPow_succ, htop, hrem, Nat.sub_add_cancel (show 1 ≤ T by omega)]
          change T.choose (d + 3) + Nat.macaulayPow (d + 1) (low (d + 1) R) + a = _
          omega
theorem

le_choose_add_low

L324 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.le_choose_add_low
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem le_choose_add_low : ∀ (d m r : ℕ), r < (m + 1).choose (d + 1) → r ≤ m.choose d + low (d +
  1) r
  | 0, m, r, _ => by
      rw [low_succ, top_zero_left, low_zero, Nat.choose_zero_right, Nat.choose_one_right]; omega
  | d + 1, m, r, h => by
      rw [low_succ]
      change r ≤ m.choose (d + 1) + ((top (d + 1) r - 1).choose (d + 2) + low (d + 1) (rem (d + 1)
        r))
      have hT : top (d + 1) r ≤ m := Nat.lt_succ_iff.1 (top_lt_of_lt_choose (d + 1) r (m + 1) h)
      have hT1 : 1 ≤ top (d + 1) r := by have := d_le_top (d + 1) r; omega
      have hRa : rem (d + 1) r + (top (d + 1) r).choose (d + 2) = r := rem_add_choose (d + 1) r
      have hRlt : rem (d + 1) r < (top (d + 1) r - 1 + 1).choose (d + 1) := by
        rw [Nat.sub_add_cancel hT1]; exact rem_lt (d + 1) r
      have ih := le_choose_add_low d (top (d + 1) r - 1) (rem (d + 1) r) hRlt
      have h1 : (top (d + 1) r - 1).choose (d + 2) + (top (d + 1) r - 1).choose (d + 1) =
          (top (d + 1) r).choose (d + 2) := by
        have := Nat.choose_succ_succ' (top (d + 1) r - 1) (d + 1)
        rw [Nat.sub_add_cancel hT1] at this
        rw [add_comm]; exact this.symm
      have h2 : (top (d + 1) r - 1).choose (d + 1) + (top (d + 1) r - 1).choose d =
          (top (d + 1) r).choose (d + 1) := by
        have := Nat.choose_succ_succ' (top (d + 1) r - 1) d
        rw [Nat.sub_add_cancel hT1] at this
        rw [add_comm]; exact this.symm
      have h3 : (top (d + 1) r).choose (d + 1) ≤ m.choose (d + 1) := Nat.choose_le_choose _ hT
      omega
theorem

le_add_low

L351 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.le_add_low
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem le_add_low : ∀ (d a s : ℕ), a ≤ Nat.macaulayPow d s → a ≤ s + low (d + 1) a
  | 0, a, s, h => by rw [macaulayPow_zero] at h; omega
  | d + 1, a, s, h => by
      rcases Nat.eq_zero_or_pos a with rfl | ha
      · exact Nat.zero_le _
      set T := top (d + 1) a with hT
      set R := rem (d + 1) a with hR
      have hTd : d + 1 < T := d_lt_top_of_pos _ _ ha
      have hRa : R + T.choose (d + 2) = a := rem_add_choose (d + 1) a
      have hRlt : R < T.choose (d + 1) := rem_lt (d + 1) a
      set T' := top d s with hT'
      have hs : rem d s + T'.choose (d + 1) = s := rem_add_choose d s
      have hlt : Nat.macaulayPow (d + 1) s < (T' + 1 + 1).choose (d + 1 + 1) :=
        macaulayPow_lt_choose (d + 1) (T' + 1) s (lt_choose_top_succ d s)
      have hTT' : T ≤ T' + 1 := by
        have := top_lt_of_lt_choose (d + 1) a (T' + 1 + 1) (h.trans_lt hlt); omega
      rw [low_succ]
      change a ≤ s + ((T - 1).choose (d + 2) + low (d + 1) R)
      have hpasc : (T - 1).choose (d + 2) + (T - 1).choose (d + 1) = T.choose (d + 2) := by
        have := Nat.choose_succ_succ' (T - 1) (d + 1)
        rw [Nat.sub_add_cancel (show 1 ≤ T by omega)] at this
        rw [add_comm]; exact this.symm
      rcases (show T ≤ T' ∨ T = T' + 1 by omega) with hle | heq
      · have h1 : T.choose (d + 1) ≤ T'.choose (d + 1) := Nat.choose_le_choose _ hle
        have h2 : R ≤ (T - 1).choose d + low (d + 1) R :=
          le_choose_add_low d (T - 1) R (by rw [Nat.sub_add_cancel (by omega)]; exact hRlt)
        have h3 : (T - 1).choose (d + 1) + (T - 1).choose d = T.choose (d + 1) := by
          have := Nat.choose_succ_succ' (T - 1) d
          rw [Nat.sub_add_cancel (show 1 ≤ T by omega)] at this
          rw [add_comm]; exact this.symm
        omega
      · have hμ : Nat.macaulayPow (d + 1) s = (T' + 1).choose (d + 2) + Nat.macaulayPow d (rem d s)
          :=
          macaulayPow_succ d s
        rw [← heq] at hμ
        rw [show T' = T - 1 by omega] at hs
        have hR' : R ≤ Nat.macaulayPow d (rem d s) := by omega
        have ih := le_add_low d R (rem d s) hR'
        omega
theorem

macaulayPow_add_le

L391 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.macaulayPow_add_le
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · statement
theorem macaulayPow_add_le (d b s : ℕ) (h : b + s ≤ Nat.macaulayPow d s) :
    Nat.macaulayPow (d + 1) b + (b + s) ≤ Nat.macaulayPow (d + 1) (b + s)
theorem

tower_bound

L398 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.tower_bound
Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
Lean source · full declaration
theorem tower_bound : ∀ (e : ℕ) (b : ℕ → ℕ) (c : ℕ), b (e + 1) ≤ 1 → (1 ≤ b e → b (e + 1) = 1) →
    (∀ k, k + 2 ≤ e + 1 → b k ≤ Nat.macaulayPow (e - k) (b (k + 1))) →
    c ≤ Nat.macaulayPow (e + 1) (b 0) →
    c + ∑ k ∈ Finset.range (e + 2), b k ≤ Nat.macaulayPow (e + 1) (∑ k ∈ Finset.range (e + 2), b k)
  | 0, b, c, h1, h2, _, h4 => by
      have h1' : b 1 ≤ 1 := h1
      have h2' : 1 ≤ b 0 → b 1 = 1 := h2
      have h4' : c ≤ (b 0 + 1).choose 2 := by rw [macaulayPow_one] at h4; exact h4
      change c + ∑ k ∈ Finset.range 2, b k ≤ Nat.macaulayPow 1 (∑ k ∈ Finset.range 2, b k)
      rw [Finset.sum_range_succ, Finset.sum_range_one, macaulayPow_one]
      rcases Nat.eq_zero_or_pos (b 0) with h0 | h0
      · have hc : c = 0 := by rw [h0] at h4'; simpa using h4'
        rw [hc, h0, zero_add, zero_add]
        rcases (show b 1 = 0 ∨ b 1 = 1 by omega) with h | h <;> rw [h] <;> simp
      · have hb1 := h2' h0
        have hp : (b 0 + 1 + 1).choose 2 = (b 0 + 1) + (b 0 + 1).choose 2 := by
          have := Nat.choose_succ_succ' (b 0 + 1) 1; rw [Nat.choose_one_right] at this; exact this
        rw [hb1]; omega
  | e + 1, b, c, h1, h2, h3, h4 => by
      have ih := tower_bound e (fun k => b (k + 1)) (b 0) h1 h2
        (fun k hk =>
          by have := h3 (k + 1) (by omega); rwa [show e + 1 - (k + 1) = e - k by omega] at this)
        (by have := h3 0 (by omega); rwa [Nat.sub_zero] at this)
      rw [Finset.sum_range_succ' b (e + 2)]
      have key := macaulayPow_add_le (e + 1) (b 0) (∑ k ∈ Finset.range (e + 2), b (k + 1)) ih
      rw [add_comm (b 0)] at key
      omega
def

Mon

L429 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.Mon
Documentation

The finite set of exponent vectors of the specified total degree.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
def Mon (e : ℕ) : Finset (Fin (n + 1) →₀ ℕ)
theorem

mem_Mon

L433 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_Mon
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem mem_Mon (e : ℕ) (m : Fin (n + 1) →₀ ℕ) : m ∈ Mon n e ↔ m.degree = e
def

MonW

L438 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.MonW
Documentation

The exponent vectors of the specified degree supported on the first given number of variables.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
def MonW (w e : ℕ) : Finset (Fin (n + 1) →₀ ℕ)
theorem

mem_MonW

L441 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_MonW
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem mem_MonW (w e : ℕ) (m : Fin (n + 1) →₀ ℕ) :
    m ∈ MonW n w e ↔ m.degree = e ∧ ∀ i : Fin (n + 1), w ≤ (i : ℕ) → m i = 0
theorem

MonW_zero_succ

L445 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.MonW_zero_succ
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem MonW_zero_succ (e : ℕ) : MonW n 0 (e + 1) = ∅
theorem

MonW_zero_right

L454 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.MonW_zero_right
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem MonW_zero_right (w : ℕ) : MonW n w 0 = {0}
def

Bplus

L462 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.Bplus
Documentation

The monomials whose every one-variable predecessor belongs to the given set.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
def Bplus (w e : ℕ) (B : Finset (Fin (n + 1) →₀ ℕ)) : Finset (Fin (n + 1) →₀ ℕ)
theorem

mem_Bplus

L465 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_Bplus
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem mem_Bplus (w e : ℕ) (B : Finset (Fin (n + 1) →₀ ℕ)) (u : Fin (n + 1) →₀ ℕ) :
    u ∈ Bplus n w e B ↔
      u ∈ MonW n w (e + 1) ∧ ∀ i : Fin (n + 1), 1 ≤ u i → u - Finsupp.single i 1 ∈ B
theorem

Bplus_subset_MonW

L470 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.Bplus_subset_MonW
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
Lean source · statement
theorem Bplus_subset_MonW (w e : ℕ) (B : Finset (Fin (n + 1) →₀ ℕ)) : Bplus n w e B ⊆ MonW n w (e +
  1)
theorem

degree_sub_single

L476 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.degree_sub_single
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
Lean source · statement
theorem degree_sub_single (u : Fin (n + 1) →₀ ℕ) (i : Fin (n + 1)) (hu : 1 ≤ u i) :
    (u - Finsupp.single i 1).degree + 1 = u.degree
theorem

exists_one_le_of_degree_ne_zero

L481 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.exists_one_le_of_degree_ne_zero
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
Lean source · statement
theorem exists_one_le_of_degree_ne_zero (u : Fin (n + 1) →₀ ℕ) (hu : u.degree ≠ 0) :
    ∃ i, 1 ≤ u i
def

mv

L492 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv
Documentation

Redistribute the exponents of the two selected variables while leaving all others unchanged.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def mv (u : Fin (n + 1) →₀ ℕ) (j : ℕ) : Fin (n + 1) →₀ ℕ
def

key

L497 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key
Documentation

The representative obtained by moving the exponent of the first selected variable to the second.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def key (u : Fin (n + 1) →₀ ℕ) : Fin (n + 1) →₀ ℕ
def

J

L500 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.J
Documentation

The allowed exponents in the fiber of the given monomial set over a fixed representative.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def J (A : Finset (Fin (n + 1) →₀ ℕ)) (m : Fin (n + 1) →₀ ℕ) : Finset ℕ
def

comp

L505 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.comp
Documentation

The compression obtained by replacing each monomial fiber with an initial interval of equal size.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def comp (A : Finset (Fin (n + 1) →₀ ℕ)) : Finset (Fin (n + 1) →₀ ℕ)
def

wt

L509 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.wt
Documentation

The sum of the exponents outside the distinguished variable.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def wt (u : Fin (n + 1) →₀ ℕ) : ℕ
def

pot

L512 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.pot
Documentation

The total weight of a finite set of monomials.

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
def pot (A : Finset (Fin (n + 1) →₀ ℕ)) : ℕ
theorem

mv_apply

L514 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_apply
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · full declaration
theorem mv_apply (u : Fin (n + 1) →₀ ℕ) (j : ℕ) (l : Fin (n + 1)) :
    mv i c u j l = if l = i then j else if l = c then u i + u c - j else u l := rfl
theorem

mv_apply_i

L517 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_apply_i
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
theorem mv_apply_i (u : Fin (n + 1) →₀ ℕ) (j : ℕ) : mv i c u j i = j
theorem

mem_J

L520 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_J
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
theorem mem_J {A : Finset (Fin (n + 1) →₀ ℕ)} {m : Fin (n + 1) →₀ ℕ} {j : ℕ} :
    j ∈ J i c A m ↔ j ≤ m c ∧ mv i c m j ∈ A
theorem

card_J_le

L524 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_J_le
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
theorem card_J_le (A : Finset (Fin (n + 1) →₀ ℕ)) (m : Fin (n + 1) →₀ ℕ) : (J i c A m).card ≤ m c +
  1
theorem

J_mono

L528 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.J_mono
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
theorem J_mono {A A' : Finset (Fin (n + 1) →₀ ℕ)} (h : A ⊆ A') (m : Fin (n + 1) →₀ ℕ) :
    J i c A m ⊆ J i c A' m
theorem

mv_injective

L532 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_injective
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
Lean source · statement
theorem mv_injective (u : Fin (n + 1) →₀ ℕ) : Function.Injective (mv i c u)
theorem

mv_apply_c

L539 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_apply_c
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_apply_c (u : Fin (n + 1) →₀ ℕ) (j : ℕ) : mv i c u j c = u i + u c - j
theorem

mv_apply_ne

L542 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_apply_ne
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem mv_apply_ne {l : Fin (n + 1)} (hli : l ≠ i) (hlc : l ≠ c) (u : Fin (n + 1) →₀ ℕ) (j : ℕ) :
    mv i c u j l = u l
theorem

key_apply_i

L546 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_apply_i
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem key_apply_i (u : Fin (n + 1) →₀ ℕ) : key i c u i = 0
theorem

key_apply_c

L548 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_apply_c
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem key_apply_c (u : Fin (n + 1) →₀ ℕ) : key i c u c = u i + u c
theorem

key_apply_ne

L551 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_apply_ne
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem key_apply_ne {l : Fin (n + 1)} (hli : l ≠ i) (hlc : l ≠ c) (u : Fin (n + 1) →₀ ℕ) :
    key i c u l = u l
theorem

ext3

L554 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.ext3
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem ext3 {f g : Fin (n + 1) →₀ ℕ} (hi : f i = g i) (hc : f c = g c)
    (h : ∀ l, l ≠ i → l ≠ c → f l = g l) : f = g
theorem

mv_key

L563 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_key
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_key (u : Fin (n + 1) →₀ ℕ) (j : ℕ) : mv i c (key i c u) j = mv i c u j
theorem

key_mv

L568 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_mv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem key_mv (u : Fin (n + 1) →₀ ℕ) (j : ℕ) (hj : j ≤ u i + u c) : key i c (mv i c u j) = key i c
  u
theorem

key_key

L574 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_key
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem key_key (u : Fin (n + 1) →₀ ℕ) : key i c (key i c u) = key i c u
theorem

mv_self

L577 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_self
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_self (u : Fin (n + 1) →₀ ℕ) : mv i c u (u i) = u
theorem

sub_add_eq_mv

L581 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sub_add_eq_mv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem sub_add_eq_mv (u : Fin (n + 1) →₀ ℕ) (hu : 1 ≤ u i) :
    u - Finsupp.single i 1 + Finsupp.single c 1 = mv i c (key i c u) (u i - 1)
theorem

mv_sub_single_i

L590 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_sub_single_i
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_sub_single_i (u : Fin (n + 1) →₀ ℕ) (x : ℕ) (hx : 1 ≤ x) (hu : 1 ≤ u i) :
    mv i c u x - Finsupp.single i 1 = mv i c (u - Finsupp.single i 1) (x - 1)
theorem

mv_sub_single_i'

L601 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_sub_single_i'
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_sub_single_i' (u : Fin (n + 1) →₀ ℕ) (x : ℕ) (hx : 1 ≤ x) (hu : 1 ≤ u c) :
    mv i c u x - Finsupp.single i 1 = mv i c (u - Finsupp.single c 1) (x - 1)
theorem

mv_sub_single_c

L614 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_sub_single_c
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_sub_single_c (u : Fin (n + 1) →₀ ℕ) (x : ℕ) (hu : 1 ≤ u c) :
    mv i c u x - Finsupp.single c 1 = mv i c (u - Finsupp.single c 1) x
theorem

mv_sub_single_ne

L621 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_sub_single_ne
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_sub_single_ne {l : Fin (n + 1)} (hli : l ≠ i) (hlc : l ≠ c) (u : Fin (n + 1) →₀ ℕ) (x :
  ℕ) :
    mv i c u x - Finsupp.single l 1 = mv i c (u - Finsupp.single l 1) x
theorem

mem_comp_iff

L629 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_comp_iff
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mem_comp_iff (A : Finset (Fin (n + 1) →₀ ℕ)) (u : Fin (n + 1) →₀ ℕ) :
    u ∈ comp i c A ↔ u i < (J i c A (key i c u)).card
theorem

comp_mono

L646 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.comp_mono
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem comp_mono {A A' : Finset (Fin (n + 1) →₀ ℕ)} (h : A ⊆ A') : comp i c A ⊆ comp i c A'
theorem

comp_step_mem

L651 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.comp_step_mem
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem comp_step_mem {A : Finset (Fin (n + 1) →₀ ℕ)} {u : Fin (n + 1) →₀ ℕ} (hu : u ∈ comp i c A)
    (h1 : 1 ≤ u i) : u - Finsupp.single i 1 + Finsupp.single c 1 ∈ comp i c A
theorem

sum_biUnion_mv

L657 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sum_biUnion_mv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · full declaration
theorem sum_biUnion_mv (K : Finset (Fin (n + 1) →₀ ℕ)) (hK : ∀ m ∈ K, key i c m = m)
    (S : (Fin (n + 1) →₀ ℕ) → Finset ℕ) (hS : ∀ m ∈ K, ∀ j ∈ S m, j ≤ m i + m c)
    (f : (Fin (n + 1) →₀ ℕ) → ℕ) :
    ∑ u ∈ K.biUnion (fun m => (S m).image (mv i c m)), f u = ∑ m ∈ K, ∑ j ∈ S m, f (mv i c m j) :=
      by
  rw [Finset.sum_biUnion]
  · exact Finset.sum_congr rfl fun m _ => Finset.sum_image fun j _ j' _ h => mv_injective i c m h
  · intro m hm m' hm' hne
    change Disjoint _ _
    rw [Finset.disjoint_left]
    intro u hu hu'
    rw [Finset.mem_image] at hu hu'
    obtain ⟨j, hj, rfl⟩ := hu
    obtain ⟨j', hj', h⟩ := hu'
    apply hne
    have h1 := key_mv hic m j (hS m hm j hj)
    have h2 := key_mv hic m' j' (hS m' hm' j' hj')
    rw [h, h1, hK m hm] at h2
    rw [hK m' hm'] at h2
    exact h2
theorem

key_of_mem_image

L678 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.key_of_mem_image
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem key_of_mem_image {A : Finset (Fin (n + 1) →₀ ℕ)} {m : Fin (n + 1) →₀ ℕ}
    (hm : m ∈ A.image (key i c)) : key i c m = m
theorem

sum_eq_sum_key

L682 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sum_eq_sum_key
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem sum_eq_sum_key (A : Finset (Fin (n + 1) →₀ ℕ)) (f : (Fin (n + 1) →₀ ℕ) → ℕ) :
    ∑ u ∈ A, f u = ∑ m ∈ A.image (key i c), ∑ j ∈ J i c A m, f (mv i c m j)
theorem

sum_comp

L697 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sum_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem sum_comp (A : Finset (Fin (n + 1) →₀ ℕ)) (f : (Fin (n + 1) →₀ ℕ) → ℕ) :
    ∑ u ∈ comp i c A, f u = ∑ m ∈ A.image (key i c), ∑ j ∈ Finset.range (J i c A m).card, f (mv i c
      m j)
theorem

card_comp

L704 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem card_comp (A : Finset (Fin (n + 1) →₀ ℕ)) : (comp i c A).card = A.card
theorem

degree_mv

L708 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.degree_mv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem degree_mv (u : Fin (n + 1) →₀ ℕ) (j : ℕ) (hj : j ≤ u i + u c) : (mv i c u j).degree =
  u.degree
theorem

mv_mem_MonW

L724 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mv_mem_MonW
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem mv_mem_MonW {u : Fin (n + 1) →₀ ℕ} {W e : ℕ} (hu : u ∈ MonW n W e) (hiW : (i : ℕ) < W)
    (hcW : (c : ℕ) < W) {j : ℕ} (hj : j ≤ u i + u c) : mv i c u j ∈ MonW n W e
theorem

comp_subset_MonW

L732 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.comp_subset_MonW
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem comp_subset_MonW {A : Finset (Fin (n + 1) →₀ ℕ)} {W e : ℕ} (hA : A ⊆ MonW n W e)
    (hiW : (i : ℕ) < W) (hcW : (c : ℕ) < W) : comp i c A ⊆ MonW n W e
theorem

sum_range_card_le

L742 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sum_range_card_le
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem sum_range_card_le (S : Finset ℕ) :
    ∑ j ∈ Finset.range S.card, j ≤ ∑ j ∈ S, j ∧
      (∑ j ∈ Finset.range S.card, j = ∑ j ∈ S, j → S = Finset.range S.card)
theorem

min_card_le

L759 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.min_card_le
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
omit hic in
Lean source · statement
theorem min_card_le (S S' : Finset ℕ) (t : ℕ) (h1 : ∀ x ∈ S, x < t → x ∈ S')
    (h2 : ∀ x ∈ S, 1 ≤ x → x - 1 ∈ S') : min S.card t ≤ S'.card
theorem

sub_single_mem_comp

L786 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sub_single_mem_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem sub_single_mem_comp {A D : Finset (Fin (n + 1) →₀ ℕ)}
    (hAD : ∀ a ∈ A, ∀ l : Fin (n + 1), 1 ≤ a l → a - Finsupp.single l 1 ∈ D)
    {u : Fin (n + 1) →₀ ℕ} (hu : u ∈ comp i c A) (l : Fin (n + 1)) (hl : 1 ≤ u l) :
    u - Finsupp.single l 1 ∈ comp i c D
theorem

card_Bplus_le_comp

L843 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_Bplus_le_comp
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem card_Bplus_le_comp (W e : ℕ) (X : Finset (Fin (n + 1) →₀ ℕ)) (hiW : (i : ℕ) < W)
    (hcW : (c : ℕ) < W) : (Bplus n W e X).card ≤ (Bplus n W e (comp i c X)).card
theorem

wt_mv

L851 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.wt_mv
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem wt_mv (m : Fin (n + 1) →₀ ℕ) (j : ℕ) (hm : m i = 0) : wt c (mv i c m j) = wt c m + j
theorem

pot_comp_lt

L862 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.pot_comp_lt
Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
section Compression
variable (i c : Fin (n + 1))
variable {i c} (hic : i ≠ c)
include hic
Lean source · statement
theorem pot_comp_lt (A : Finset (Fin (n + 1) →₀ ℕ)) {u : Fin (n + 1) →₀ ℕ} (hu : u ∈ A) (h1 : 1 ≤ u
  i)
    (hnot : u - Finsupp.single i 1 + Finsupp.single c 1 ∉ A) : pot c (comp i c A) < pot c A
theorem

exists_stable

L896 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.exists_stable
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
Lean source · statement
theorem exists_stable (w : ℕ) (c : Fin (n + 1)) (hcw : (c : ℕ) = w) (e : ℕ) :
    ∀ (P : ℕ) (X : Finset (Fin (n + 1) →₀ ℕ)), pot c X = P → X ⊆ MonW n (w + 1) e →
    ∃ Y : Finset (Fin (n + 1) →₀ ℕ), Y ⊆ MonW n (w + 1) e ∧ Y.card = X.card ∧
      (Bplus n (w + 1) e X).card ≤ (Bplus n (w + 1) e Y).card ∧
      ∀ u ∈ Y, ∀ l : Fin (n + 1), (l : ℕ) < w → 1 ≤ u l →
        u - Finsupp.single l 1 + Finsupp.single c 1 ∈ Y
def

T

L922 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.T
Documentation

The monomials that enter the given set after adding the specified exponent at one variable.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
Lean source · statement
def T (w : ℕ) (c : Fin (n + 1)) (X : Finset (Fin (n + 1) →₀ ℕ)) (e k : ℕ) :
    Finset (Fin (n + 1) →₀ ℕ)
theorem

T_subset

L926 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.T_subset
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
Lean source · statement
theorem T_subset (w : ℕ) (c : Fin (n + 1)) (X : Finset (Fin (n + 1) →₀ ℕ)) (e k : ℕ) :
    T n w c X e k ⊆ MonW n w (e - k)
theorem

mem_T_iff

L937 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.mem_T_iff
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · statement
theorem mem_T_iff {k : ℕ} (hk : k ≤ e) (v : Fin (n + 1) →₀ ℕ) :
    v ∈ T n w c X e k ↔ v c = 0 ∧ v + Finsupp.single c k ∈ X
theorem

card_T

L953 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_T
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · full declaration
theorem card_T {k : ℕ} (hk : k ≤ e) : (T n w c X e k).card = (X.filter fun u => u c = k).card := by
  refine Finset.card_bij' (fun v _ => v + Finsupp.single c k) (fun u _ => u - Finsupp.single c k)
    ?_ ?_ ?_ ?_
  · intro v hv
    rw [mem_T_iff hcw hX hk] at hv
    rw [Finset.mem_filter]
    exact ⟨hv.2, by rw [Finsupp.add_apply, Finsupp.single_eq_same, hv.1, zero_add]⟩
  · intro u hu
    rw [Finset.mem_filter] at hu
    rw [mem_T_iff hcw hX hk]
    refine ⟨by rw [Finsupp.tsub_apply, Finsupp.single_eq_same, hu.2, Nat.sub_self], ?_⟩
    rw [tsub_add_cancel_of_le (Finsupp.single_le_iff.2 (by rw [hu.2]))]
    exact hu.1
  · intro v _; exact add_tsub_cancel_right _ _
  · intro u hu
    rw [Finset.mem_filter] at hu
    exact tsub_add_cancel_of_le (Finsupp.single_le_iff.2 (by rw [hu.2]))
theorem

sum_card_T

L971 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sum_card_T
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · statement
theorem sum_card_T : ∑ k ∈ Finset.range (e + 1), (T n w c X e k).card = X.card
theorem

card_Bplus_succ_le

L979 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_Bplus_succ_le
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · statement
theorem card_Bplus_succ_le : (Bplus n (w + 1) e X).card ≤ (Bplus n w e (T n w c X e 0)).card +
  X.card
theorem

sub_add_single_comm

L1004 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.sub_add_single_comm
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
omit hcw hX in
Lean source · statement
theorem sub_add_single_comm (v : Fin (n + 1) →₀ ℕ) {l c' : Fin (n + 1)} (hlc : l ≠ c') (k : ℕ) :
    v - Finsupp.single l 1 + Finsupp.single c' (k + 1) =
      v + Finsupp.single c' k - Finsupp.single l 1 + Finsupp.single c' 1
theorem

T_subset_Bplus

L1015 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.T_subset_Bplus
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · statement
theorem T_subset_Bplus
    (hstab : ∀ u ∈ X, ∀ l : Fin (n + 1), (l : ℕ) < w → 1 ≤ u l →
      u - Finsupp.single l 1 + Finsupp.single c 1 ∈ X)
    (k : ℕ) (hk : k + 1 ≤ e) : T n w c X e k ⊆ Bplus n w (e - (k + 1)) (T n w c X e (k + 1))
theorem

card_T_last_le

L1035 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_T_last_le
Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
omit hcw hX in
Lean source · statement
theorem card_T_last_le : (T n w c X e e).card ≤ 1
theorem

card_T_last_eq

L1039 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.card_T_last_eq
Source context 11 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
section Tower
variable {w : ℕ} {c : Fin (n + 1)} (hcw : (c : ℕ) = w) {X : Finset (Fin (n + 1) →₀ ℕ)} {e : ℕ}
  (hX : X ⊆ MonW n (w + 1) e)
include hcw hX
Lean source · statement
theorem card_T_last_eq
    (hstab : ∀ u ∈ X, ∀ l : Fin (n + 1), (l : ℕ) < w → 1 ≤ u l →
      u - Finsupp.single l 1 + Finsupp.single c 1 ∈ X)
    (he : 1 ≤ e) (hne : 1 ≤ (T n w c X e (e - 1)).card) : (T n w c X e e).card = 1
theorem

stable_bound

L1053 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.stable_bound
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
Lean source · statement
theorem stable_bound (w : ℕ) (c : Fin (n + 1)) (hcw : (c : ℕ) = w)
    (ih : ∀ e, 1 ≤ e → ∀ Z : Finset (Fin (n + 1) →₀ ℕ), Z ⊆ MonW n w e →
      (Bplus n w e Z).card ≤ Nat.macaulayPow e Z.card)
    {e : ℕ} (he : 1 ≤ e) {X : Finset (Fin (n + 1) →₀ ℕ)} (hX : X ⊆ MonW n (w + 1) e)
    (hstab : ∀ u ∈ X, ∀ l : Fin (n + 1), (l : ℕ) < w → 1 ≤ u l →
      u - Finsupp.single l 1 + Finsupp.single c 1 ∈ X) :
    (Bplus n (w + 1) e X).card ≤ Nat.macaulayPow e X.card
theorem

main

L1077 ↗
AlgebraicCurves.Foundations.Algebra.Proofs.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem.MacaulayCL.main
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
namespace MacaulayCL
variable (n : ℕ)
variable {n}
variable (n)
variable {n}
Lean source · full declaration
theorem main : ∀ w : ℕ, w ≤ n + 1 → ∀ e : ℕ, 1 ≤ e → ∀ X : Finset (Fin (n + 1) →₀ ℕ),
    X ⊆ MonW n w e → (Bplus n w e X).card ≤ Nat.macaulayPow e X.card
  | 0, _, e, he, X, hX => by
      obtain ⟨e, rfl⟩ : ∃ e', e = e' + 1 := ⟨e - 1, by omega⟩
      have h1 : X = ∅ := Finset.subset_empty.1 (by rw [MonW_zero_succ] at hX; exact hX)
      subst h1
      have h2 : Bplus n 0 (e + 1) ∅ = ∅ := Finset.subset_empty.1 (by
        have := Bplus_subset_MonW n 0 (e + 1) ∅; rw [MonW_zero_succ] at this; exact this)
      rw [h2, Finset.card_empty]; exact Nat.zero_le _
  | w + 1, hw, e, he, X, hX => by
      obtain ⟨Y, hY, hYc, hYB, hYs⟩ := exists_stable w ⟨w, by omega⟩ rfl e _ X rfl hX
      refine hYB.trans ?_
      rw [← hYc]
      exact stable_bound w ⟨w, by omega⟩ rfl (main w (by omega)) he hY hYs
theorem

card_le_macaulayPow_card_of_forall_sub_single_mem

L1100 ↗
Finsupp.card_le_macaulayPow_card_of_forall_sub_single_mem
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
attribute [local simp] MacaulayCL.mem_Mon
attribute [local simp] MacaulayCL.mv_apply_i
attribute [local simp] MacaulayCL.key_apply_i
open MacaulayCL in
Lean source · statement
theorem _root_.Finsupp.card_le_macaulayPow_card_of_forall_sub_single_mem
    (n d : ℕ) (hd : 1 ≤ d) (B : Finset (Fin (n + 1) →₀ ℕ)) (hB : ∀ m ∈ B, m.degree = d)
    (C : Finset (Fin (n + 1) →₀ ℕ)) (hC : ∀ u ∈ C, u.degree = d + 1)
    (hCB : ∀ u ∈ C, ∀ i : Fin (n + 1), 1 ≤ u i → u - Finsupp.single i 1 ∈ B) :
    C.card ≤ Nat.macaulayPow d B.card

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.