NYLL
Module

MvPolynomial_finrank_piece_eq_of_maximal_growth.lean

Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_eq_of_maximal_growth
34 declarations indexed from sourceView source ↗

Module documentation

Mv Polynomial finrank piece eq of maximal growth

Imports30
Imported by2

Declarations

def

Ik

L67 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.Ik
Documentation

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

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
def Ik (I : Ideal (MvPolynomial (Fin (n + 1)) L)) (d : ℕ) :
    Submodule L ↥(homogeneousSubmodule (Fin (n + 1)) L d)
theorem

mem_Ik

L71 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.mem_Ik
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem mem_Ik {I : Ideal (MvPolynomial (Fin (n + 1)) L)} {d : ℕ}
    (x : ↥(homogeneousSubmodule (Fin (n + 1)) L d)) :
    x ∈ Ik I d ↔ (x : MvPolynomial (Fin (n + 1)) L) ∈ I
theorem

Ik_mono

L75 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.Ik_mono
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem Ik_mono {I I' : Ideal (MvPolynomial (Fin (n + 1)) L)} (h : I ≤ I') (d : ℕ) : Ik I d ≤ Ik I'
  d
theorem

piece_eq

L79 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.piece_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem piece_eq (I : Ideal (MvPolynomial (Fin (n + 1)) L)) (d : ℕ) :
    piece I d = (↥(homogeneousSubmodule (Fin (n + 1)) L d) ⧸ Ik I d)
instance

finite_homogeneousSubmodule

L82 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finite_homogeneousSubmodule
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
instance finite_homogeneousSubmodule (d : ℕ) :
    Module.Finite L ↥(homogeneousSubmodule (Fin (n + 1)) L d)
instance

finite_piece

L90 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finite_piece
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
instance finite_piece (I : Ideal (MvPolynomial (Fin (n + 1)) L)) (d : ℕ) : Module.Finite L
  (piece I d)
theorem

finrank_piece_add

L94 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem finrank_piece_add (I : Ideal (MvPolynomial (Fin (n + 1)) L)) (d : ℕ) :
    Module.finrank L (piece I d) + Module.finrank L ↥(Ik I d) =
      Module.finrank L ↥(homogeneousSubmodule (Fin (n + 1)) L d)
theorem

finrank_piece_eq_of_Ik_eq

L99 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_eq_of_Ik_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem finrank_piece_eq_of_Ik_eq {I I' : Ideal (MvPolynomial (Fin (n + 1)) L)} {d : ℕ} (h : Ik I d
  = Ik I' d) :
    Module.finrank L (piece I d) = Module.finrank L (piece I' d)
theorem

finrank_piece_eq_zero_of_forall

L104 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_eq_zero_of_forall
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem finrank_piece_eq_zero_of_forall {I : Ideal (MvPolynomial (Fin (n + 1)) L)} {d : ℕ}
    (h : ∀ f : MvPolynomial (Fin (n + 1)) L, f.IsHomogeneous d → f ∈ I) : Module.finrank L (piece I
      d) = 0
theorem

mem_of_finrank_piece_eq_zero

L112 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.mem_of_finrank_piece_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem mem_of_finrank_piece_eq_zero {I : Ideal (MvPolynomial (Fin (n + 1)) L)} {d : ℕ}
    (h : Module.finrank L (piece I d) = 0) (f : MvPolynomial (Fin (n + 1)) L) (hf : f.IsHomogeneous
      d) :
    f ∈ I
theorem

decompose_eq

L122 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.decompose_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem decompose_eq (q : MvPolynomial (Fin (n + 1)) L) (d : ℕ) :
    (DirectSum.decompose (homogeneousSubmodule (Fin (n + 1)) L) q d : MvPolynomial (Fin (n + 1)) L)
      =
      homogeneousComponent d q
theorem

homogeneousComponent_mul_add

L128 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.homogeneousComponent_mul_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem homogeneousComponent_mul_add {G : MvPolynomial (Fin (n + 1)) L} {m : ℕ} (hG :
  G.IsHomogeneous m)
    (a : MvPolynomial (Fin (n + 1)) L) (d : ℕ) :
    homogeneousComponent (m + d) (a * G) = homogeneousComponent d a * G
theorem

span_homogeneous

L137 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.span_homogeneous
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Pieces
variable {L : Type} [Field L]
Lean source · statement
theorem span_homogeneous (s : Set (MvPolynomial (Fin (n + 1)) L))
    (hs : ∀ p ∈ s, ∃ i : ℕ, p.IsHomogeneous i) :
    ∀ p ∈ Ideal.span s, ∀ d : ℕ, homogeneousComponent d p ∈ Ideal.span s
theorem

exists_eq_sum_X_mul

L151 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.exists_eq_sum_X_mul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Regen
variable {L : Type} [Field L]
Lean source · statement
theorem exists_eq_sum_X_mul (k : ℕ) (g : MvPolynomial (Fin (n + 1)) L) (hg : g.IsHomogeneous (k +
  1)) :
    ∃ q : Fin (n + 1) → MvPolynomial (Fin (n + 1)) L, (∀ i, (q i).IsHomogeneous k) ∧ g = ∑ i, X i *
      q i
theorem

finrank_piece_succ_eq_zero

L198 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_succ_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Regen
variable {L : Type} [Field L]
Lean source · statement
theorem finrank_piece_succ_eq_zero {I : Ideal (MvPolynomial (Fin (n + 1)) L)} {k : ℕ}
    (h : Module.finrank L (piece I k) = 0) : Module.finrank L (piece I (k + 1)) = 0
theorem

homogeneous_of_gen

L209 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.homogeneous_of_gen
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Regen
variable {L : Type} [Field L]
variable {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
include hJ in
Lean source · statement
theorem homogeneous_of_gen : ∀ p ∈ J, ∀ i : ℕ, homogeneousComponent i p ∈ J
theorem

finrank_homogeneousSubmodule

L219 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_homogeneousSubmodule
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem finrank_homogeneousSubmodule (d : ℕ) :
    Module.finrank L ↥(homogeneousSubmodule (Fin (n + 1)) L d) = Nat.card {x : Fin (n + 1) →₀ ℕ //
      x.degree = d}
theorem

natCard_degree_zero

L226 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.natCard_degree_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem natCard_degree_zero : Nat.card {x : Fin (n + 1) →₀ ℕ // x.degree = 0} = 1
theorem

finrank_homogeneousSubmodule_le

L232 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_homogeneousSubmodule_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem finrank_homogeneousSubmodule_le (d : ℕ) :
    Module.finrank L ↥(homogeneousSubmodule (Fin (n + 1)) L d) ≤ (n + d).choose n
theorem

finrank_piece_le

L255 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem finrank_piece_le (I : Ideal (MvPolynomial (Fin (n + 1)) L)) (d : ℕ) :
    Module.finrank L (piece I d) ≤ (n + d).choose n
theorem

finrank_piece_bot

L261 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.finrank_piece_bot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem finrank_piece_bot (d : ℕ) :
    Module.finrank L (piece (⊥ : Ideal (MvPolynomial (Fin (n + 1)) L)) d) =
      Nat.card {x : Fin (n + 1) →₀ ℕ // x.degree = d}
theorem

eq_bot_of_finrank_piece_eq

L270 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.eq_bot_of_finrank_piece_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Full
variable (L : Type) [Field L]
Lean source · statement
theorem eq_bot_of_finrank_piece_eq {e : ℕ} (I : Ideal (MvPolynomial (Fin (n + 1)) L))
    (hI : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous e) ∧ I = Ideal.span s)
    (h : Module.finrank L (piece I e) = Nat.card {x : Fin (n + 1) →₀ ℕ // x.degree = e}) : I = ⊥
def

formsIdeal

L293 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.formsIdeal
Documentation

The ideal generated by the homogeneous forms of the specified degree in the given ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Forms
variable {L : Type} [Field L] {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
Lean source · statement
def formsIdeal (e : ℕ) (J : Ideal (MvPolynomial (Fin (n + 1)) L)) :
    Ideal (MvPolynomial (Fin (n + 1)) L)
theorem

formsIdeal_le

L297 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.formsIdeal_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Forms
variable {L : Type} [Field L] {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
Lean source · statement
theorem formsIdeal_le (e : ℕ) : formsIdeal e J ≤ J
theorem

formsIdeal_generated

L299 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.formsIdeal_generated
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Forms
variable {L : Type} [Field L] {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
Lean source · statement
theorem formsIdeal_generated (e : ℕ) : ∃ s : Set (MvPolynomial (Fin (n + 1)) L),
    (∀ p ∈ s, p.IsHomogeneous e) ∧ formsIdeal e J = Ideal.span s
theorem

mem_formsIdeal_of_mem

L302 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.mem_formsIdeal_of_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Forms
variable {L : Type} [Field L] {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
include hJ in
Lean source · full declaration
theorem mem_formsIdeal_of_mem {e : ℕ} (he : m ≤ e) : ∀ (i : ℕ) (x : MvPolynomial (Fin (n + 1)) L),
    x.IsHomogeneous (e + i) → x ∈ J → x ∈ formsIdeal e J
  | 0, x, hx, hxJ => Ideal.subset_span ⟨hxJ, hx⟩
  | i + 1, x, hx, hxJ => by
      obtain ⟨s, hs, hJs⟩ := hJ
      rw [hJs] at hxJ
      obtain ⟨N, f, g, hfg⟩ := Submodule.mem_span_set'.mp hxJ
      set d := e + i + 1 - m with hd
      have hd1 : 1 ≤ d := by omega
      have hsplit : e + i + 1 = m + d := by omega
      have hq : ∀ t : Fin N, ∃ q : Fin (n + 1) → MvPolynomial (Fin (n + 1)) L,
          (∀ k, (q k).IsHomogeneous (d - 1)) ∧ homogeneousComponent d (f t) = ∑ k, X k * q k := fun
            t =>
        exists_eq_sum_X_mul (d - 1) _
          (by rw [Nat.sub_add_cancel hd1]; exact homogeneousComponent_isHomogeneous _ _)
      choose q hq₁ hq₂ using hq
      have hx1 : x = homogeneousComponent (e + i + 1) x := by
        rw [homogeneousComponent_of_mem (show x ∈ homogeneousSubmodule (Fin (n + 1)) L (e + i + 1)
          from hx),
          ite_eq_left rfl]
      have hx2 : x = ∑ k, X k * ∑ t, q t k * (g t : MvPolynomial (Fin (n + 1)) L) := by
        rw [hx1, ← hfg, hsplit, map_sum]
        have : ∀ t : Fin N, homogeneousComponent (m + d) (HSMul.hSMul (f t) (g t : MvPolynomial
          (Fin (n + 1)) L)) =
            ∑ k, X k * (q t k * (g t : MvPolynomial (Fin (n + 1)) L)) := fun t => by
          rw [smul_eq_mul, homogeneousComponent_mul_add (hs _ (g t).2) (f t) d, hq₂ t,
            Finset.sum_mul]
          exact Finset.sum_congr rfl fun k _ => mul_assoc _ _ _
        rw [Finset.sum_congr rfl fun t _ => this t, Finset.sum_comm]
        exact Finset.sum_congr rfl fun k _ => (Finset.mul_sum _ _ _).symm
      rw [hx2]
      refine Ideal.sum_mem _ fun k _ => Ideal.mul_mem_left _ _ ?_
      refine mem_formsIdeal_of_mem he i _ ?_ ?_
      · have : (∑ t, q t k * (g t : MvPolynomial (Fin (n + 1)) L)).IsHomogeneous (d - 1 + m) :=
          IsHomogeneous.sum _ _ _ fun t _ => (hq₁ t k).mul (hs _ (g t).2)
        rwa [show d - 1 + m = e + i by omega] at this
      · rw [hJs]; exact Ideal.sum_mem _ fun t _ => Ideal.mul_mem_left _ _ (Ideal.subset_span (g
          t).2)
theorem

Ik_formsIdeal_eq

L341 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.Ik_formsIdeal_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Forms
variable {L : Type} [Field L] {m : ℕ} (J : Ideal (MvPolynomial (Fin (n + 1)) L))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) L), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
include hJ in
Lean source · statement
theorem Ik_formsIdeal_eq {e : ℕ} (he : m ≤ e) {k : ℕ} (hk : e ≤ k) : Ik (formsIdeal e J) k = Ik J k
theorem

h_succ_eq

L361 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.h_succ_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Growth
variable (h : ℕ → ℕ) {m : ℕ}
  (h₂ : ∀ e, m ≤ e → ∀ (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) →
      Module.finrank K (piece J e) = h e → Module.finrank K (piece J (e + 1)) ≤ h (e + 1))
  (h₃ : ∀ e, m ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
include h₂ h₃ in
Lean source · statement
theorem h_succ_eq {e : ℕ} (hme : m ≤ e) (he : 1 ≤ e) : h (e + 1) = Nat.macaulayPow e (h e)
theorem

two_values

L384 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.two_values
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Positive
variable {K : Type} [Field K] (h : ℕ → ℕ) {m : ℕ}
  (hgrowth : ∀ e, m ≤ e → h (e + 1) = Nat.macaulayPow e (h e))
  (J : Ideal (MvPolynomial (Fin (n + 1)) K))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
  (hm : Module.finrank K (piece J m) = h m) (hm₁ : Module.finrank K (piece J (m + 1)) = h (m + 1))
include hgrowth hJ hm hm₁ in
Lean source · full declaration
theorem two_values : ∀ j : ℕ,
    Module.finrank K (piece J (m + j)) = h (m + j) ∧ Module.finrank K (piece J (m + j + 1)) = h (m
      + j + 1)
  | 0 => ⟨hm, hm₁⟩
  | j + 1 => by
      obtain ⟨hj0, hj1⟩ := two_values j
      refine ⟨hj1, ?_⟩
      have he : m ≤ m + j := Nat.le_add_right m j
      have hk : ∀ k, m + j ≤ k →
          Module.finrank K (piece (formsIdeal (m + j) J) k) = Module.finrank K (piece J k) :=
        fun k hk => finrank_piece_eq_of_Ik_eq (Ik_formsIdeal_eq J hJ he hk)
      have step :=
        MvPolynomial.finrank_piece_add_two_eq_macaulayPow_of_finrank_piece_succ_eq_macaulayPow n (m
        + j)
        K (formsIdeal (m + j) J) (formsIdeal_generated J (m + j))
        (by rw [hk (m + j) le_rfl, hk (m + j + 1) (by omega), hj0, hj1]; exact hgrowth (m + j) he)
      rw [hk (m + j + 1)
        (by omega), hk (m + j + 2) (by omega), hj1, ← hgrowth (m + j + 1) (by omega)] at step
      exact step
theorem

h_eq_zero

L414 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.h_eq_zero
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Zero
variable (h : ℕ → ℕ)
  (h₃ : ∀ e, 0 ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
include h₃ in
Lean source · full declaration
theorem h_eq_zero (h0 : h 0 = 0) : ∀ e, h e = 0
  | 0 => h0
  | e + 1 => by
      obtain ⟨K₀, _, J₀, -, he0, he1⟩ := h₃ e (Nat.zero_le e)
      rw [← he1]
      exact finrank_piece_succ_eq_zero (by rw [he0]; exact h_eq_zero h0 e)
theorem

h_eq_full

L421 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.h_eq_full
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Zero
variable (h : ℕ → ℕ)
  (h₃ : ∀ e, 0 ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
include h₃ in
Lean source · full declaration
theorem h_eq_full (h0 : h 0 = Nat.card {x : Fin (n + 1) →₀ ℕ // x.degree = 0}) :
    ∀ e, h e = Nat.card {x : Fin (n + 1) →₀ ℕ // x.degree = e}
  | 0 => h0
  | e + 1 => by
      obtain ⟨K₀, _, J₀, hJ₀, he0, he1⟩ := h₃ e (Nat.zero_le e)
      have hbot : J₀ = ⊥ := eq_bot_of_finrank_piece_eq K₀ J₀ hJ₀ (by rw [he0]; exact h_eq_full h0 e)
      rw [← he1, hbot]
      exact finrank_piece_bot K₀ (e + 1)
theorem

persistence_zero

L435 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.persistence_zero
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
section Zero
variable (h : ℕ → ℕ)
  (h₃ : ∀ e, 0 ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
variable {K : Type} [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K))
  (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous 0) ∧ J = Ideal.span s)
  (hm : Module.finrank K (piece J 0) = h 0)
include h₃ hJ hm in
Lean source · statement
theorem persistence_zero : ∀ e, Module.finrank K (piece J e) = h e
theorem

main

L458 ↗
AlgebraicCurves.Foundations.Polynomial.Proofs.MvPolynomial_finrank_piece_eq_of_maximal_growth.GotzPers.main
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_eq_of_maximal_growth
namespace GotzPers
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
variable {n : ℕ}
Lean source · statement
theorem main (n m : ℕ) (h : ℕ → ℕ)
    (h₂ : ∀ e, m ≤ e → ∀ (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) →
      Module.finrank K (piece J e) = h e → Module.finrank K (piece J (e + 1)) ≤ h (e + 1))
    (h₃ : ∀ e, m ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
    (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K))
    (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
    (hm : Module.finrank K (piece J m) = h m) (hm₁ : Module.finrank K (piece J (m + 1)) = h (m +
      1)) :
    ∀ e, m ≤ e → Module.finrank K (piece J e) = h e
theorem

finrank_piece_eq_of_maximal_growth

L486 ↗
MvPolynomial.finrank_piece_eq_of_maximal_growth
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Polynomial.Proofs
namespace MvPolynomial_finrank_piece_eq_of_maximal_growth
attribute [local instance] GotzPers.finite_homogeneousSubmodule
attribute [local instance] GotzPers.finite_piece
open MvPolynomial AlgebraicGeometry.HilbertFunctor in
Lean source · statement
theorem _root_.MvPolynomial.finrank_piece_eq_of_maximal_growth
    (n m : ℕ) (h : ℕ → ℕ)
    (h₂ : ∀ e, m ≤ e → ∀ (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) →
      Module.finrank K (piece J e) = h e → Module.finrank K (piece J (e + 1)) ≤ h (e + 1))
    (h₃ : ∀ e, m ≤ e → ∃ (K : Type) (_ : Field K) (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous e) ∧ J = Ideal.span s) ∧
      Module.finrank K (piece J e) = h e ∧ Module.finrank K (piece J (e + 1)) = h (e + 1))
    (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K))
    (hJ : ∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s)
    (hm : Module.finrank K (piece J m) = h m) (hm₁ : Module.finrank K (piece J (m + 1)) = h (m +
      1)) :
    ∀ e, m ≤ e → Module.finrank K (piece J e) = h e

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