Module

StandardAffineChart.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.StandardAffineChart

10 declarations indexed from sourceView source ↗

Module documentation

The affine coordinate chart of the projective line

The degree-zero homogeneous localization of R[T₀,T₁] at T₁ is identified with R[t], with t mapping to T₀ / T₁. The inverse is constructed by evaluating the homogeneous coordinates at (t, 1); equality on coordinate ratios proves that the maps are inverse. Taking spectra gives the actual scheme chart, over an arbitrary commutative base ring.

This chart is used in the proof of Proposition 2.5 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports8

Nyll.SchemeTheory.ProjectiveSpace.Basic
Nyll.AlgebraicCurves.Geometry.Projective.ProjSpace_exists_algHom_away_apply_ratio_eq
Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.Tactic.FinCases

Imported by26

abbrev

ProjectiveLine

L41 ↗

ShimizuYamaguchi26BranchedCoverings.ProjectiveLine

Documentation

The projective line as the projective spectrum of a graded polynomial ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

abbrev ProjectiveLine (R : Type u) [CommRing R] : Scheme.{u}

abbrev

StandardChartRing

L45 ↗

ShimizuYamaguchi26BranchedCoverings.StandardChartRing

Documentation

The homogeneous coordinate ring of the chart T₁ ≠ 0.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

abbrev StandardChartRing (R : Type u) [CommRing R] : Type u

def

infinityComplement

L50 ↗

ShimizuYamaguchi26BranchedCoverings.infinityComplement

Documentation

The complement of the section at infinity, defined as a genuine scheme open.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

def infinityComplement (R : Type u) [CommRing R] : (ProjectiveLine R).Opens

theorem

standardChart_aeval_bijective

L54 ↗

ShimizuYamaguchi26BranchedCoverings.standardChart_aeval_bijective

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem standardChart_aeval_bijective (R : Type u) [CommRing R] :
    Function.Bijective (Polynomial.aeval (ProjSpace.ratio R 1 1 0) :
      Polynomial R →ₐ[R] StandardChartRing R)

def

standardChartEquiv

L84 ↗

ShimizuYamaguchi26BranchedCoverings.standardChartEquiv

Documentation

The standard chart ring is the polynomial algebra in the ratio T₀ / T₁.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

def standardChartEquiv (R : Type u) [CommRing R] :
    Polynomial R ≃ₐ[R] StandardChartRing R

theorem

standardChartEquiv_X

L90 ↗

ShimizuYamaguchi26BranchedCoverings.standardChartEquiv_X

Documentation

The affine coordinate maps to the homogeneous coordinate ratio.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem standardChartEquiv_X (R : Type u) [CommRing R] :
    standardChartEquiv R Polynomial.X = ProjSpace.ratio R 1 1 0

def

standardAffineChartIso

L95 ↗

ShimizuYamaguchi26BranchedCoverings.standardAffineChartIso

Documentation

The standard chart is the spectrum of a one-variable polynomial ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

def standardAffineChartIso (R : Type u) [CommRing R] :
    (infinityComplement R).toScheme ≅ Spec (CommRingCat.of (Polynomial R))

def

standardChartEmbedding

L102 ↗

ShimizuYamaguchi26BranchedCoverings.standardChartEmbedding

Documentation

The usual affine chart as a morphism into the actual projective line.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

def standardChartEmbedding (R : Type u) [CommRing R] :
    Spec (CommRingCat.of (Polynomial R)) ⟶ ProjectiveLine R

instance

(anonymous instance)

L108 ↗

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

instance (R : Type u) [CommRing R] : IsOpenImmersion (standardChartEmbedding R)

theorem

standardChartEmbedding_opensRange

L113 ↗

ShimizuYamaguchi26BranchedCoverings.standardChartEmbedding_opensRange

Documentation

The image of the affine chart is exactly the complement of infinity.

Source context 5 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra

Lean source · statement

theorem standardChartEmbedding_opensRange (R : Type u) [CommRing R] :
    (standardChartEmbedding R).opensRange = infinityComplement R

Module documentation

The affine coordinate chart of the projective line

Declarations