NYLL
Module

IntegralCoordinateChange.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralCoordinateChange
16 declarations indexed from sourceView source ↗

Module documentation

Integral changes of coordinates on the projective line

Bézout coefficients a*u+b*v = 1 give a homogeneous substitution with matrix [[a,b],[v,-u]]. Its inverse has matrix [[u,b],[v,-a]]. The two substitutions preserve degrees, and their compositions are the identity. Applying Proj.map therefore constructs an actual scheme automorphism of the integral projective line, rather than only an action on field-valued projective points.

The inverse image of the infinity chart is D₊(v*T₀-u*T₁). Restriction then identifies the complement of this equation with the affine line for every primitive pair (u,v). The transformed second equation has its determinant as the coefficient of T₀. Restriction identifies the common complement of the two equations with the spectrum of the corresponding affine localization, as needed in Proposition 2.5 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

The identification of the closed equation with the image of a section and the local intersection-multiplicity comparison are separate assertions.

Imports17
Imported by11

Declarations

def

bezoutCoordinateSubstitution

L60 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution
Documentation

The degree-preserving substitution (T₀,T₁) ↦ (a*T₀+b*T₁,v*T₀-u*T₁).

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · full declaration
def bezoutCoordinateSubstitution (u v a b : R) :
    MvPolynomial.homogeneousSubmodule (Fin 2) R →+*ᵍ
      MvPolynomial.homogeneousSubmodule (Fin 2) R where
  __ := MvPolynomial.eval₂Hom MvPolynomial.C (fun i : Fin 2 =>
    if i = 0 then MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1
    else linearSectionEquation u v)
  map_mem {i} {p} hp := by
    apply (MvPolynomial.mem_homogeneousSubmodule i _).mpr
    have h := (MvPolynomial.mem_homogeneousSubmodule i p).mp hp
    have hcoordinates : ∀ j : Fin 2,
        (if j = 0 then MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1
          else linearSectionEquation u v).IsHomogeneous 1 := by
      intro j
      by_cases hj : j = 0
      · rw [ite_eq_left hj]
        exact (MvPolynomial.isHomogeneous_C_mul_X a (0 : Fin 2)).add
          (MvPolynomial.isHomogeneous_C_mul_X b (1 : Fin 2))
      · rw [ite_eq_right hj]
        exact (MvPolynomial.mem_homogeneousSubmodule 1 _).mp
          (linearSectionEquation_mem_one u v)
    simpa only [MvPolynomial.coe_eval₂Hom, one_mul] using
      h.eval₂ MvPolynomial.C _ (MvPolynomial.isHomogeneous_C _) hcoordinates
theorem

bezoutCoordinateSubstitution_C

L84 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution_C
Documentation

The substitution fixes the coefficient ring.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem bezoutCoordinateSubstitution_C (u v a b r : R) :
    bezoutCoordinateSubstitution u v a b (MvPolynomial.C r) = MvPolynomial.C r
theorem

bezoutCoordinateSubstitution_X_zero

L89 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution_X_zero
Documentation

The first coordinate of the homogeneous substitution.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem bezoutCoordinateSubstitution_X_zero (u v a b : R) :
    bezoutCoordinateSubstitution u v a b (MvPolynomial.X 0) =
      MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1
theorem

bezoutCoordinateSubstitution_X_one

L96 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution_X_one
Documentation

The second coordinate is the primitive section equation.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem bezoutCoordinateSubstitution_X_one (u v a b : R) :
    bezoutCoordinateSubstitution u v a b (MvPolynomial.X 1) = linearSectionEquation u v
theorem

bezoutCoordinateSubstitution_comp

L102 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution_comp
Documentation

Bézout's identity makes the two explicit homogeneous substitutions inverse.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem bezoutCoordinateSubstitution_comp (u v a b : R) (hab : a * u + b * v = 1) :
    (bezoutCoordinateSubstitution u v a b).comp (bezoutCoordinateSubstitution a v u b) =
      GradedRingHom.id (MvPolynomial.homogeneousSubmodule (Fin 2) R)
theorem

bezoutCoordinateSubstitution_irrelevant

L146 ↗
ShimizuYamaguchi26BranchedCoverings.bezoutCoordinateSubstitution_irrelevant
Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem bezoutCoordinateSubstitution_irrelevant
    (u v a b : R) (hab : a * u + b * v = 1) :
    HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin 2) R) ≤
      (HomogeneousIdeal.irrelevant (MvPolynomial.homogeneousSubmodule (Fin 2) R)).map
        (bezoutCoordinateSubstitution u v a b)
def

integralCoordinateChange

L165 ↗
ShimizuYamaguchi26BranchedCoverings.integralCoordinateChange
Documentation

The projective scheme automorphism over the base ring sending the equation of (u,v) to infinity. In particular this gives the integral coordinate change over ℤ.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · full declaration
def integralCoordinateChange (u v a b : R) (hab : a * u + b * v = 1) :
    ProjectiveLine R ≅ ProjectiveLine R where
  hom := Proj.map (bezoutCoordinateSubstitution u v a b)
    (bezoutCoordinateSubstitution_irrelevant u v a b hab)
  inv := Proj.map (bezoutCoordinateSubstitution a v u b)
    (bezoutCoordinateSubstitution_irrelevant a v u b (by
      rw [mul_comm u a]
      exact hab))
  hom_inv_id := by
    rw [← Proj.map_comp]
    simp only [bezoutCoordinateSubstitution_comp u v a b hab, Proj.map_id]
  inv_hom_id := by
    rw [← Proj.map_comp]
    simp only [bezoutCoordinateSubstitution_comp a v u b (by
      rw [mul_comm u a]
      exact hab), Proj.map_id]
def

projectiveCoordinateSwap

L183 ↗
ShimizuYamaguchi26BranchedCoverings.projectiveCoordinateSwap
Documentation

The projective automorphism exchanging the two homogeneous coordinates.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
def projectiveCoordinateSwap (R : Type u) [CommRing R] :
    ProjectiveLine R ≅ ProjectiveLine R
theorem

integralCoordinateChange_preimage_infinity

L189 ↗
ShimizuYamaguchi26BranchedCoverings.integralCoordinateChange_preimage_infinity
Documentation

The primitive linear equation is the inverse image of the infinity equation.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem integralCoordinateChange_preimage_infinity
    (u v a b : R) (hab : a * u + b * v = 1) :
    (integralCoordinateChange u v a b hab).hom ⁻¹ᵁ infinityComplement R =
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) R) (linearSectionEquation u v)
theorem

inverseCoordinateSubstitution_linearSection

L198 ↗
ShimizuYamaguchi26BranchedCoverings.inverseCoordinateSubstitution_linearSection
Documentation

The coefficient of T₀ in the transformed second equation is the original determinant.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem inverseCoordinateSubstitution_linearSection (u v a b u' v' : ℤ) :
    bezoutCoordinateSubstitution a v u b (linearSectionEquation u' v') =
      linearSectionEquation (-(a * u' + b * v')) (coordinateDeterminant u v u' v')
theorem

integralCoordinateChange_inv_preimage_linearSection

L207 ↗
ShimizuYamaguchi26BranchedCoverings.integralCoordinateChange_inv_preimage_linearSection
Documentation

A second section equation transforms with determinant denominator under the inverse map.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem integralCoordinateChange_inv_preimage_linearSection
    (u v a b u' v' : ℤ) (hab : a * u + b * v = 1) :
    (integralCoordinateChange u v a b hab).inv ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ) (linearSectionEquation u' v') =
      Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        (linearSectionEquation (-(a * u' + b * v')) (coordinateDeterminant u v u' v'))
theorem

integralCoordinateChange_inv_preimage_firstSection

L218 ↗
ShimizuYamaguchi26BranchedCoverings.integralCoordinateChange_inv_preimage_firstSection
Documentation

In the new coordinates, the first equation becomes the infinity equation.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem integralCoordinateChange_inv_preimage_firstSection
    (u v a b : ℤ) (hab : a * u + b * v = 1) :
    (integralCoordinateChange u v a b hab).inv ⁻¹ᵁ
        Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ) (linearSectionEquation u v) =
      infinityComplement ℤ
def

integralPairComplement

L227 ↗
ShimizuYamaguchi26BranchedCoverings.integralPairComplement
Documentation

The common nonvanishing open of two integral homogeneous linear equations.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
def integralPairComplement (u v u' v' : ℤ) : (ProjectiveLine ℤ).Opens
theorem

integralCoordinateChange_inv_preimage_pairComplement

L232 ↗
ShimizuYamaguchi26BranchedCoverings.integralCoordinateChange_inv_preimage_pairComplement
Documentation

The two-equation complement pulls back to the explicit standard affine complement.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem integralCoordinateChange_inv_preimage_pairComplement
    (u v a b u' v' : ℤ) (hab : a * u + b * v = 1) :
    (integralCoordinateChange u v a b hab).inv ⁻¹ᵁ integralPairComplement u v u' v' =
      twoSectionComplement (-(a * u' + b * v')) (coordinateDeterminant u v u' v')
def

integralPairComplementIso

L246 ↗
ShimizuYamaguchi26BranchedCoverings.integralPairComplementIso
Documentation

A pair of equations with primitive first coordinates has an explicit affine localization model.

The new denominator coefficient is the determinant of the original coordinate pairs. No affine or projective comparison is assumed: the isomorphism restricts the constructed projective automorphism and then uses the standard chart comparison.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
def integralPairComplementIso (u v a b u' v' : ℤ) (hab : a * u + b * v = 1) :
    (integralPairComplement u v u' v').toScheme ≅
      Spec (CommRingCat.of (TwoSectionCoordinateRing (-(a * u' + b * v'))
        (coordinateDeterminant u v u' v')))
theorem

nonempty_primitiveSectionComplementIso

L257 ↗
ShimizuYamaguchi26BranchedCoverings.nonempty_primitiveSectionComplementIso
Documentation

The complement of any primitive integral linear equation is an affine line.

Source context 6 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
variable {R : Type u} [CommRing R]
Lean source · statement
theorem nonempty_primitiveSectionComplementIso
    (u v : ℤ) (huv : IsCoprime u v) :
    Nonempty ((Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
      (linearSectionEquation u v)).toScheme ≅ Spec (CommRingCat.of (Polynomial ℤ)))

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