Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Diagonal.Basic

Diagonal matrices in the special linear group #

The diagonal torus of SL_n is the preimage of the diagonal torus of GL_n. A unit in a commutative ring also 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 #

References #

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

source
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
Instances For
    source
    @[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.

    source
    @[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.

    source
    @[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.

    source
    @[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.

    source
    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.

    source
    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.

    source
    theorem Matrix.GeneralLinearGroup.exists_toGL_mul_eq {R : Type u} [CommRing R] {m : Type v} [Fintype m] [DecidableEq m] (g : GL m R) :
    ∃ (x : SpecialLinearGroup m R) (t : m → Rˣ), SpecialLinearGroup.toGL x * TauCeti.diagGL t = g

    Every invertible matrix over a commutative ring is a determinant-one matrix times a diagonal matrix.

    source
    def Matrix.SpecialLinearGroup.diagonalTorus (R : Type u) (n : ℕ) [CommRing R] :
    Subgroup (SpecialLinearGroup (Fin n) R)

    The diagonal torus of SL_n(R): the determinant-one invertible diagonal matrices, that is, the preimage of the diagonal torus of GL_n(R).

    Equations
    Instances For
      source
      theorem Matrix.SpecialLinearGroup.mem_diagonalTorus_iff_toGL_mem {R : Type u} {n : ℕ} [CommRing R] {g : SpecialLinearGroup (Fin n) R} :
      g ∈ diagonalTorus R n ↔ toGL g ∈ TauCeti.diagonalTorus R n

      An element of SL_n(R) lies in its diagonal torus exactly when it lies in the diagonal torus of GL_n(R).

      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.mem_diagonalTorus_iff {R : Type u} {n : ℕ} [CommRing R] {g : SpecialLinearGroup (Fin n) R} :
      g ∈ diagonalTorus R n ↔ (↑g).IsDiag

      An element of SL_n(R) lies in its diagonal torus exactly when it is a diagonal matrix.