The infinity-chart equation of primitive integral coordinates (u,v) is v-u*w. When u is nonzero, coprimality makes this polynomial irreducible, and unique factorization in ℤ[w] makes its principal ideal prime. When u is zero, v is a unit and the ideal is the unit ideal.
Thus the equation ideal is radical in both cases. Primitive coordinates of distinct projective points give relatively prime equations, so the intersection of a finite family of these ideals equals their product. These are the algebraic steps needed to pass from the closed support of the actual integral sections to their scheme-theoretic equation ideals in Lemma 2.3 of Shimizu and Yamaguchi, On branched coverings of the projective line over the integers.
The principal ideal of the section equation in the integral infinity chart.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringsdef infinitySectionIdeal (u v : ℤ) : Ideal ℤ[X]A primitive nonconstant section equation generates a prime ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringstheorem infinitySectionIdeal_isPrime (u v : ℤ) (hu : u ≠ 0)
(huv : IsCoprime u v) : (infinitySectionIdeal u v).IsPrimeA primitive section equation has no common nonunit factor with the equation of a different projective point. Only the first coordinate pair must be primitive.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringstheorem infinitySectionEquations_isRelPrime (u v u' v' : ℤ)
(huv : IsCoprime u v) (hdet : coordinateDeterminant u v u' v' ≠ 0) :
IsRelPrime (Polynomial.C v - Polynomial.C u * Polynomial.X)
(Polynomial.C v' - Polynomial.C u' * Polynomial.X)For finitely many distinct primitive sections, the intersection of their infinity-chart equation ideals equals the product of those ideals.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringstheorem infinitySectionIdeal_finset_inf_eq_prod {ι : Type*} (s : Finset ι)
(u v : ι → ℤ) (hprimitive : ∀ i ∈ s, IsCoprime (u i) (v i))
(hdet : ∀ i ∈ s, ∀ j ∈ s, i ≠ j →
coordinateDeterminant (u i) (v i) (u j) (v j) ≠ 0) :
(s.inf fun i => infinitySectionIdeal (u i) (v i)) =
∏ i ∈ s, infinitySectionIdeal (u i) (v i) := by
let f : ι → ℤ[X] := fun i => Polynomial.C (v i) - Polynomial.C (u i) * Polynomial.X
have hrel : (s : Set ι).Pairwise (fun i j => IsRelPrime (f i) (f j)) := by
intro i hi j hj hij
exact infinitySectionEquations_isRelPrime (u i) (v i) (u j) (v j)
(hprimitive i hi) (hdet i hi j hj hij)
change (s.inf fun i => Ideal.span {f i}) = ∏ i ∈ s, Ideal.span {f i}
rw [Ideal.prod_span_singleton]
ext z
simp only [Submodule.mem_finsetInf, Ideal.mem_span_singleton]
exact ⟨Finset.prod_dvd_of_isRelPrime hrel,
fun hz i hi => (Finset.dvd_prod_of_mem f hi).trans hz⟩The section equation ideal is reduced for every primitive coordinate pair.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringstheorem infinitySectionIdeal_isRadical (u v : ℤ) (huv : IsCoprime u v) :
(infinitySectionIdeal u v).IsRadicalThe vanishing ideal of the primitive equation's zero locus is the equation ideal itself.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Polynomial BigOperators
namespace ShimizuYamaguchi26BranchedCoveringstheorem vanishingIdeal_infinitySectionIdeal (u v : ℤ) (huv : IsCoprime u v) :
PrimeSpectrum.vanishingIdeal
(PrimeSpectrum.zeroLocus (infinitySectionIdeal u v : Set ℤ[X])) =
infinitySectionIdeal u v