Diagonal matrices in the special linear group

A unit in a commutative ring defines a determinant-one diagonal matrix by placing the unit and its inverse in two distinct diagonal positions. This generalizes Mathlib's field-valued Matrix.SpecialLinearGroup.diag2n construction.

Main declarations

• Matrix.SpecialLinearGroup.diag2nUnit: the two-coordinate diagonal matrix attached to a unit.
• Matrix.SpecialLinearGroup.map_diag2nUnit: naturality under a ring homomorphism.
• Matrix.SpecialLinearGroup.diag2nUnit_decompose: a two-coordinate unit diagonal matrix is a product of six transvections.
• Matrix.SpecialLinearGroup.diag2n_decompose: a two-coordinate diagonal matrix over a field is a product of six transvections.

References

The definition of diag2nUnit and its determinant proof generalize and are adapted from Mathlib's Matrix.SpecialLinearGroup.diag2n.

noncomputable def Matrix.SpecialLinearGroup.diag2nUnit {R : Type u} [CommRing R] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (a : Rˣ) : SpecialLinearGroup m R

The determinant-one diagonal matrix with a unit in position i, its inverse in position j, and ones in every other position. This generalizes Mathlib's Matrix.SpecialLinearGroup.diag2n; the determinant proof is adapted from that construction.

Equations

• Matrix.SpecialLinearGroup.diag2nUnit hij a = ⟨Matrix.diagonal fun (r : m) => if r = i then ↑a else if r = j then ↑a⁻¹ else 1, ⋯⟩

@[simp]

theorem Matrix.SpecialLinearGroup.diag2nUnit_coe {R : Type u} [CommRing R] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (a : Rˣ) : ↑(diag2nUnit hij a) = diagonal fun (r : m) => if r = i then ↑a else if r = j then ↑a⁻¹ else 1

The matrix underlying diag2nUnit is its defining diagonal matrix.

@[simp]

theorem Matrix.SpecialLinearGroup.map_diag2nUnit {R : Type u} {S : Type w} [CommRing R] [CommRing S] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (f : R →+* S) (a : Rˣ) : (map f) (diag2nUnit hij a) = diag2nUnit hij ((Units.map ↑f) a)

Mapping the coefficients of a unit diagonal matrix maps its defining unit.

@[simp]

theorem Matrix.SpecialLinearGroup.diag2nUnit_one {R : Type u} [CommRing R] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) : diag2nUnit hij 1 = 1

The unit diagonal family takes the identity unit to the identity matrix.

@[simp]

theorem Matrix.SpecialLinearGroup.diag2nUnit_mk0 {K : Type u} [Field K] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (b : K) (hb : b ≠ 0) : diag2nUnit hij (Units.mk0 b hb) = diag2n hij b hb

Over a field, the unit construction specializes to Mathlib's two-coordinate diagonal matrix.

theorem Matrix.SpecialLinearGroup.diag2nUnit_decompose {R : Type u} [CommRing R] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (a : Rˣ) : diag2nUnit hij a = transvection hij ↑a * transvection ⋯ (-↑a⁻¹) * transvection hij ↑a * transvection hij (-1) * transvection ⋯ 1 * transvection hij (-1)

A two-coordinate unit diagonal matrix is a product of six transvections. The factorization and proof generalize and are adapted from Mathlib's Matrix.SpecialLinearGroup.diag2_decompose.

theorem Matrix.SpecialLinearGroup.diag2n_decompose {K : Type u} [Field K] {m : Type v} [Fintype m] [DecidableEq m] {i j : m} (hij : i ≠ j) (a : K) (ha : a ≠ 0) : diag2n hij a ha = transvection hij a * transvection ⋯ (-a⁻¹) * transvection hij a * transvection hij (-1) * transvection ⋯ 1 * transvection hij (-1)

A two-coordinate diagonal matrix over a field is a product of six transvections.