NYLL
Module

Point_flat_comp_of_ideal_basicOpen_eq_span.lean

Nyll.AlgebraicCurves.Hilbert.Point_flat_comp_of_ideal_basicOpen_eq_span
5 declarations indexed from sourceView source ↗

Module documentation

Point flat comp of ideal basic Open eq span

Imports4
Imported by1

Declarations

theorem

decompose_eq

L40 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_flat_comp_of_ideal_basicOpen_eq_span.K1ASOL.decompose_eq
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_flat_comp_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
namespace K1ASOL
open HomogeneousLocalization
variable (n : ℕ) (A : Type) [CommRing A]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem decompose_eq (a : MvPolynomial (Fin (n + 1)) A) (k : ℕ) :
    (DirectSum.decompose 𝒜 a k : MvPolynomial (Fin (n + 1)) A) = homogeneousComponent k a
theorem

iSup_basicOpen_X

L44 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_flat_comp_of_ideal_basicOpen_eq_span.K1ASOL.iSup_basicOpen_X
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_flat_comp_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
namespace K1ASOL
open HomogeneousLocalization
variable (n : ℕ) (A : Type) [CommRing A]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem iSup_basicOpen_X : (⨆ i : Fin (n + 1), Proj.basicOpen 𝒜 (X i)) = ⊤
theorem

fromSpec_eq

L51 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_flat_comp_of_ideal_basicOpen_eq_span.K1ASOL.fromSpec_eq
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_flat_comp_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
namespace K1ASOL
open HomogeneousLocalization
variable (n : ℕ) (A : Type) [CommRing A]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem fromSpec_eq (i : Fin (n + 1)) :
    (Proj.isAffineOpen_basicOpen 𝒜 (X i) (ProjSpace.X_mem_one A n i) one_pos).fromSpec =
      Spec.map (Proj.awayToSection 𝒜 (X i)) ≫ Proj.awayι 𝒜 (X i) (ProjSpace.X_mem_one A n i)
        one_pos
theorem

algebraMap_away_eq

L63 ↗
AlgebraicCurves.Hilbert.Proofs.S_AlgebraicGeometry_HilbertFunctor_Point_flat_comp_of_ideal_basicOpen_eq_span.K1ASOL.algebraMap_away_eq
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_flat_comp_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
namespace K1ASOL
open HomogeneousLocalization
variable (n : ℕ) (A : Type) [CommRing A]
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
Lean source · statement
theorem algebraMap_away_eq (i : Fin (n + 1)) :
    algebraMap A (Away 𝒜 (MvPolynomial.X i)) =
      (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers (X i))).comp
        ((GradedRing.projZeroRingHom' 𝒜).comp (algebraMap A (MvPolynomial (Fin (n + 1)) A)))
theorem

flat_comp_of_ideal_basicOpen_eq_span

L80 ↗
AlgebraicGeometry.HilbertFunctor.Point.flat_comp_of_ideal_basicOpen_eq_span
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Hilbert.Proofs
namespace S_AlgebraicGeometry_HilbertFunctor_Point_flat_comp_of_ideal_basicOpen_eq_span
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor
attribute [local instance] MvPolynomial.gradedAlgebra
open K1ASOL in
Lean source · statement
theorem _root_.AlgebraicGeometry.HilbertFunctor.Point.flat_comp_of_ideal_basicOpen_eq_span
    (n : ℕ) (A : Type) [CommRing A] (h : ℕ → ℕ) (p : Point A n h)
    (𝓘 : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).IdealSheafData)
    (h𝓘 : ∀ i : Fin (n + 1),
        𝓘.ideal ⟨Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i),
          Proj.isAffineOpen_basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i)
            (ProjSpace.X_mem_one A n i) one_pos⟩ =
        Ideal.span { s | ∃ (d : ℕ) (F : MvPolynomial (Fin (n + 1)) A) (hF : F.IsHomogeneous d),
          F ∈ p.I ∧
          s = (Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A) (X i))
              (HomogeneousLocalization.mk
                { deg := d
                  num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                  den := ⟨X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                    (MvPolynomial.isHomogeneous_X_pow i d)⟩
                  den_mem := ⟨d, rfl⟩ }) }) :
    Flat (𝓘.subschemeι ≫ ProjSpace.π A n)

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