Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Antitranspose

The antitranspose on the special linear group #

The antitranspose (a b; c d) ↦ (d b; c a), the reflection of a matrix in its antidiagonal, preserves determinants and reverses products, so it restricts to an anti-involution of SL(m, R). On SL(2, ℤ) it fixes the translation T.

Main declarations #

source
def Matrix.SpecialLinearGroup.antitranspose {R : Type u_1} [CommRing R] {m : ℕ} (g : SpecialLinearGroup (Fin m) R) :
SpecialLinearGroup (Fin m) R

The antitranspose of a matrix of determinant one, its reflection in the antidiagonal.

Instances For
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.coe_antitranspose {R : Type u_1} [CommRing R] {m : ℕ} (g : SpecialLinearGroup (Fin m) R) :
    ↑g.antitranspose = (↑g).antitranspose
    source
    theorem Matrix.SpecialLinearGroup.antitranspose_mul {R : Type u_1} [CommRing R] {m : ℕ} (g h : SpecialLinearGroup (Fin m) R) :
    (g * h).antitranspose = h.antitranspose * g.antitranspose

    The antitranspose reverses products.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.antitranspose_one {R : Type u_1} [CommRing R] {m : ℕ} :
    antitranspose 1 = 1
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.antitranspose_inv {R : Type u_1} [CommRing R] {m : ℕ} (g : SpecialLinearGroup (Fin m) R) :
    g⁻¹.antitranspose = g.antitranspose⁻¹

    The antitranspose commutes with inversion.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.antitranspose_antitranspose {R : Type u_1} [CommRing R] {m : ℕ} (g : SpecialLinearGroup (Fin m) R) :
    g.antitranspose.antitranspose = g
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.antitranspose_T :
    ModularGroup.T.antitranspose = ModularGroup.T

    The antitranspose fixes the translation T = (1 1; 0 1).