NYLL
Module

Point_I_eq_span_of_forall_finrank_piece_succ_le.lean

Nyll.AlgebraicCurves.Hilbert.Point_I_eq_span_of_forall_finrank_piece_succ_le
22 declarations indexed from sourceView source ↗

Module documentation

Point I eq span of forall finrank piece succ le

Imports22
  • Mathlib.Algebra.Module.Projective
  • Mathlib.Data.Finsupp.Multiset
  • Mathlib.Data.Finsupp.Weight
  • Mathlib.Data.Sym.Card
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.LinearAlgebra.Dimension.StrongRankCondition
  • Mathlib.LinearAlgebra.FiniteDimensional.Basic
  • Mathlib.LinearAlgebra.TensorProduct.Prod
  • Mathlib.LinearAlgebra.TensorProduct.Quotient
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Finiteness.Nakayama
  • Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  • Mathlib.RingTheory.MvPolynomial.Basic
  • Mathlib.RingTheory.MvPolynomial.Homogeneous
  • Mathlib.RingTheory.Spectrum.Prime.FreeLocus
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.Tactic.Abel
  • Nyll.AlgebraicCurves.Hilbert.Functor.Basic
  • Nyll.AlgebraicCurves.Hilbert.exists_linearEquiv_baseChange_piece_map
Imported by1

Declarations

theorem

exists_equiv_prod_ker

L56 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.exists_equiv_prod_ker
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
section Modules
variable {A : Type} [CommRing A]
Lean source · statement
theorem exists_equiv_prod_ker {Q₁ Q₂ : Type} [AddCommGroup Q₁] [Module A Q₁] [AddCommGroup Q₂]
  [Module A Q₂]
    [Module.Projective A Q₂] (π : Q₁ →ₗ[A] Q₂) (hπ : Function.Surjective π) :
    ∃ e : Q₁ ≃ₗ[A] Q₂ × LinearMap.ker π, ∀ x, (e x).1 = π x
theorem

subsingleton_of_finrank_fiber_eq_zero

L72 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.subsingleton_of_finrank_fiber_eq_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
section Modules
variable {A : Type} [CommRing A]
Lean source · statement
theorem subsingleton_of_finrank_fiber_eq_zero (K : Type) [AddCommGroup K] [Module A K]
  [Module.Finite A K]
    (hK : ∀ p : PrimeSpectrum A, Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[A]
      K) = 0) :
    Subsingleton K
theorem

finite_homogeneousSubmodule

L120 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.finite_homogeneousSubmodule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem finite_homogeneousSubmodule (R : Type) [CommRing R] (d : ℕ) :
    Module.Finite R ↥(homogeneousSubmodule (Fin (n + 1)) R d)
theorem

free_homogeneousSubmodule

L128 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.free_homogeneousSubmodule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem free_homogeneousSubmodule (R : Type) [CommRing R] (d : ℕ) :
    Module.Free R ↥(homogeneousSubmodule (Fin (n + 1)) R d)
theorem

finite_piece

L134 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.finite_piece
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem finite_piece (R : Type) [CommRing R] (J : Ideal (MvPolynomial (Fin (n + 1)) R)) (d
  : ℕ) :
    Module.Finite R (piece J d)
theorem

natCard_degree_eq

L143 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.natCard_degree_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem natCard_degree_eq (d : ℕ) : Nat.card {s : Fin (n + 1) →₀ ℕ // s.degree = d} = (n +
  d).choose n
theorem

finrank_homogeneousSubmodule

L167 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.finrank_homogeneousSubmodule
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem finrank_homogeneousSubmodule (A : Type) [CommRing A] [Nontrivial A] (d : ℕ) :
    Module.finrank A ↥(homogeneousSubmodule (Fin (n + 1)) A d) = (n + d).choose n
theorem

span_homogeneous

L174 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.span_homogeneous
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
Lean source · statement
theorem span_homogeneous (A : Type) [CommRing A] (s : Set (MvPolynomial (Fin (n + 1)) A)) (e : ℕ)
    (hs : ∀ p ∈ s, p.IsHomogeneous e) :
    ∀ p ∈ Ideal.span s, ∀ d : ℕ, homogeneousComponent d p ∈ Ideal.span s
def

J'

L190 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.J'
Documentation

The ideal generated by the homogeneous elements of the specified degree in the point ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
def J' : Ideal (MvPolynomial (Fin (n + 1)) A)
theorem

J'_le

L193 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.J'_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem J'_le : J' h P e ≤ P.I
theorem

J'_generated

L195 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.J'_generated
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem J'_generated : ∃ s : Set (MvPolynomial (Fin (n + 1)) A), (∀ p ∈ s, p.IsHomogeneous e) ∧ J'
  h P e = Ideal.span s
theorem

J'_homogeneous

L199 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.J'_homogeneous
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem J'_homogeneous : ∀ p ∈ J' h P e, ∀ d : ℕ, homogeneousComponent d p ∈ J' h P e
theorem

comap_J'_eq

L202 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.comap_J'_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem comap_J'_eq :
    Submodule.comap (homogeneousSubmodule (Fin (n + 1)) A e).subtype ((J' h P e).restrictScalars A)
      =
      Submodule.comap (homogeneousSubmodule (Fin (n + 1)) A e).subtype (P.I.restrictScalars A)
def

pieceJ'Equiv

L211 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.pieceJ'Equiv
Documentation

The equivalence of the degree pieces for the generated ideal and the original point ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
def pieceJ'Equiv : piece (J' h P e) e ≃ₗ[A] piece P.I e
def

π

L215 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.π
Documentation

The quotient map on the next degree piece induced by inclusion of the generated ideal.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
def π : piece (J' h P e) (e + 1) →ₗ[A] piece P.I (e + 1)
theorem

π_mk

L222 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.π_mk
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem π_mk (q : ↥(homogeneousSubmodule (Fin (n + 1)) A (e + 1))) :
    π h P e (Submodule.Quotient.mk q) = Submodule.Quotient.mk q
theorem

π_surjective

L225 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.π_surjective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
Lean source · statement
theorem π_surjective : Function.Surjective (π h P e)
theorem

finrank_fiber_Q₁_le

L235 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.finrank_fiber_Q₁_le
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
variable (hm : ∀ (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 hm in
Lean source · statement
theorem finrank_fiber_Q₁_le (p : PrimeSpectrum A) :
    Module.finrank p.asIdeal.ResidueField (p.asIdeal.ResidueField ⊗[A] piece (J' h P e) (e + 1)) ≤
      h (e + 1)
theorem

ker_π_eq_bot

L259 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.ker_π_eq_bot
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
variable (hm : ∀ (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 hm in
Lean source · statement
theorem ker_π_eq_bot : LinearMap.ker (π h P e) = ⊥
theorem

mem_J'_of_mem

L301 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.mem_J'_of_mem
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Step
variable {A : Type} [CommRing A] (h : ℕ → ℕ) (P : Point A n h) (e : ℕ)
variable (hm : ∀ (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 hm in
Lean source · statement
theorem mem_J'_of_mem (q : MvPolynomial (Fin (n + 1)) A) (hqI : q ∈ P.I) (hq : q.IsHomogeneous (e +
  1)) :
    q ∈ J' h P e
theorem

eq_zero_of_mem_of_lt

L321 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le.HilbGenH2c.eq_zero_of_mem_of_lt
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbGenH2c
variable {n : ℕ}
section Low
variable {A : Type} [CommRing A] [Nontrivial A] (h : ℕ → ℕ) (P : Point A n h) (d : ℕ)
  (hd : h d = Nat.choose (n + d) n)
include hd in
Lean source · statement
theorem eq_zero_of_mem_of_lt (q : MvPolynomial (Fin (n + 1)) A) (hqI : q ∈ P.I) (hq :
  q.IsHomogeneous d) : q = 0
theorem

I_eq_span_of_forall_finrank_piece_succ_le

L364 ↗
AlgebraicGeometry.HilbertFunctor.Point.I_eq_span_of_forall_finrank_piece_succ_le
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_I_eq_span_of_forall_finrank_piece_succ_le
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HilbGenH2c in
Lean source · statement
theorem _root_.AlgebraicGeometry.HilbertFunctor.Point.I_eq_span_of_forall_finrank_piece_succ_le
    (n m : ℕ) (h : ℕ → ℕ) (h₁ : ∀ d, d < m → h d = Nat.choose (n + d) n)
    (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))
    (A : Type) [CommRing A] (P : Point A n h) :
    P.I = Ideal.span {p | p ∈ P.I ∧ p.IsHomogeneous m}

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