The type-A graph automorphism on the special linear group

The signed reverse-inverse-transpose automorphism of GL_{r+1} preserves determinant one. This file restricts it to an involutive automorphism of SL_{r+1}. Its matrix formula is inherited from TauCeti.typeAGraphAutomorphism, so the conjugating signs still make the action on the standard type-A pinning sign-free.

Main declarations

• Matrix.SpecialLinearGroup.typeAGraphAutomorphism: signed reverse inverse transpose on SL_{r+1}.
• Matrix.SpecialLinearGroup.toGL_typeAGraphAutomorphism: compatibility with the ambient automorphism of GL_{r+1}.
• Matrix.SpecialLinearGroup.typeAGraphAutomorphism_transvection_of_ne: its action on every root subgroup.
• Matrix.SpecialLinearGroup.typeAGraphAutomorphism_typeAGraphAutomorphism and Matrix.SpecialLinearGroup.typeAGraphAutomorphism_mul_self: the involution equations.

References

• R. W. Carter, Simple Groups of Lie Type, Chapter 12.
• R. Steinberg, Lectures on Chevalley Groups, §3.

noncomputable def Matrix.SpecialLinearGroup.typeAGraphAutomorphism (r : ℕ) (A : Type u) [CommRing A] : SpecialLinearGroup (Fin (r + 1)) A ≃* SpecialLinearGroup (Fin (r + 1)) A

The signed reverse-inverse-transpose automorphism of SL_{r+1}. This is the restriction of TauCeti.typeAGraphAutomorphism from the general linear group to determinant-one matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.SpecialLinearGroup.toGL_typeAGraphAutomorphism (r : ℕ) (A : Type u) [CommRing A] (g : SpecialLinearGroup (Fin (r + 1)) A) : toGL ((typeAGraphAutomorphism r A) g) = (TauCeti.typeAGraphAutomorphism r A) (toGL g)

The special-linear graph automorphism restricts the ambient general-linear graph automorphism.

@[simp]

theorem Matrix.SpecialLinearGroup.typeAGraphAutomorphism_transvection_of_ne (r : ℕ) (A : Type u) [CommRing A] {i j : Fin (r + 1)} (hij : i ≠ j) (c : A) : (typeAGraphAutomorphism r A) (transvection hij c) = transvection ⋯ ((-1) ^ (↑i + ↑j + 1) * c)

The special-linear graph automorphism sends the transvection at ε_i - ε_j to the transvection at ε_{rev j} - ε_{rev i}, with the sign from the signed conjugator.

theorem Matrix.SpecialLinearGroup.typeAGraphAutomorphism_transvection (r : ℕ) (A : Type u) [CommRing A] (i : Fin r) (c : A) : (typeAGraphAutomorphism r A) (transvection ⋯ c) = transvection ⋯ c

The special-linear graph automorphism reverses the positive simple-root transvections without changing their parameters.

theorem Matrix.SpecialLinearGroup.typeAGraphAutomorphism_transvection_lower (r : ℕ) (A : Type u) [CommRing A] (i : Fin r) (c : A) : (typeAGraphAutomorphism r A) (transvection ⋯ c) = transvection ⋯ c

The special-linear graph automorphism reverses the negative simple-root transvections without changing their parameters.

@[simp]

theorem Matrix.SpecialLinearGroup.typeAGraphAutomorphism_typeAGraphAutomorphism (r : ℕ) (A : Type u) [CommRing A] (g : SpecialLinearGroup (Fin (r + 1)) A) : (typeAGraphAutomorphism r A) ((typeAGraphAutomorphism r A) g) = g

Applying the special-linear type-A graph automorphism twice is the identity.

@[simp]

theorem Matrix.SpecialLinearGroup.typeAGraphAutomorphism_mul_self (r : ℕ) (A : Type u) [CommRing A] : typeAGraphAutomorphism r A * typeAGraphAutomorphism r A = 1

The special-linear type-A graph automorphism has order dividing two.

@[simp]

theorem Matrix.SpecialLinearGroup.map_typeAGraphAutomorphism (r : ℕ) {A : Type u} [CommRing A] {B : Type u_1} [CommRing B] (f : A →+* B) (g : SpecialLinearGroup (Fin (r + 1)) A) : (map f) ((typeAGraphAutomorphism r A) g) = (typeAGraphAutomorphism r B) ((map f) g)

The signed type-A graph automorphism commutes with entrywise ring maps.