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 comparison is a separate result.
Source: Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers, Lemma 2.3.
The signed determinant of two integral homogeneous coordinate pairs.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringsdef coordinateDeterminant (u v u' v' : ℤ) : ℤSwapping the two coordinate pairs reverses the determinant's sign.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem coordinateDeterminant_swap (u v u' v' : ℤ) :
coordinateDeterminant u' v' u v = -coordinateDeterminant u v u' v'An integral change of coordinates multiplies the determinant by the matrix determinant.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem coordinateDeterminant_transform (a b c d u v u' v' : ℤ) :
coordinateDeterminant (a * u + b * v) (c * u + d * v)
(a * u' + b * v') (c * u' + d * v') =
(a * d - b * c) * coordinateDeterminant u v u' v'Divisibility of the determinant is unchanged by an integral matrix of determinant 1 or -1. In particular this applies to every prime power.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem dvd_coordinateDeterminant_transform_iff
(a b c d u v u' v' m : ℤ) (hdet : a * d - b * c = 1 ∨ a * d - b * c = -1) :
m ∣ coordinateDeterminant (a * u + b * v) (c * u + d * v)
(a * u' + b * v') (c * u' + d * v') ↔
m ∣ coordinateDeterminant u v u' v'Bezout coefficients give the integral coordinate change used to move a primitive section to infinity. Its second row is (v,-u).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem exists_integral_change_sending_to_infinity
(u v : ℤ) (huv : IsCoprime u v) :
∃ a b : ℤ, a * u + b * v = 1 ∧
coordinateDeterminant a b v (-u) = -1The normalized coordinates of a second primitive pair remain primitive under the explicit integral change sending the first pair to infinity. The witnesses are computed from the original two Bezout identities.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ShimizuYamaguchi26BranchedCoveringstheorem isCoprime_normalizedCoordinates
(u v a b u' v' : ℤ) (hab : a * u + b * v = 1)
(huv' : IsCoprime u' v') :
IsCoprime (-(a * u' + b * v')) (coordinateDeterminant u v u' v')