NYLL
Module

TwoSectionComplement.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.TwoSectionComplement
11 declarations indexed from sourceView source ↗

Module documentation

The complement of two linear equations in the integral projective line

The homogeneous equation v * T₀ - u * T₁ restricts on the chart T₁ ≠ 0 to v * t - u. Consequently the complement of its zero set and the section at infinity is isomorphic, as a scheme, to Spec ℤ[t, 1 / (v * t - u)]. The comparison is constructed from open immersions with the same image.

For primitive (u,v), the first equation is the rational section considered in Proposition 2.5 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The scheme comparison proved here applies without the primitivity assumption; identifying the closed subscheme with the corresponding section is a separate assertion. IntegralCoordinateChange extends this comparison to pairs of equations with arbitrary primitive first coordinates.

Imports10
Imported by16

Declarations

def

linearSectionEquation

L47 ↗
ShimizuYamaguchi26BranchedCoverings.linearSectionEquation
Documentation

The homogeneous linear equation of the section with coordinates (u,v).

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def linearSectionEquation {R : Type u} [CommRing R] (u v : R) : MvPolynomial (Fin 2) R
theorem

linearSectionEquation_mem_one

L51 ↗
ShimizuYamaguchi26BranchedCoverings.linearSectionEquation_mem_one
Documentation

The section equation is homogeneous of degree one.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem linearSectionEquation_mem_one {R : Type u} [CommRing R] (u v : R) :
    linearSectionEquation u v ∈ MvPolynomial.homogeneousSubmodule (Fin 2) R 1
theorem

linearSectionEquation_dehomogenize

L58 ↗
ShimizuYamaguchi26BranchedCoverings.linearSectionEquation_dehomogenize
Documentation

Dividing the section equation by T₁ gives its affine linear expression.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem linearSectionEquation_dehomogenize {R : Type u} [CommRing R] (u v : R) :
    Away.isLocalizationElem (ProjSpace.X_mem_one R 1 (1 : Fin 2))
      (linearSectionEquation_mem_one u v) =
        algebraMap R (StandardChartRing R) v * ProjSpace.ratio R 1 1 0 -
          algebraMap R (StandardChartRing R) u
theorem

standardChartEquiv_linearSectionEquation

L73 ↗
ShimizuYamaguchi26BranchedCoverings.standardChartEquiv_linearSectionEquation
Documentation

The chart isomorphism sends v*t-u to the actual homogeneous localization element.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem standardChartEquiv_linearSectionEquation {R : Type u} [CommRing R] (u v : R) :
    standardChartEquiv R (Polynomial.C v * Polynomial.X - Polynomial.C u) =
      Away.isLocalizationElem (ProjSpace.X_mem_one R 1 (1 : Fin 2))
        (linearSectionEquation_mem_one u v)
theorem

standardChartEmbedding_preimage_linearSection

L82 ↗
ShimizuYamaguchi26BranchedCoverings.standardChartEmbedding_preimage_linearSection
Documentation

The nonvanishing open of the homogeneous section equation pulls back to D(v*t-u).

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem standardChartEmbedding_preimage_linearSection {R : Type u} [CommRing R] (u v : R) :
    standardChartEmbedding R ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (linearSectionEquation u v) =
      PrimeSpectrum.basicOpen (Polynomial.C v * Polynomial.X - Polynomial.C u)
def

twoSectionComplement

L102 ↗
ShimizuYamaguchi26BranchedCoverings.twoSectionComplement
Documentation

The open complement of T₁ = 0 and v*T₀-u*T₁ = 0 in ℙ¹_ℤ.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def twoSectionComplement (u v : ℤ) : (ProjectiveLine ℤ).Opens
def

twoSectionComplementEmbedding

L107 ↗
ShimizuYamaguchi26BranchedCoverings.twoSectionComplementEmbedding
Documentation

The affine localization embeds into the projective line by its standard coordinate chart.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def twoSectionComplementEmbedding (u v : ℤ) :
    Spec (CommRingCat.of (TwoSectionCoordinateRing u v)) ⟶ ProjectiveLine ℤ
instance

(anonymous instance)

L112 ↗
Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
instance (u v : ℤ) : IsOpenImmersion (twoSectionComplementEmbedding u v)
theorem

twoSectionComplementEmbedding_opensRange

L117 ↗
ShimizuYamaguchi26BranchedCoverings.twoSectionComplementEmbedding_opensRange
Documentation

The affine localization has exactly the required two-equation complement as its image.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem twoSectionComplementEmbedding_opensRange (u v : ℤ) :
    (twoSectionComplementEmbedding u v).opensRange = twoSectionComplement u v
def

twoSectionComplementIso

L128 ↗
ShimizuYamaguchi26BranchedCoverings.twoSectionComplementIso
Documentation

The actual projective complement is the spectrum of ℤ[t, 1/(v*t-u)].

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def twoSectionComplementIso (u v : ℤ) :
    (twoSectionComplement u v).toScheme ≅ Spec (CommRingCat.of (TwoSectionCoordinateRing u v))
theorem

twoSectionComplementIso_hom_comp_embedding

L136 ↗
ShimizuYamaguchi26BranchedCoverings.twoSectionComplementIso_hom_comp_embedding
Documentation

The affine comparison commutes with the maps to the projective line.

Source context 6 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry HomogeneousLocalization
open scoped Polynomial
namespace ShimizuYamaguchi26BranchedCoverings
universe u
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem twoSectionComplementIso_hom_comp_embedding (u v : ℤ) :
    (twoSectionComplementIso u v).hom ≫ twoSectionComplementEmbedding u v =
      (twoSectionComplement u v).ι

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