NYLL
Module

IntegralSection.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.IntegralSection
5 declarations indexed from sourceView source ↗

Module documentation

Integral sections with primitive homogeneous coordinates

Bézout coefficients for an integer pair construct an actual section of the projective line over Spec ℤ. The zero section of the affine chart is first sent to infinity by exchanging coordinates, and then transported by the inverse Bézout coordinate change. The resulting section is a closed immersion, and its image is exactly the projective zero locus of v*T₀-u*T₁.

This supplies the integral section underlying the first assertion of Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers.

Imports16
Imported by10

Declarations

theorem

range_zeroSection_comp_swap

L46 ↗
ShimizuYamaguchi26BranchedCoverings.range_zeroSection_comp_swap
Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem range_zeroSection_comp_swap :
    Set.range (zeroSection ℤ ≫ (projectiveCoordinateSwap ℤ).hom) =
      (infinityComplement ℤ : Set (ProjectiveLine ℤ))ᶜ
def

integralSection

L71 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection
Documentation

The actual integral section associated to coordinates and Bézout coefficients.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
def integralSection (u v a b : ℤ) (hab : a * u + b * v = 1) :
    Spec (CommRingCat.of ℤ) ⟶ ProjectiveLine ℤ
theorem

integralSection_comp_π

L77 ↗
ShimizuYamaguchi26BranchedCoverings.integralSection_comp_π
Documentation

The constructed morphism is a section of the integral projective line.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem integralSection_comp_π (u v a b : ℤ) (hab : a * u + b * v = 1) :
    integralSection u v a b hab ≫ ProjSpace.π ℤ 1 =
      𝟙 (Spec (CommRingCat.of ℤ))
instance

(anonymous instance)

L83 ↗
Documentation

Every integral section constructed from a primitive coordinate pair is closed.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
instance (u v a b : ℤ) (hab : a * u + b * v = 1) :
    IsClosedImmersion (integralSection u v a b hab)
theorem

range_integralSection

L91 ↗
ShimizuYamaguchi26BranchedCoverings.range_integralSection
Documentation

The image of the actual integral section is its homogeneous linear zero locus.

Source context 4 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
theorem range_integralSection (u v a b : ℤ) (hab : a * u + b * v = 1) :
    Set.range (integralSection u v a b hab) =
      ProjectiveSpectrum.zeroLocus (MvPolynomial.homogeneousSubmodule (Fin 2) ℤ)
        {linearSectionEquation u v}

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