NYLL
Module

MvPolynomial_finrank_piece_succ_le_macaulayPow.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_succ_le_macaulayPow
33 declarations indexed from sourceView source ↗

Module documentation

Mv Polynomial finrank piece succ le macaulay Pow

Imports68
  • Batteries.Tactic.Init
  • Mathlib.Algebra.BigOperators.Group.Finset.Basic
  • Mathlib.Algebra.BigOperators.Group.Finset.Defs
  • Mathlib.Algebra.Field.Defs
  • Mathlib.Algebra.Group.Action.Defs
  • Mathlib.Algebra.Group.Equiv.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.GroupWithZero.Action.Defs
  • Mathlib.Algebra.GroupWithZero.Basic
  • Mathlib.Algebra.Module.LinearMap.Defs
  • Mathlib.Algebra.Module.Submodule.Defs
  • Mathlib.Algebra.Module.Submodule.Ker
  • Mathlib.Algebra.Module.Submodule.Lattice
  • Mathlib.Algebra.Module.Submodule.LinearMap
  • Mathlib.Algebra.Module.Submodule.Map
  • Mathlib.Algebra.Module.Submodule.RestrictScalars
  • Mathlib.Algebra.MonoidAlgebra.Defs
  • Mathlib.Algebra.MvPolynomial.Basic
  • Mathlib.Algebra.Notation.Pi.Defs
  • Mathlib.Basic.Finite.Defs
  • Mathlib.Data.Finset.Card
  • Mathlib.Data.Finset.Defs
  • Mathlib.Data.Finset.Filter
  • Mathlib.Data.Finset.Max
  • Mathlib.Data.Finset.SDiff
  • Mathlib.Data.Finsupp.Defs
  • Mathlib.Data.Finsupp.MonomialOrder
  • Mathlib.Data.Finsupp.Order
  • Mathlib.Data.Finsupp.Single
  • Mathlib.Data.Finsupp.Weight
  • Mathlib.Data.Fintype.Basic
  • Mathlib.Data.Fintype.Card
  • Mathlib.Data.Fintype.Defs
  • Mathlib.Data.Fintype.EquivFin
  • Mathlib.Data.Fintype.Sets
  • Mathlib.Data.Nat.Basic
  • Mathlib.Data.Nat.Choose.Basic
  • Mathlib.Data.Nat.Find
  • Mathlib.Data.Set.Card
  • Mathlib.Data.Set.Finite.Basic
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.Finite
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.Dimension.RankNullity
  • Mathlib.LinearAlgebra.Dimension.StrongRankCondition
  • Mathlib.LinearAlgebra.FiniteDimensional.Defs
  • Mathlib.LinearAlgebra.FreeModule.Finite.Basic
  • Mathlib.LinearAlgebra.LinearIndependent.Defs
  • Mathlib.Order.Basic
  • Mathlib.Order.Defs.LinearOrder
  • Mathlib.Order.Defs.PartialOrder
  • Mathlib.Order.Fin.Basic
  • Mathlib.Order.RelClasses
  • Mathlib.RingTheory.Finiteness.Defs
  • Mathlib.RingTheory.Ideal.Defs
  • Mathlib.RingTheory.MvPolynomial.Basic
  • Mathlib.RingTheory.MvPolynomial.Homogeneous
  • Mathlib.RingTheory.MvPolynomial.MonomialOrder
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Set
  • Nyll.AlgebraicCurves.Hilbert.Functor.Basic
  • Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow
  • Nyll.AlgebraicCurves.Foundations.Algebra.Finsupp_card_le_macaulayPow_card_of_forall_sub_single_mem
Imported by9

Declarations

def

top

L95 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.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.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
Lean source · statement
def top (d a : ℕ) : ℕ
def

rem

L97 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.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.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
Lean source · statement
def rem (d a : ℕ) : ℕ
theorem

macaulayPow_zero

L99 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.macaulayPow_zero
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
Lean source · statement
theorem macaulayPow_zero (a : ℕ) : Nat.macaulayPow 0 a = 0
theorem

macaulayPow_succ

L101 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.macaulayPow_succ
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
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

L105 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.sub_le_choose
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
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

L116 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.choose_top_le
Source context 4 commands

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

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

lt_choose_of_top_lt

L119 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.lt_choose_of_top_lt
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
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

L126 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.lt_choose_top_succ
Source context 4 commands

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

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

top_lt_of_lt_choose

L129 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.top_lt_of_lt_choose
Source context 4 commands

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

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

le_top_of_choose_le

L136 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.le_top_of_choose_le
Source context 4 commands

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

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

rem_add_choose

L142 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.rem_add_choose
Source context 4 commands

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

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

rem_lt

L145 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.rem_lt
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
Lean source · statement
theorem rem_lt (d a : ℕ) : rem d a < (top d a).choose d
theorem

macaulayPow_lt_choose

L150 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.macaulayPow_lt_choose
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
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

L166 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.macaulayPow_mono
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
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
def

Mon

L190 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.Mon
Documentation

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

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
Lean source · statement
def Mon (e : ℕ) : Finset (Fin (n + 1) →₀ ℕ)
theorem

mem_Mon

L194 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.mem_Mon
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
Lean source · statement
theorem mem_Mon (e : ℕ) (m : Fin (n + 1) →₀ ℕ) : m ∈ Mon n e ↔ m.degree = e
def

lex

L197 ↗
MacaulayRed.lex
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
Lean source · statement
def _root_.MacaulayRed.lex : MonomialOrder (Fin (n + 1))
theorem

degree_eq_of_mem_support

L202 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.degree_eq_of_mem_support
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem degree_eq_of_mem_support {e : ℕ} {p : MvPolynomial (Fin (n + 1)) K}
    (hp : p.IsHomogeneous e) {m : Fin (n + 1) →₀ ℕ} (hm : m ∈ p.support) : m.degree = e
def

LM

L209 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.LM
Documentation

The leading exponent vectors of nonzero homogeneous elements of the ideal.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
def LM (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) : Finset (Fin (n + 1) →₀ ℕ)
theorem

mem_LM

L215 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.mem_LM
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem mem_LM (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) (a : Fin (n + 1) →₀ ℕ) :
    a ∈ LM n K J e ↔ a.degree = e ∧ ∃ f : MvPolynomial (Fin (n + 1)) K,
      f ∈ J ∧ f.IsHomogeneous e ∧ f ≠ 0 ∧ (lex n).degree f = a
theorem

LM_subset

L221 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.LM_subset
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem LM_subset (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) : LM n K J e ⊆ Mon n e
theorem

degree_mem_LM

L225 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.degree_mem_LM
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem degree_mem_LM (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ)
    {f : MvPolynomial (Fin (n + 1)) K} (hfJ : f ∈ J) (hf : f.IsHomogeneous e) (hf0 : f ≠ 0) :
    (lex n).degree f ∈ LM n K J e
theorem

add_single_mem_LM

L231 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.add_single_mem_LM
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem add_single_mem_LM (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (d : ℕ)
    {a : Fin (n + 1) →₀ ℕ} (ha : a ∈ LM n K J d) (i : Fin (n + 1)) :
    a + Finsupp.single i 1 ∈ LM n K J (d + 1)
def

W

L245 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.W
Documentation

The part of the ideal lying in the specified homogeneous component.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
def W (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) :
    Submodule K ↥(homogeneousSubmodule (Fin (n + 1)) K e)
theorem

mem_W

L249 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.mem_W
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem mem_W (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ)
    (p : ↥(homogeneousSubmodule (Fin (n + 1)) K e)) : p ∈ W n K J e ↔ (p : MvPolynomial _ K) ∈ J
instance

finite_homogeneousSubmodule

L253 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.finite_homogeneousSubmodule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
instance finite_homogeneousSubmodule (e : ℕ) :
    Module.Finite K ↥(homogeneousSubmodule (Fin (n + 1)) K e)
theorem

finrank_homogeneousSubmodule

L261 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.finrank_homogeneousSubmodule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem finrank_homogeneousSubmodule (e : ℕ) :
    Module.finrank K ↥(homogeneousSubmodule (Fin (n + 1)) K e) = (Mon n e).card
theorem

finrank_W_le

L271 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.finrank_W_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem finrank_W_le (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) :
    Module.finrank K ↥(W n K J e) ≤ (LM n K J e).card
theorem

linearIndependent_of_degree_eq

L296 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.linearIndependent_of_degree_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem linearIndependent_of_degree_eq (s : Finset (Fin (n + 1) →₀ ℕ))
    (g : ↥s → MvPolynomial (Fin (n + 1)) K) (hg0 : ∀ a, g a ≠ 0)
    (hg : ∀ a, (lex n).degree (g a) = a.1) : LinearIndependent K g
theorem

card_LM_le

L325 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.card_LM_le
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem card_LM_le (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) :
    (LM n K J e).card ≤ Module.finrank K ↥(W n K J e)
theorem

finrank_W

L340 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.finrank_W
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem finrank_W (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) :
    Module.finrank K ↥(W n K J e) = (LM n K J e).card
theorem

finrank_piece_add

L344 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed.finrank_piece_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
namespace MacaulayRed
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped MonomialOrder
variable (n : ℕ)
variable (K : Type) [Field K]
Lean source · statement
theorem finrank_piece_add (J : Ideal (MvPolynomial (Fin (n + 1)) K)) (e : ℕ) :
    Module.finrank K (piece J e) + (LM n K J e).card = (Mon n e).card
theorem

finrank_piece_succ_le_macaulayPow

L358 ↗
MvPolynomial.finrank_piece_succ_le_macaulayPow
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_succ_le_macaulayPow
attribute [local simp] MacaulayRed.mem_Mon
attribute [local instance] MacaulayRed.finite_homogeneousSubmodule
open _root_.AlgebraicCurves.Foundations.Polynomial.Proofs in
open MvPolynomial_finrank_piece_succ_le_macaulayPow.MacaulayRed in
open MvPolynomial AlgebraicGeometry.HilbertFunctor in
Lean source · statement
theorem _root_.MvPolynomial.finrank_piece_succ_le_macaulayPow
    (n d : ℕ) (hd : 1 ≤ d) (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K))
    (_hJ : ∀ p ∈ J, ∀ i : ℕ, homogeneousComponent i p ∈ J) :
    Module.finrank K (piece J (d + 1)) ≤ Nat.macaulayPow d (Module.finrank K (piece J d))

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