NYLL
Module

InfinityChartStalk.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.InfinityChartStalk
13 declarations indexed from sourceView source ↗

Module documentation

The actual projective stalk at the infinity chart point

Swapping the homogeneous coordinates turns the standard affine chart into the chart T₀ ≠ 0. At the prime (maximalIdeal R, X), the open immersion identifies the stalk of the projective line with the prime localization of R[X]. Polynomial germs are constructed from the actual structure-sheaf germ on Spec R[X] and the inverse chart stalk map. The stalk isomorphism sends these germs to the usual localization map.

This identifies the ring in the infinity-chart intersection calculation with an actual projective local ring, as needed for Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports19
Imported by11

Declarations

def

infinityChartEmbedding

L55 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartEmbedding
Documentation

The affine chart at infinity, with coordinate T₁ / T₀.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def infinityChartEmbedding (R : Type u) [CommRing R] :
    Spec (CommRingCat.of R[X]) ⟶ ProjectiveLine R
instance

(anonymous instance)

L59 ↗
Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
instance (R : Type u) [CommRing R] : IsOpenImmersion (infinityChartEmbedding R)
theorem

infinityChartEmbedding_opensRange

L64 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartEmbedding_opensRange
Documentation

The infinity chart is the actual open T₀ ≠ 0 in the projective line.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem infinityChartEmbedding_opensRange (R : Type u) [CommRing R] :
    (infinityChartEmbedding R).opensRange =
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R)
        (MvPolynomial.X (0 : Fin 2))
theorem

infinityChartEmbedding_preimage_linearSection

L86 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartEmbedding_preimage_linearSection
Documentation

The original integral section equation restricts to v-u*w on the infinity chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem infinityChartEmbedding_preimage_linearSection (u v : ℤ) :
    infinityChartEmbedding ℤ ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
          (linearSectionEquation u v) =
      PrimeSpectrum.basicOpen (Polynomial.C v - Polynomial.C u * Polynomial.X)
theorem

infinityChartEmbedding_linearSection_mem_iff

L100 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartEmbedding_linearSection_mem_iff
Documentation

Vanishing of the homogeneous section equation is vanishing of its actual chart polynomial.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem infinityChartEmbedding_linearSection_mem_iff
    (u v : ℤ) (q : PrimeSpectrum ℤ[X]) :
    linearSectionEquation u v ∈ (infinityChartEmbedding ℤ q).asHomogeneousIdeal ↔
      Polynomial.C v - Polynomial.C u * Polynomial.X ∈ q.asIdeal
def

infinityChartClosedPoint

L115 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartClosedPoint
Documentation

The prime of the infinity chart above the closed point of the local base.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def infinityChartClosedPoint (R : Type u) [CommRing R] [IsLocalRing R] :
    PrimeSpectrum R[X]
def

projectiveInfinityPoint

L120 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityPoint
Documentation

The corresponding actual point of the projective line.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def projectiveInfinityPoint (R : Type u) [CommRing R] [IsLocalRing R] :
    ProjectiveLine R
def

infinityChartStalkEquiv

L126 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartStalkEquiv
Documentation

At any prime of the infinity chart, the actual projective stalk is the localization of the polynomial ring at that prime.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · full declaration
def infinityChartStalkEquiv (R : Type u) [CommRing R]
    (q : Spec (CommRingCat.of R[X])) :
    let : q.asIdeal.IsPrime := q.isPrime
    (ProjectiveLine R).presheaf.stalk (infinityChartEmbedding R q) ≃+*
      Localization.AtPrime q.asIdeal := by
  intro hprime
  let e : (ProjectiveLine R).presheaf.stalk (infinityChartEmbedding R q) ≅
      (Spec (CommRingCat.of R[X])).presheaf.stalk q :=
    asIso ((infinityChartEmbedding R).stalkMap q)
  exact (e ≪≫ Spec.stalkIso (CommRingCat.of R[X]) q).commRingCatIsoToRingEquiv
def

infinityChartGermAt

L139 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartGermAt
Documentation

A polynomial gives a germ at any point of the infinity chart, using the actual structure-sheaf germ and the inverse stalk map of the open immersion.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def infinityChartGermAt (R : Type u) [CommRing R]
    (q : Spec (CommRingCat.of R[X])) :
    R[X] →+* (ProjectiveLine R).presheaf.stalk (infinityChartEmbedding R q)
theorem

infinityChartStalkEquiv_germAt

L149 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartStalkEquiv_germAt
Documentation

The actual chart germ becomes the localization map at the chosen prime.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · full declaration
theorem infinityChartStalkEquiv_germAt (R : Type u) [CommRing R]
    (q : Spec (CommRingCat.of R[X])) (f : R[X]) :
    let : q.asIdeal.IsPrime := q.isPrime
    infinityChartStalkEquiv R q (infinityChartGermAt R q f) =
      algebraMap R[X] (Localization.AtPrime q.asIdeal) f := by
  intro hprime
  let e : (ProjectiveLine R).presheaf.stalk (infinityChartEmbedding R q) ≅
      (Spec (CommRingCat.of R[X])).presheaf.stalk q :=
    asIso ((infinityChartEmbedding R).stalkMap q)
  let g : CommRingCat.of R[X] ⟶ (Spec (CommRingCat.of R[X])).presheaf.stalk q :=
    (Scheme.ΓSpecIso (CommRingCat.of R[X])).inv ≫
      (Spec (CommRingCat.of R[X])).presheaf.germ ⊤ q trivial
  have hcancel : e.hom (e.inv (g f)) = g f := CommRingCat.hom_inv_apply e (g f)
  have hspec : (Spec.stalkIso (CommRingCat.of R[X]) q).hom (g f) =
      algebraMap R[X] (Localization.AtPrime q.asIdeal) f := by
    have hbase : CommRingCat.ofHom (algebraMap R[X] (Localization.AtPrime q.asIdeal)) ≫
        (Spec.stalkIso (CommRingCat.of R[X]) q).inv = g :=
      Spec.algebraMap_stalkIso_inv (R := CommRingCat.of R[X]) q
    have hmap : g ≫ (Spec.stalkIso (CommRingCat.of R[X]) q).hom =
        CommRingCat.ofHom (algebraMap R[X] (Localization.AtPrime q.asIdeal)) := by
      rw [← hbase, Category.assoc, Iso.inv_hom_id, Category.comp_id]
    simpa only [ConcreteCategory.comp_apply, ConcreteCategory.hom_ofHom] using
      (ConcreteCategory.congr_hom hmap f)
  exact (congrArg (Spec.stalkIso (CommRingCat.of R[X]) q).hom hcancel).trans hspec
def

projectiveInfinityStalkEquiv

L175 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityStalkEquiv
Documentation

The projective stalk is the localization at the concrete infinity chart prime.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def projectiveInfinityStalkEquiv (R : Type u) [CommRing R] [IsLocalRing R] :
    (ProjectiveLine R).presheaf.stalk (projectiveInfinityPoint R) ≃+*
      InfinityChartLocalRing R
def

infinityChartGerm

L182 ↗
ShimizuYamaguchi26BranchedCoverings.infinityChartGerm
Documentation

A polynomial defines a projective local germ at the point above the closed point of the local base through the actual affine structure sheaf.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def infinityChartGerm (R : Type u) [CommRing R] [IsLocalRing R] :
    R[X] →+* (ProjectiveLine R).presheaf.stalk (projectiveInfinityPoint R)
theorem

projectiveInfinityStalkEquiv_germ

L187 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveInfinityStalkEquiv_germ
Documentation

The actual chart germ becomes the standard polynomial localization map.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem projectiveInfinityStalkEquiv_germ (R : Type u) [CommRing R] [IsLocalRing R]
    (f : R[X]) :
    projectiveInfinityStalkEquiv R (infinityChartGerm R f) =
      algebraMap R[X] (InfinityChartLocalRing R) f

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