Rows and columns of invertible 2 × 2 matrices are coprime

The determinant a d - b c of an invertible 2 × 2 matrix !![a, b; c, d] over a commutative ring is a unit, so each row and each column of the matrix generates the unit ideal. These are the GL₂ versions of Mathlib's Matrix.SpecialLinearGroup.isCoprime_row and Matrix.SpecialLinearGroup.isCoprime_col, where the determinant is 1; the proofs follow those.

Over ℤ this says that the image of a primitive vector under GL (Fin 2) ℤ is again primitive, for instance that an integral change of basis of the first homology of a torus carries the coordinate curves to simple closed curves.

Main results

• Matrix.GeneralLinearGroup.isCoprime_row: the two entries of a row are coprime.
• Matrix.GeneralLinearGroup.isCoprime_col: the two entries of a column are coprime.

theorem Matrix.GeneralLinearGroup.isCoprime_row {R : Type u_1} [CommRing R] (A : GL (Fin 2) R) (i : Fin 2) : IsCoprime (↑A i 0) (↑A i 1)

The two entries of a row of an invertible 2 × 2 matrix are coprime.

theorem Matrix.GeneralLinearGroup.isCoprime_col {R : Type u_1} [CommRing R] (A : GL (Fin 2) R) (j : Fin 2) : IsCoprime (↑A 0 j) (↑A 1 j)

The two entries of a column of an invertible 2 × 2 matrix are coprime.