Branched coverings of the projective line over the integers

Formalization of Ryoji Shimizu and Naganori Yamaguchi's On branched coverings of the projective line over the integers, using the numbering of arXiv v1. Numbered files contain the corresponding paper arguments; Arithmeti…

The determinant of two primitive integral coordinate pairs controls the intersection of their rational sections. This file proves its change-of-coordinates identities. The scheme-theoretic intersection multiplicity compa…

After moving their common reduction to zero, three rational sections have even numerators and odd denominators. Some pair has determinant divisible by four. The statement below is the coordinate calculation in Lemma 2.4;…

For a nonzero integer, the additive DVR valuation in ℤ(p) is its integer p-adic valuation. The comparison uses the inverse images of powers of the localized maximal ideal: membership in its nth power is exactly divisibil…

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…

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…

Taking spectra of the explicit quadratic algebra gives a finite etale, surjective morphism with integral, connected source. Its coordinate algebra is free of rank two. The parameter restrictions are precisely the arithme…

The discriminant in Proposition 2.5 of Shimizu--Yamaguchi has degree one. Its nonsquareness follows from the integer degree of rational functions: a nonzero square has even degree. This argument does not require a choice…

For an actual point of Projectivization ℚ (ℚ × ℚ), the coordinates are (1, 0) at infinity and the reduced numerator and positive denominator of the affine coordinate elsewhere. Their primitivity and their representation…

Primitive integral coordinate pairs have six normalized projective residue classes modulo four. Pairs in the same class have determinant divisible by four. Thus a finite family with no such collision has at most six memb…

The homogeneous core of the kernel of evaluation at (u,v) is a homogeneous prime ideal. A nonzero coordinate prevents this ideal from containing the irrelevant ideal, so it defines a point of the actual projective scheme…

The equation vT₀-uT₁ for a nonzero pair (u,v) has exactly the point constructed by homogeneous evaluation as its zero locus in the actual projective scheme. If v is nonzero, relevance forces the zero locus into the stand…

At the point of the section b over p, the actual kernel ideal of a section c becomes the unit ideal when p does not divide Delta(c,b). This follows from the previously computed actual intersection length. Thus every othe…

Swapping the homogeneous coordinates turns the standard affine chart into the chart T₀ ≠ 0. At the prime (maximalIdeal R, X), the open immersion identifies the stalk of the projective line with the prime localization of…

On the affine chart with coordinate w = T₁ / T₀, the equations of the section at infinity and a section given by a primitive pair (u,v) are w and v - uw. The affine intersection of these equations has coordinate ring R[w…

The point (p, X) in Spec ℤ[X] is defined by pulling the prime ideal (p) back along the constant-coefficient map. Its ideal is the inverse image of the infinity chart closed point after localizing the coefficient ring at…

The actual point of ℙ¹ℤ represented by (p,w) in the infinity chart has local ring ℤ[w](p,w). The chart stalk isomorphism and the coefficient localization comparison identify this ring with the local chart ring over ℤ(p),…

The concrete equations w and v-uw form a weakly regular sequence in ℤ[w] when v is nonzero: modulo w, multiplication by the second equation is multiplication by the nonzero integer v. When p divides v, both equations lie…

Bézout coefficients au+bv = 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 P…

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 th…

On the two polynomial charts, the section at infinity has equations X and 1. An integral projective coordinate change then transports its actual kernel ideal to that of any rational section.

When the first primitive coordinate is a unit in a reduced coefficient ring, its inverse times the second coordinate gives a concrete affine coordinate. Evaluation at this value, followed by the infinity chart of the int…

Pullback by the inverse of a scheme isomorphism agrees with pushforward by the isomorphism. Applied to reduced vanishing ideal sheaves, this identifies pullback with the vanishing ideal of the inverse image. The explicit…

The section constructed from a primitive integer pair has reduced source Spec ℤ. Its scheme-theoretic image therefore has the reduced induced structure on its closed image. The actual kernel ideal sheaf is consequently t…

The intersection ideal is the sum of the stalk ideals of the two actual closed section morphisms. On the infinity chart these ideals are generated by their primitive linear equations. If the second rational point is infi…

Consider the product of the actual kernel ideal sheaves of the infinity section and a primitive integral section (u,v). At the point (p,w), the stalk of this product is generated by w(v-uw). When v is nonzero and vp(v)=1…

The closed point of Spec ℤ defined by p maps under evaluation at zero in the polynomial chart to the prime (p, X). The actual integral section is the zero section followed by a coordinate swap and the inverse Bézout coor…

A primitive section has a reduced kernel ideal sheaf. On the infinity chart, its support is the zero locus of v-uw. Restriction to the open chart preserves radical ideals, so equality of these zero loci identifies the ac…

For a local coefficient ring R, the infinity chart point over its closed point has prime ideal (maximalIdeal R, X) in R[X]. Localizing at this actual ideal and quotienting by the two section equations (X, v-uX) gives the…

The infinity-chart equation of primitive integral coordinates (u,v) is v-uw. When u is nonzero, coprimality makes this polynomial irreducible, and unique factorization in ℤ[w] makes its principal ideal prime. When u is z…

The equations w and v-uw are sent to the stalk of the projective line through the genuine chart germ map. The chart stalk isomorphism carries their generated ideal to the localized polynomial intersection ideal. Conseque…

The primitive numerator and denominator of an actual rational projective point supply Bezout coefficients. These construct a section of the integral projective line, whose image is the homogeneous linear zero locus alrea…

The support is the actual homogeneous zero locus of the primitive equation vT₀-uT₁ in the integral projective line. Pulling it back along the coefficient morphism computes the same equation over the new coefficient ring.…

A common point of two homogeneous linear equations over a field forces the coordinate determinant to vanish: two explicit linear combinations put the determinant times both coordinates in its homogeneous prime ideal, and…

The degree-zero homogeneous localization of R[T₀,T₁] at T₁ is identified with R[t], with t mapping to T₀ / T₁. The inverse is constructed by evaluating the homogeneous coordinates at (t, 1); equality on coordinate ratios…

The homogeneous equation v T₀ - u T₁ restricts on the chart T₁ ≠ 0 to v t - u. Consequently the complement of its zero set and the section at infinity is isomorphic, as a scheme, to Spec ℤ[t, 1 / (v t - u)]. The comparis…

Evaluation at zero gives a morphism from Spec R to the standard affine chart of the projective line. The kernel of this evaluation is generated by the affine coordinate, so its affine image is its zero locus. The irrelev…

The corresponding Lean declaration is rationalSectionIntersectionlength. The integral Bezout coordinate isomorphism sends the second original section point over p to the infinity-chart point (p,w). Pullback carries the a…

The finite-boundary declaration is existstwolepadicValIntdeltainboundary. The support of a rational section is the actual homogeneous zero locus of vT₀-uT₁ in ℙ¹ℤ, using primitive integral coordinates of the rational pro…

The determinant-obstruction declaration is existssurjectivecyclicTwooffourdvdpairDeterminant. The connected quadratic cover constructed from an odd numerator and a nonzero denominator divisible by four gives a continuous…

Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, arXiv:2608.15057v1, Corollary 2.7, the case of at least seven boundary components. For a finite set A of ratio…