Module

exists_ideal_forall_projective_piece_succ_iff.lean

Nyll.AlgebraicCurves.Hilbert.exists_ideal_forall_projective_piece_succ_iff

4 declarations indexed from sourceView source ↗

Module documentation

exists ideal forall projective piece succ iff

Imports5

Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Nyll.AlgebraicCurves.Hilbert.Functor.Basic
Nyll.AlgebraicCurves.Hilbert.exists_linearEquiv_baseChange_piece_map
Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Module_exists_ideal_forall_projective_and_rankAtStalk_eq_iff

Imported by1

Nyll.AlgebraicCurves.Hilbert.All

theorem

finite_homogeneousSubmodule

L37 ↗

AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_ideal_forall_projective_piece_succ_iff.HilbClosedH2b.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_exists_ideal_forall_projective_piece_succ_iff
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbClosedH2b
variable {n : ℕ}

Lean source · statement

theorem finite_homogeneousSubmodule (R : Type) [CommRing R] (d : ℕ) :
    Module.Finite R ↥(homogeneousSubmodule (Fin (n + 1)) R d)

theorem

finite_piece

L45 ↗

AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_ideal_forall_projective_piece_succ_iff.HilbClosedH2b.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_exists_ideal_forall_projective_piece_succ_iff
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbClosedH2b
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

span_homogeneous

L50 ↗

AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_exists_ideal_forall_projective_piece_succ_iff.HilbClosedH2b.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_exists_ideal_forall_projective_piece_succ_iff
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
namespace HilbClosedH2b
variable {n : ℕ}

Lean source · statement

theorem span_homogeneous (A : Type) [CommRing A] (s : Set (MvPolynomial (Fin (n + 1)) A)) (m : ℕ)
    (hs : ∀ p ∈ s, p.IsHomogeneous m) :
    ∀ p ∈ Ideal.span s, ∀ d : ℕ, homogeneousComponent d p ∈ Ideal.span s

theorem

exists_ideal_forall_projective_piece_succ_iff

L64 ↗

AlgebraicGeometry.HilbertFunctor.exists_ideal_forall_projective_piece_succ_iff

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_exists_ideal_forall_projective_piece_succ_iff
open MvPolynomial AlgebraicGeometry.HilbertFunctor
open scoped TensorProduct
attribute [local instance] MvPolynomial.gradedAlgebra
open HilbClosedH2b in

Lean source · statement

theorem _root_.AlgebraicGeometry.HilbertFunctor.exists_ideal_forall_projective_piece_succ_iff
    (n m q r : ℕ)
    (hmax : ∀ (K : Type) [Field K] (J : Ideal (MvPolynomial (Fin (n + 1)) K)),
      (∃ s : Set (MvPolynomial (Fin (n + 1)) K), (∀ p ∈ s, p.IsHomogeneous m) ∧ J = Ideal.span s) →
      Module.finrank K (piece J m) = q → Module.finrank K (piece J (m + 1)) ≤ r)
    (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
    (hI : ∃ s : Set (MvPolynomial (Fin (n + 1)) A), (∀ p ∈ s, p.IsHomogeneous m) ∧ I = Ideal.span s)
    (hproj : Module.Projective A (piece I m))
    (hrank : ∀ p : PrimeSpectrum A, Module.rankAtStalk (piece I m) p = q) :
    ∃ 𝔞 : Ideal A, ∀ (B : Type) [CommRing B] [Algebra A B],
      (Module.Projective B (piece (I.map (MvPolynomial.map (algebraMap A B))) (m + 1)) ∧
        ∀ 𝔮 : PrimeSpectrum B,
          Module.rankAtStalk (piece (I.map (MvPolynomial.map (algebraMap A B))) (m + 1)) 𝔮 = r) ↔
      ∀ a ∈ 𝔞, algebraMap A B a = 0

Module documentation

exists ideal forall projective piece succ iff

Declarations

finite_homogeneousSubmodule

finite_piece

span_homogeneous

exists_ideal_forall_projective_piece_succ_iff