NYLL
Module

Theorem2Dot5QuadraticQuotient.lean

Nyll.ShimizuYamaguchi26BranchedCoverings.Theorem2Dot5QuadraticQuotient
4 declarations indexed from sourceView source ↗

Module documentation

Proposition 2.5: the quadratic quotient construction

The determinant-obstruction declaration is exists_surjective_cyclicTwo_of_four_dvd_pairDeterminant.

The connected quadratic cover constructed from an odd numerator and a nonzero denominator divisible by four gives a continuous quotient of order two of the fundamental group of Spec ℤ[t, 1/(v*t-u)], at every geometric point. The degree condition is obtained from the actual free coordinate algebra, via the rank of the affine scheme morphism.

This supplies the affine quotient construction in Proposition 2.5 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The actual standard-chart comparison transports this quotient to every open subscheme of the projective complement of T₁ = 0 and v*T₀-u*T₁ = 0. The explicit integral change of coordinates also gives the quotient for any two primitive equations with nonzero determinant divisible by four. Identifying their closed loci as section images and comparing normal crossings remain separate geometric assertions.

Imports29
Imported by2

Declarations

theorem

exists_surjective_cyclicTwo_twoSectionCoordinateRing

L69 ↗
ShimizuYamaguchi26BranchedCoverings.exists_surjective_cyclicTwo_twoSectionCoordinateRing
Documentation

The explicit dyadic affine complement has a continuous cyclic quotient of order two. The finite etale cover and its degree are constructed from the arithmetic hypotheses, rather than supplied as inputs.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem exists_surjective_cyclicTwo_twoSectionCoordinateRing
    (u v : ℤ) (hu : Odd u) (hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0)
    {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ Spec (.of (TwoSectionCoordinateRing u v))) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ
theorem

exists_surjective_cyclicTwo_of_openImmersion_twoSectionCoordinateRing

L98 ↗
ShimizuYamaguchi26BranchedCoverings.exists_surjective_cyclicTwo_of_openImmersion_twoSectionCoordinateRing
Documentation

Removing further closed subsets preserves the constructed quotient of order two. The source is any open subscheme of the actual affine complement; its geometric point supplies nonemptiness. This is the restriction step needed when the original divisor has additional components.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem exists_surjective_cyclicTwo_of_openImmersion_twoSectionCoordinateRing
    (u v : ℤ) (hu : Odd u) (hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0)
    {U : Scheme.{0}} (j : U ⟶ Spec (.of (TwoSectionCoordinateRing u v)))
    [IsOpenImmersion j] {Ω : Type} [Field Ω] [IsSepClosed Ω]
    (ξ : Spec (.of Ω) ⟶ U) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ
theorem

exists_surjective_cyclicTwo_of_le_twoSectionComplement

L116 ↗
ShimizuYamaguchi26BranchedCoverings.exists_surjective_cyclicTwo_of_le_twoSectionComplement
Documentation

Every open contained in the two-section projective complement has a continuous quotient of order two. The map into the affine localization is constructed from the actual open inclusion and standard-chart isomorphism; no comparison map or quotient is supplied as an assumption.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem exists_surjective_cyclicTwo_of_le_twoSectionComplement
    (u v : ℤ) (hu : Odd u) (hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0)
    (U : (ProjectiveLine ℤ).Opens) (hU : U ≤ twoSectionComplement u v)
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ
theorem

exists_surjective_cyclicTwo_of_four_dvd_pairDeterminant

L134 ↗
ShimizuYamaguchi26BranchedCoverings.exists_surjective_cyclicTwo_of_four_dvd_pairDeterminant
Documentation

Two primitive integral equations with nonzero determinant divisible by four give a continuous cyclic quotient of order two on every open inside their common complement. The odd normalized numerator, coordinate change, and quadratic cover are all constructed from the original primitive pairs.

This is the determinant-obstruction case of Proposition 2.5. Comparing this condition with failure of normal crossings is a separate geometric step.

Source context 3 commands

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

noncomputable section
open CategoryTheory AlgebraicGeometry
namespace ShimizuYamaguchi26BranchedCoverings
Lean source · statement
theorem exists_surjective_cyclicTwo_of_four_dvd_pairDeterminant
    (u v u' v' : ℤ) (huv : IsCoprime u v) (huv' : IsCoprime u' v')
    (hfour : (4 : ℤ) ∣ coordinateDeterminant u v u' v')
    (hne : coordinateDeterminant u v u' v' ≠ 0)
    (U : (ProjectiveLine ℤ).Opens) (hU : U ≤ integralPairComplement u v u' v')
    {Ω : Type} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ U.toScheme) :
    ∃ φ : π₁ᵉᵗ(ξ) →ₜ* Multiplicative (ZMod 2), Function.Surjective φ

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