NYLL
Module

ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.lean

Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
17 declarations indexed from sourceView source ↗

Module documentation

Proj Space exists ideal Sheaf Data ideal basic Open eq span

Imports23
Imported by1

Declarations

theorem

pow_mem

L89 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.pow_mem
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem pow_mem (f : S) (hf : f ∈ 𝒜 1) (e : ℕ) : f ^ e ∈ 𝒜 e
def

gens

L96 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.gens
Documentation

Homogeneous fractions whose numerators belong to the ideal, with matching powers of the chosen degree-one denominator.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
def gens (f : S) (hf : f ∈ 𝒜 1) : Set (Away 𝒜 f)
def

chartIdeal

L108 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.chartIdeal
Documentation

The ideal on a projective chart generated by homogeneous fractions from the given homogeneous ideal.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
def chartIdeal (f : S) (hf : f ∈ 𝒜 1) : Ideal (Away 𝒜 f)
def

overlapUnit

L111 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.overlapUnit
Documentation

The overlap fraction represented by g ^ 2 / x, where x = f * g.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
def overlapUnit (f g x : S) (hg : g ∈ 𝒜 1) (_hx : x = f * g) (hxm : x ∈ 𝒜 2) : Away 𝒜 x
theorem

awayMap_gen

L118 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.awayMap_gen
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem awayMap_gen (f g x : S) (hf : f ∈ 𝒜 1) (hg : g ∈ 𝒜 1) (hx : x = f * g) (hx' : x = g * f)
    (d : ℕ) (F : S) (hF : F.IsHomogeneous d) :
    awayMap 𝒜 hg hx (HomogeneousLocalization.mk
        { deg := d
          num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
          den := ⟨f ^ d, pow_mem n A f hf d⟩
          den_mem := ⟨d, rfl⟩ }) =
      overlapUnit n A f g x hg hx (hx ▸ SetLike.mul_mem_graded hf hg) ^ d *
      awayMap 𝒜 hf hx' (HomogeneousLocalization.mk
        { deg := d
          num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
          den := ⟨g ^ d, pow_mem n A g hg d⟩
          den_mem := ⟨d, rfl⟩ })
theorem

map_chartIdeal_le

L141 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.map_chartIdeal_le
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem map_chartIdeal_le (f g x : S) (hf : f ∈ 𝒜 1) (hg : g ∈ 𝒜 1) (hx : x = f * g) (hx' : x = g *
  f) :
    (chartIdeal n A I f hf).map (awayMap 𝒜 hg hx) ≤ (chartIdeal n A I g hg).map (awayMap 𝒜 hf hx')
theorem

map_chartIdeal_eq

L151 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.map_chartIdeal_eq
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem map_chartIdeal_eq (f g x : S) (hf : f ∈ 𝒜 1) (hg : g ∈ 𝒜 1) (hx : x = f * g) (hx' : x = g *
  f) :
    (chartIdeal n A I f hf).map (awayMap 𝒜 hg hx) = (chartIdeal n A I g hg).map (awayMap 𝒜 hf hx')
def

chartSheaf

L159 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.chartSheaf
Documentation

The ideal sheaf on the affine chart induced by the chart ideal.

Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
def chartSheaf (f : S) (hf : f ∈ 𝒜 1) : (Spec (.of (Away 𝒜 f))).IdealSheafData
theorem

chartSheaf_comap_specMap

L163 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.chartSheaf_comap_specMap
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem chartSheaf_comap_specMap (f g x : S) (hf : f ∈ 𝒜 1) (hg : g ∈ 𝒜 1) (hx : x = f * g) (hx' :
  x = g * f) :
    (chartSheaf n A I f hf).comap (Spec.map (CommRingCat.ofHom (awayMap 𝒜 hg hx))) =
      (chartSheaf n A I g hg).comap (Spec.map (CommRingCat.ofHom (awayMap 𝒜 hf hx')))
theorem

le_preimage_awayι

L216 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.le_preimage_awayι
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem le_preimage_awayι (f : S) (hf : f ∈ 𝒜 1) :
    (⊤ : (Spec (.of (Away 𝒜 f))).Opens) ≤ Proj.awayι 𝒜 f hf one_pos ⁻¹ᵁ Proj.basicOpen 𝒜 f
theorem

ofIdealTop_ideal_top

L223 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.ofIdealTop_ideal_top
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem ofIdealTop_ideal_top {Y : Scheme.{0}} [IsAffine Y] (J : Ideal Γ(Y, ⊤)) :
    (Scheme.IdealSheafData.ofIdealTop J).ideal ⟨⊤, isAffineOpen_top Y⟩ = J
theorem

appLE_awayToSection

L229 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.appLE_awayToSection
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem appLE_awayToSection (f : S) (hf : f ∈ 𝒜 1) (z : Away 𝒜 f) :
    (Proj.awayι 𝒜 f hf one_pos).appLE (Proj.basicOpen 𝒜 f) ⊤ (le_preimage_awayι n A f hf)
        (Proj.awayToSection 𝒜 f z) =
      (Scheme.ΓSpecIso (.of (Away 𝒜 f))).inv z
theorem

bijective_appLE

L259 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.bijective_appLE
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem bijective_appLE (f : S) (hf : f ∈ 𝒜 1) :
    Function.Bijective
      ((Proj.awayι 𝒜 f hf one_pos).appLE (Proj.basicOpen 𝒜 f) ⊤ (le_preimage_awayι n A f hf))
theorem

ideal_eq_of_map_appLE

L280 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.ideal_eq_of_map_appLE
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem ideal_eq_of_map_appLE (f : S) (hf : f ∈ 𝒜 1) (𝔧 : Ideal Γ(Proj 𝒜, Proj.basicOpen 𝒜 f))
    (h : (chartIdeal n A I f hf).map (Scheme.ΓSpecIso (.of (Away 𝒜 f))).inv.hom =
      𝔧.map ((Proj.awayι 𝒜 f hf one_pos).appLE (Proj.basicOpen 𝒜 f) ⊤ (le_preimage_awayι n A f
        hf)).hom) :
    𝔧 = (chartIdeal n A I f hf).map (Proj.awayToSection 𝒜 f).hom
theorem

compat

L294 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.compat
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem compat (i j : Fin (n + 1)) {V : Scheme.{0}}
    (a : V ⟶ Spec (.of (Away 𝒜 (X i)))) (b : V ⟶ Spec (.of (Away 𝒜 (X j))))
    (hab : a ≫ Proj.awayι 𝒜 (X i) (ProjSpace.X_mem_one A n i) one_pos =
      b ≫ Proj.awayι 𝒜 (X j) (ProjSpace.X_mem_one A n j) one_pos) :
    (chartSheaf n A I (X i) (ProjSpace.X_mem_one A n i)).comap a =
      (chartSheaf n A I (X j) (ProjSpace.X_mem_one A n j)).comap b
theorem

main

L323 ↗
AlgebraicCurves.Geometry.Projective.Proofs.ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span.AlgebraicGeometry.ProjSpace.K0.main
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace AlgebraicGeometry
namespace ProjSpace
namespace K0
open _root_.AlgebraicGeometry.ProjSpace
open _root_.AlgebraicGeometry
variable (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A))
local notation "𝒜" => MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A
local notation "S" => MvPolynomial (Fin (n + 1)) A
Lean source · statement
theorem main :
    ∃ 𝓘 : (Proj 𝒜).IdealSheafData, ∀ i : Fin (n + 1),
      𝓘.ideal ⟨Proj.basicOpen 𝒜 (X i), Proj.isAffineOpen_basicOpen 𝒜 (X i) (ProjSpace.X_mem_one A n
        i) one_pos⟩ =
        (chartIdeal n A I (X i) (ProjSpace.X_mem_one A n i)).map (Proj.awayToSection 𝒜 (X i)).hom
theorem

exists_idealSheafData_ideal_basicOpen_eq_span

L356 ↗
AlgebraicGeometry.ProjSpace.exists_idealSheafData_ideal_basicOpen_eq_span
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Projective.Proofs
namespace ProjSpace_exists_idealSheafData_ideal_basicOpen_eq_span
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.HomogeneousLocalization
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.MvPolynomial
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.HilbertFunctor
Lean source · statement
theorem _root_.AlgebraicGeometry.ProjSpace.exists_idealSheafData_ideal_basicOpen_eq_span
    (n : ℕ) (A : Type) [CommRing A] (I : Ideal (MvPolynomial (Fin (n + 1)) A)) :
    ∃ 𝓘 : (Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) A)).IdealSheafData,
      ∀ 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 ∈ 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⟩ }) }

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