Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.ConjJ

Conjugation by a coordinate reflection in the special linear group #

Conjugating a two-by-two matrix by diag(-1, 1) negates both off-diagonal entries and preserves its determinant. The canonical conjJ operation is available over every commutative ring, for modular-form conjugation and reflection of binary quadratic forms.

source
def Matrix.SpecialLinearGroup.conjJ {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
SpecialLinearGroup (Fin 2) R

Conjugation by the coordinate reflection diag(-1, 1) in SL₂(R).

Instances For
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.coe_conjJ {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
    ↑γ.conjJ = !![↑γ 0 0, -↑γ 0 1; -↑γ 1 0, ↑γ 1 1]
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.conjJ_one {R : Type u_1} [CommRing R] :
    conjJ 1 = 1

    Coordinate conjugation preserves the identity.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.conjJ_mul {R : Type u_1} [CommRing R] (γ δ : SpecialLinearGroup (Fin 2) R) :
    (γ * δ).conjJ = γ.conjJ * δ.conjJ

    Coordinate conjugation preserves multiplication.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.conjJ_conjJ {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
    γ.conjJ.conjJ = γ

    Coordinate conjugation is an involution.

    source
    def Matrix.SpecialLinearGroup.conjJMulAut {R : Type u_1} [CommRing R] :
    MulAut (SpecialLinearGroup (Fin 2) R)

    Coordinate conjugation as an involutive group automorphism.

    Instances For
      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.conjJMulAut_apply {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
      conjJMulAut γ = γ.conjJ
      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.conjJMulAut_symm_apply {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
      (MulEquiv.symm conjJMulAut) γ = γ.conjJ
      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.conjJMulAut_mul_self {R : Type u_1} [CommRing R] :
      conjJMulAut * conjJMulAut = 1

      The coordinate reflection has square equal to the identity automorphism.

      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.conjJ_inv {R : Type u_1} [CommRing R] (γ : SpecialLinearGroup (Fin 2) R) :
      γ⁻¹.conjJ = γ.conjJ⁻¹

      Coordinate conjugation preserves inverses.

      source
      @[simp]
      theorem Matrix.SpecialLinearGroup.map_conjJ {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (γ : SpecialLinearGroup (Fin 2) R) :
      (map f) γ.conjJ = ((map f) γ).conjJ

      Coordinate conjugation commutes with a ring homomorphism on coefficients.