NYLL
Module

exists_ideal_forall_mem_iff_app_awayToSection_eq_zero_and_polynomial.lean

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

Module documentation

exists ideal forall mem iff app away To Section eq zero and polynomial

Imports57
  • Mathlib.Algebra.Algebra.Defs
  • Mathlib.Algebra.BigOperators.Group.Finset.Basic
  • Mathlib.Algebra.BigOperators.Group.Finset.Defs
  • Mathlib.Algebra.BigOperators.Ring.Finset
  • Mathlib.Algebra.Category.Ring.Basic
  • Mathlib.Algebra.DirectSum.Decomposition
  • Mathlib.Algebra.Field.Defs
  • Mathlib.Algebra.Field.Rat
  • Mathlib.Algebra.GradedMonoid
  • 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.Submonoid.Defs
  • Mathlib.Algebra.Group.Submonoid.Membership
  • Mathlib.Algebra.GroupWithZero.Defs
  • Mathlib.Algebra.Module.Defs
  • Mathlib.Algebra.Module.LinearMap.Defs
  • Mathlib.Algebra.Module.Submodule.Defs
  • Mathlib.Algebra.MonoidAlgebra.Basic
  • Mathlib.Algebra.MonoidAlgebra.Defs
  • Mathlib.Algebra.MonoidAlgebra.Module
  • Mathlib.Algebra.MvPolynomial.Basic
  • Mathlib.Algebra.Polynomial.Basic
  • Mathlib.Algebra.Polynomial.Eval.Defs
  • Mathlib.Algebra.Ring.Hom.Defs
  • Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
  • Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
  • Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
  • Mathlib.AlgebraicGeometry.Scheme
  • Mathlib.CategoryTheory.Category.Basic
  • Mathlib.CategoryTheory.Functor.Basic
  • Mathlib.Data.Finset.Defs
  • Mathlib.Data.Finset.Insert
  • Mathlib.Data.Nat.Basic
  • Mathlib.Data.Opposite
  • Mathlib.Data.Rat.Init
  • Mathlib.Geometry.RingedSpace.PresheafedSpace
  • Mathlib.GroupTheory.MonoidLocalization.Basic
  • Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.Quotient.Defs
  • Mathlib.Order.Defs.LinearOrder
  • Mathlib.Order.Defs.PartialOrder
  • Mathlib.RingTheory.GradedAlgebra.Basic
  • Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
  • Mathlib.RingTheory.Ideal.Defs
  • Mathlib.RingTheory.Localization.Defs
  • Mathlib.RingTheory.MvPolynomial.Homogeneous
  • Mathlib.Tactic.SplitIfs
  • Nyll.SchemeTheory.ProjectiveSpace.Basic
  • Nyll.AlgebraicCurves.Hilbert.Functor.Basic
  • Nyll.AlgebraicCurves.Foundations.Algebra.Nat_MacaulayPow
  • Nyll.AlgebraicCurves.Foundations.Polynomial.MvPolynomial_finrank_piece_succ_le_macaulayPow
  • Nyll.AlgebraicCurves.Foundations.Algebra.Nat_exists_forall_eq_macaulayPow_of_forall_le_macaulayPow
  • Nyll.AlgebraicCurves.Foundations.Polynomial.Nat_exists_polynomial_forall_eval_eq_of_forall_eq_macaulayPow
Imported by4

Declarations

def

xpow

L95 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.xpow
Documentation

The dth power of a variable, regarded as a homogeneous polynomial of degree d.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def xpow (i : Fin (n + 1)) (d : ℕ) : ↥(homogeneousSubmodule (Fin (n + 1)) k d)
def

frac

L100 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.frac
Documentation

The degree-zero homogeneous fraction with numerator F and denominator the dth variable power.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def frac (i : Fin (n + 1)) (d : ℕ) (F : ↥(homogeneousSubmodule (Fin (n + 1)) k d)) :
    HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i)
theorem

frac_zero

L108 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.frac_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem frac_zero (i : Fin (n + 1)) (d : ℕ) : frac (k := k) i d 0 = 0
theorem

frac_add

L114 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.frac_add
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem frac_add (i : Fin (n + 1)) (d : ℕ) (F G : ↥(homogeneousSubmodule (Fin (n + 1)) k d)) :
    frac i d (F + G) = frac i d F + frac i d G
theorem

frac_mul

L121 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.frac_mul
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem frac_mul (i : Fin (n + 1)) (e d : ℕ) (G : ↥(homogeneousSubmodule (Fin (n + 1)) k e))
    (F : ↥(homogeneousSubmodule (Fin (n + 1)) k d)) :
    frac i (e + d) ⟨(G : MvPolynomial (Fin (n + 1)) k) * (F : MvPolynomial (Fin (n + 1)) k),
      SetLike.mul_mem_graded G.2 F.2⟩ =
      frac i e G * frac i d F
def

chartHom

L134 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.chartHom
Documentation

The homomorphism from a projective affine chart to sections on its inverse image.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def chartHom (i : Fin (n + 1)) :
    HomogeneousLocalization.Away 𝒜 (MvPolynomial.X i) →+*
      ↑(Zk.presheaf.obj (Opposite.op (ιk ⁻¹ᵁ (Proj.basicOpen 𝒜 (MvPolynomial.X i)))))
def

Van

L140 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.Van
Documentation

The condition that a homogeneous polynomial vanishes on every standard projective chart.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def Van (d : ℕ) (F : ↥(homogeneousSubmodule (Fin (n + 1)) k d)) : Prop
theorem

Van_zero

L143 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.Van_zero
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem Van_zero (d : ℕ) : Van ιk d 0
theorem

Van_add

L146 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.Van_add
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem Van_add {d : ℕ} {F G : ↥(homogeneousSubmodule (Fin (n + 1)) k d)}
    (hF : Van ιk d F) (hG : Van ιk d G) : Van ιk d (F + G)
theorem

Van_mul_left

L150 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.Van_mul_left
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem Van_mul_left (e : ℕ) {d : ℕ} (G : ↥(homogeneousSubmodule (Fin (n + 1)) k e))
    {F : ↥(homogeneousSubmodule (Fin (n + 1)) k d)} (hF : Van ιk d F) :
    Van ιk (e + d) ⟨(G : MvPolynomial (Fin (n + 1)) k) * (F : MvPolynomial (Fin (n + 1)) k),
      SetLike.mul_mem_graded G.2 F.2⟩
def

comp

L157 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.comp
Documentation

The homogeneous degree-d component of a polynomial, with its homogeneity proof.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
def comp (d : ℕ) (p : MvPolynomial (Fin (n + 1)) k) : ↥(homogeneousSubmodule (Fin (n + 1)) k d)
theorem

comp_zero

L160 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.comp_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
omit ιk in
Lean source · statement
theorem comp_zero (d : ℕ) : comp (k := k) (n := n) d 0 = 0
theorem

comp_add

L162 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.comp_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
omit ιk in
Lean source · statement
theorem comp_add (d : ℕ) (p q : MvPolynomial (Fin (n + 1)) k) : comp d (p + q) = comp d p + comp d
  q
theorem

coe_decompose

L166 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.coe_decompose
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
omit ιk in
Lean source · statement
theorem coe_decompose (φ : MvPolynomial (Fin (n + 1)) k) (i : ℕ) :
    ((DirectSum.decompose 𝒜 φ) i : MvPolynomial (Fin (n + 1)) k) = homogeneousComponent i φ
theorem

homogeneousComponent_mul_of_mem_left

L170 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.homogeneousComponent_mul_of_mem_left
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
omit ιk in
Lean source · full declaration
theorem homogeneousComponent_mul_of_mem_left {e : ℕ} {c : MvPolynomial (Fin (n + 1)) k}
    (hc : c ∈ homogeneousSubmodule (Fin (n + 1)) k e) (p : MvPolynomial (Fin (n + 1)) k) (d : ℕ) :
    homogeneousComponent d (c * p) = if e ≤ d then c * homogeneousComponent (d - e) p else 0 := by
  have h := DirectSum.coe_decompose_mul_of_left_mem 𝒜 (b := p) d hc
  simpa only [coe_decompose] using h
theorem

comp_of_mem

L176 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.comp_of_mem
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
omit ιk in
Lean source · full declaration
theorem comp_of_mem {e : ℕ} {F : MvPolynomial (Fin (n + 1)) k}
    (hF : F ∈ homogeneousSubmodule (Fin (n + 1)) k e) (d : ℕ) :
    comp d F = if h : d = e then ⟨F, h ▸ hF⟩ else 0 := by
  apply Subtype.ext
  simp only [comp, homogeneousComponent_of_mem hF]
  split_ifs <;> rfl
theorem

Van_comp_sum

L183 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.Van_comp_sum
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem Van_comp_sum {ι : Type} (s : Finset ι) (f : ι → MvPolynomial (Fin (n + 1)) k) (d : ℕ)
    (h : ∀ a ∈ s, Van ιk d (comp d (f a))) : Van ιk d (comp d (∑ a ∈ s, f a))
def

satIdeal

L194 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.satIdeal
Documentation

The ideal whose homogeneous components vanish on every standard projective chart.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · full declaration
def satIdeal : Ideal (MvPolynomial (Fin (n + 1)) k) where
  carrier := {p | ∀ d : ℕ, Van ιk d (comp d p)}
  zero_mem' := by
    intro d; rw [comp_zero]; exact Van_zero ιk d
  add_mem' := by
    intro p q hp hq d
    rw [comp_add]; exact Van_add ιk (hp d) (hq d)
  smul_mem' := by
    intro c p hp d
    rw [smul_eq_mul, ← sum_homogeneousComponent c, Finset.sum_mul]
    apply Van_comp_sum
    intro e _
    rcases Nat.lt_or_ge d e with hde | hed
    · have hc0 : comp d (homogeneousComponent e c * p) = 0 := by
        apply Subtype.ext
        simp only [comp, homogeneousComponent_mul_of_mem_left (homogeneousComponent_mem e c) p d,
          ite_eq_right (not_le.mpr hde), Submodule.coe_zero]
      rw [hc0]; exact Van_zero ιk d
    · obtain ⟨d', rfl⟩ := Nat.exists_eq_add_of_le hed
      have hceq : comp (e + d') (homogeneousComponent e c * p) =
          ⟨(comp e c : MvPolynomial (Fin (n + 1)) k) * (comp d' p : MvPolynomial (Fin (n + 1)) k),
            SetLike.mul_mem_graded (comp e c).2 (comp d' p).2⟩ := by
        apply Subtype.ext
        simp only [comp, homogeneousComponent_mul_of_mem_left (homogeneousComponent_mem e c) p (e +
          d'),
          ite_eq_left (Nat.le_add_right e d'), Nat.add_sub_cancel_left]
      rw [hceq]
      exact Van_mul_left ιk e (comp e c) (hp d')
theorem

mem_satIdeal_iff

L223 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.mem_satIdeal_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem mem_satIdeal_iff (p : MvPolynomial (Fin (n + 1)) k) :
    p ∈ satIdeal ιk ↔ ∀ d : ℕ, Van ιk d (comp d p)
theorem

satIdeal_homogeneous

L226 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.satIdeal_homogeneous
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem satIdeal_homogeneous (p : MvPolynomial (Fin (n + 1)) k) (hp : p ∈ satIdeal ιk) (d : ℕ) :
    homogeneousComponent d p ∈ satIdeal ιk
theorem

mem_satIdeal_iff_of_isHomogeneous

L235 ↗
AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial.E2SOL.mem_satIdeal_iff_of_isHomogeneous
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace E2SOL
section Sat
variable {n : ℕ} {k : Type} [Field k]
    {Zk : Scheme.{0}} (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k
Lean source · statement
theorem mem_satIdeal_iff_of_isHomogeneous {d : ℕ} {F : MvPolynomial (Fin (n + 1)) k}
    (hF : F.IsHomogeneous d) :
    F ∈ satIdeal ιk ↔ Van ιk d ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
theorem

exists_ideal_forall_mem_iff_app_awayToSection_eq_zero_and_polynomial

L265 ↗
AlgebraicGeometry.HilbertFunctor.exists_ideal_forall_mem_iff_app_awayToSection_eq_zero_and_polynomial
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicGeometry.HilbertFunctor
noncomputable section
open _root_.AlgebraicCurves.Hilbert.Proofs.HilbertIdealPolynomial
open _root_.MvPolynomial _root_.CategoryTheory _root_.CategoryTheory.Limits _root_.AlgebraicGeometry
  _root_.AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open E2SOL in
Lean source · statement
theorem exists_ideal_forall_mem_iff_app_awayToSection_eq_zero_and_polynomial
    (n : ℕ) (k : Type) [Field k]
    (Zk : Scheme.{0}) (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k))
    (_hιk : IsClosedImmersion ιk) :
    ∃ (I : Ideal (MvPolynomial (Fin (n + 1)) k)),
      (∀ p ∈ I, ∀ d : ℕ, homogeneousComponent d p ∈ I) ∧
      (∀ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d),
        (F ∈ I ↔ ∀ i : Fin (n + 1),
                  (ιk.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                    (MvPolynomial.X i)))
                    (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)
                      (MvPolynomial.X i)
                      (HomogeneousLocalization.mk
                        { deg := d
                          num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                          den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d
                            _).mpr
                            (MvPolynomial.isHomogeneous_X_pow i d)⟩
                          den_mem := ⟨d, rfl⟩ })) = 0)) ∧
      ∃ (P : Polynomial ℚ) (D₀ : ℕ), ∀ d : ℕ, D₀ ≤ d → (Module.finrank k (piece I d) : ℚ) = P.eval
        (d : ℚ)

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