The discriminant of the quadratic equation in Proposition 2.5 is the nonconstant linear polynomial ε * (v * t - u). Its image in ℚ(t) is not a square, by degree. A root over ℤ[t, 1 / (v * t - u)] would make this image a square. Thus the quadratic is irreducible. Unique factorization in this localization then proves that its adjoined-root algebra is an integral domain.
The argument uses the explicit constant term from QuadraticCover; neither irreducibility nor nonsquareness is an input assumption.
Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Proposition 2.5.
The usual inclusion of integral polynomials into the rational function field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsdef integerPolynomialToRatFunc : ℤ[X] →+* RatFunc ℚThe nonconstant signed boundary equation cannot be a square in ℚ(t).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem signedBoundary_ne_square (u v ε : ℤ) (hε : ε ≠ 0) (hv : v ≠ 0)
(r : RatFunc ℚ) :
integerPolynomialToRatFunc (C ε * boundaryPolynomial u v) ≠ r ^ 2The canonical map from the affine coordinate ring to ℚ(t).
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsdef twoSectionToRatFunc (u v : ℤ) (hv : v ≠ 0) :
TwoSectionCoordinateRing u v →+* RatFunc ℚThe map from the localization extends the original polynomial inclusion.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem twoSectionToRatFunc_algebraMap (u v : ℤ) (hv : v ≠ 0) (p : ℤ[X]) :
twoSectionToRatFunc u v hv (algebraMap ℤ[X] (TwoSectionCoordinateRing u v) p) =
integerPolynomialToRatFunc pThe actual quadratic polynomial of Proposition 2.5 is irreducible over its affine coordinate ring. The divisibility hypotheses produce its integral coefficients and the discriminant identity.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem quadraticCoverPolynomial_irreducible (u v ε : ℤ)
(hε : ε = 1 ∨ ε = -1) (hεu : (4 : ℤ) ∣ 1 + ε * u)
(hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0) :
Irreducible (quadraticPolynomial
(algebraMap ℤ[X] (TwoSectionCoordinateRing u v) (quadraticConstantTerm u v ε)))The quadratic covering algebra on the complement of the two sections.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringsabbrev TwoSectionQuadraticAlgebra (u v ε : ℤ) : TypeThe explicit quadratic covering algebra is an integral domain.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace ShimizuYamaguchi26BranchedCoveringstheorem twoSectionQuadraticAlgebra_isDomain (u v ε : ℤ)
(hε : ε = 1 ∨ ε = -1) (hεu : (4 : ℤ) ∣ 1 + ε * u)
(hv : (4 : ℤ) ∣ v) (hv0 : v ≠ 0) :
IsDomain (TwoSectionQuadraticAlgebra u v ε)