For an odd integer u and an integer v divisible by four, the proof constructs an integral polynomial c(t) and a sign ε with 1 - 4 * c(t) = ε * (v * t - u). Thus adjoining a root of X² + X + c(t) over ℤ[t, 1 / (v * t - u)] gives an actual finite free etale algebra. For nonzero v, its rank is two.
The proof derives invertibility of the derivative from the equation of its adjoined root, then uses the existing etale criterion. Connectedness of this cover and its comparison with the complement of two projective-line sections are not asserted here.
Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Proposition 2.5.
The monic quadratic equation used in the dyadic construction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsdef quadraticPolynomial {R : Type*} [CommRing R] (c : R) : R[X]The quadratic equation is monic over any commutative coefficient ring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticPolynomial_monic {R : Type*} [CommRing R] (c : R) :
(quadraticPolynomial c).MonicThe derivative square is exactly the image of the quadratic discriminant.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticPolynomial_derivative_square {R : Type*} [CommRing R] (c : R) :
(aeval (AdjoinRoot.root (quadraticPolynomial c))
(quadraticPolynomial c).derivative) ^ 2 =
algebraMap R (AdjoinRoot (quadraticPolynomial c)) (1 - 4 * c)Invertibility of the discriminant makes the quadratic algebra etale. The derivative condition is proved from the actual adjoined-root equation.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticPolynomial_etale {R : Type*} [CommRing R] (c : R)
(hdisc : IsUnit (1 - 4 * c)) :
Algebra.Etale R (AdjoinRoot (quadraticPolynomial c))The underlying free quadratic algebra has rank two over a nonzero ring.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticPolynomial_finrank {R : Type*} [CommRing R] [Nontrivial R] (c : R) :
Module.finrank R (AdjoinRoot (quadraticPolynomial c)) = 2The equation removed from the affine chart of the two-section complement.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsdef boundaryPolynomial (u v : ℤ) : ℤ[X]The integral constant term in the quadratic covering equation.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsdef quadraticConstantTerm (u v ε : ℤ) : ℤ[X]The explicit integral constant term has the required discriminant identity.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticConstantTerm_discriminant (u v ε : ℤ)
(hu : (4 : ℤ) ∣ 1 + ε * u) (hv : (4 : ℤ) ∣ v) :
1 - 4 * quadraticConstantTerm u v ε = C ε * boundaryPolynomial u vThe affine coordinate ring obtained by removing v * t - u = 0.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsabbrev TwoSectionCoordinateRing (u v : ℤ) : TypeThe actual discriminant is a unit after removing the boundary equation. This uses the constructed integral constant term and either integral sign.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticConstantTerm_discriminant_isUnit (u v ε : ℤ)
(hε : ε = 1 ∨ ε = -1) (hεu : (4 : ℤ) ∣ 1 + ε * u)
(hv : (4 : ℤ) ∣ v) :
IsUnit (1 - 4 * algebraMap ℤ[X] (TwoSectionCoordinateRing u v)
(quadraticConstantTerm u v ε))A nonzero denominator makes the boundary equation a nonzero polynomial.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem boundaryPolynomial_ne_zero (u v : ℤ) (hv : v ≠ 0) :
boundaryPolynomial u v ≠ 0The algebraic construction in Proposition 2.5: over the stated affine localization there is a finite free etale quadratic algebra of rank two.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem exists_finite_etale_quadratic_algebra (u v : ℤ)
(hu : Odd u) (hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0) :
∃ (ε : ℤ) (c : ℤ[X]), (ε = 1 ∨ ε = -1) ∧
1 - 4 * c = C ε * boundaryPolynomial u v ∧
let R : Type := TwoSectionCoordinateRing u v
let f : R[X] := quadraticPolynomial (algebraMap ℤ[X] R c)
Algebra.Etale R (AdjoinRoot f) ∧ Module.Finite R (AdjoinRoot f) ∧
Module.Free R (AdjoinRoot f) ∧ Module.finrank R (AdjoinRoot f) = 2 := by
obtain ⟨ε, hε, hεu⟩ := exists_sign_four_dvd_one_add u hu
let c : ℤ[X] := quadraticConstantTerm u v ε
have hdisc : 1 - 4 * c = C ε * boundaryPolynomial u v :=
quadraticConstantTerm_discriminant u v ε hεu hv
refine ⟨ε, c, hε, hdisc, ?_⟩
let R : Type := TwoSectionCoordinateRing u v
let : IsDomain R := Localization.Away.isDomain (boundaryPolynomial_ne_zero u v hv0)
let cR : R := algebraMap ℤ[X] R c
have hunit : IsUnit (1 - 4 * cR) :=
quadraticConstantTerm_discriminant_isUnit u v ε hε hεu hv
exact ⟨quadraticPolynomial_etale cR hunit,
(quadraticPolynomial_monic cR).finite_adjoinRoot,
(quadraticPolynomial_monic cR).free_adjoinRoot,
quadraticPolynomial_finrank cR⟩