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 members.
This is a coordinate ingredient for Corollary 2.7 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The comparison between the determinant condition and normal crossings of actual divisors on the projective line is a separate geometric assertion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringsdef projectiveResidueClass (u v : ZMod 4) : Fin 6Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem primitive_residues_of_bezout :
∀ u v a b : ZMod 4, a * u + b * v = 1 →
u.val % 2 = 1 ∨ v.val % 2 = 1Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem determinant_zero_of_projectiveResidueClass_eq :
∀ u v u' v' : ZMod 4,
(u.val % 2 = 1 ∨ v.val % 2 = 1) →
(u'.val % 2 = 1 ∨ v'.val % 2 = 1) →
projectiveResidueClass u v = projectiveResidueClass u' v' →
u * v' - v * u' = 0A family of primitive integral coordinate pairs with pairwise determinants not divisible by four contains at most six members.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem card_le_six_of_pairwise_four_not_dvd_coordinateDeterminant
{ι : Type*} [Fintype ι] (u v : ι → ℤ)
(hprimitive : ∀ i : ι, IsCoprime (u i) (v i))
(hseparate : ∀ i j : ι, i ≠ j →
¬ (4 : ℤ) ∣ coordinateDeterminant (u i) (v i) (u j) (v j)) :
Fintype.card ι ≤ 6Among more than six primitive integral coordinate pairs, two distinct members have determinant divisible by four.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem exists_four_dvd_coordinateDeterminant_of_six_lt_card
{ι : Type*} [Fintype ι] (u v : ι → ℤ)
(hprimitive : ∀ i : ι, IsCoprime (u i) (v i))
(hcard : 6 < Fintype.card ι) :
∃ i j : ι, i ≠ j ∧ (4 : ℤ) ∣ coordinateDeterminant (u i) (v i) (u j) (v j)