The pinned type-A graph automorphism on matrices

For a commutative ring A, inverse transpose is an automorphism of GL_n(A). In type A_r, conjugating it by the signed reversal matrix gives the pinned graph automorphism

g ↦ Q (g⁻¹)ᵀ Q⁻¹,

where Q reverses the standard basis and alternates its signs. The sign correction is essential: it makes the automorphism carry each positive simple-root transvection to the positive simple-root transvection at the reversed Dynkin node, with the parameter unchanged. Without it, inverse transpose would introduce a minus sign.

The construction is over an arbitrary commutative ring and is natural under ring homomorphisms. It is the matrix-points input for the graph automorphism of the full-weight type-A Chevalley carrier.

Main definitions

• Matrix.GeneralLinearGroup.inverseTranspose: the automorphism g ↦ (g⁻¹)ᵀ.
• TauCeti.typeAGraphConjugator: the signed reversal matrix Q.
• TauCeti.typeAGraphAutomorphism: the pinned graph automorphism g ↦ Q (g⁻¹)ᵀ Q⁻¹.

Main results

• TauCeti.typeAGraphAutomorphism_eq_iff_mul_conjugator_mul_transpose_eq and TauCeti.typeAGraphAutomorphism_eq_iff_transpose_mul_conjugator_mul_eq: the automorphism carries g to h exactly when h * Q * gᵀ = Q, equivalently when gᵀ * Q * h = Q.
• TauCeti.typeAGraphAutomorphism_transvectionUnit: the sign-free equation on every positive simple-root subgroup.
• TauCeti.typeAGraphAutomorphism_transvectionUnit_lower: the corresponding equation on every negative simple-root subgroup.
• TauCeti.typeAGraphAutomorphism_transvectionUnit_of_ne: the equation on the root subgroup of an arbitrary root ε_i - ε_j, where the parameter is rescaled by the sign (-1) ^ (i + j + 1).
• TauCeti.typeAGraphAutomorphism_diagGL: the automorphism reverses and inverts diagonal entries.
• TauCeti.typeAGraphAutomorphism_mul_self: the automorphism has order dividing two.
• TauCeti.map_typeAGraphAutomorphism: the construction is natural in the coefficient ring.

References

• R. W. Carter, Finite Groups of Lie Type: Conjugacy Classes and Complex Characters, §1.15.
• R. Steinberg, Lectures on Chevalley Groups, §10.

This supplies the matrix-points prerequisite for the pinned type-A graph automorphism in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, consumed by milestone L1 of TauCetiRoadmap/CFSGStatement/README.md for the Steinberg map defining ²A_r(q).

def Matrix.GeneralLinearGroup.inverseTranspose {n : Type u} [Fintype n] [DecidableEq n] {A : Type v} [CommRing A] : GL n A ≃* GL n A

Inverse transpose on the general linear group. This is the group automorphism g ↦ (g⁻¹)ᵀ.

Equations

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

@[simp]

theorem Matrix.GeneralLinearGroup.coe_inverseTranspose {n : Type u} [Fintype n] [DecidableEq n] {A : Type v} [CommRing A] (g : GL n A) : ↑(inverseTranspose g) = (↑g⁻¹).transpose

The matrix underlying inverse transpose is (g⁻¹)ᵀ.

@[simp]

theorem Matrix.GeneralLinearGroup.inverseTranspose_inverseTranspose {n : Type u} [Fintype n] [DecidableEq n] {A : Type v} [CommRing A] (g : GL n A) : inverseTranspose (inverseTranspose g) = g

Inverse transpose is an involution.

@[simp]

theorem Matrix.GeneralLinearGroup.map_inverseTranspose {n : Type u} [Fintype n] [DecidableEq n] {A : Type v} [CommRing A] {B : Type u_1} [CommRing B] (f : A →+* B) (g : GL n A) : (map f) (inverseTranspose g) = inverseTranspose ((map f) g)

Inverse transpose commutes with entrywise application of a ring homomorphism.

@[simp]

theorem TauCeti.inverseTranspose_diagGL {A : Type u} [CommRing A] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (d : ι → Aˣ) : Matrix.GeneralLinearGroup.inverseTranspose (diagGL d) = diagGL fun (i : ι) => (d i)⁻¹

Inverse transpose inverts the entries of an invertible diagonal matrix.

def TauCeti.typeAGraphConjugator (r : ℕ) (A : Type u) [CommRing A] : GL (Fin (r + 1)) A

The signed reversal matrix Q used in the pinned type-A_r graph automorphism. It first reverses the standard basis and then applies alternating signs.

Equations

• TauCeti.typeAGraphConjugator r A = TauCeti.diagGL TauCeti.typeAGraphSign✝ * TauCeti.permutationGL Fin.revPerm

def TauCeti.typeAGraphAutomorphism (r : ℕ) (A : Type u) [CommRing A] : GL (Fin (r + 1)) A ≃* GL (Fin (r + 1)) A

The pinned graph automorphism of the type-A_r matrix group. It is signed reverse inverse transpose, g ↦ Q (g⁻¹)ᵀ Q⁻¹.

Equations

• TauCeti.typeAGraphAutomorphism r A = Matrix.GeneralLinearGroup.inverseTranspose.trans (MulAut.conj (TauCeti.typeAGraphConjugator r A))

theorem TauCeti.typeAGraphAutomorphism_apply {A : Type u} [CommRing A] (r : ℕ) (g : GL (Fin (r + 1)) A) : (typeAGraphAutomorphism r A) g = typeAGraphConjugator r A * Matrix.GeneralLinearGroup.inverseTranspose g * (typeAGraphConjugator r A)⁻¹

The type-A graph automorphism is conjugated inverse transpose.

theorem TauCeti.typeAGraphConjugator_mul_self {A : Type u} [CommRing A] (r : ℕ) : typeAGraphConjugator r A * typeAGraphConjugator r A = (Matrix.GeneralLinearGroup.scalar (Fin (r + 1))) ((-1) ^ r)

The square of the signed reversal matrix is the scalar matrix (-1)^r I.

@[simp]

theorem TauCeti.typeAGraphAutomorphism_eq_iff_mul_conjugator_mul_transpose_eq {A : Type u} [CommRing A] (r : ℕ) (g h : GL (Fin (r + 1)) A) : (typeAGraphAutomorphism r A) g = h ↔ ↑h * ↑(typeAGraphConjugator r A) * (↑g).transpose = ↑(typeAGraphConjugator r A)

The pinned type-A graph automorphism, read as an invariance equation. The automorphism carries g to h exactly when h * Q * gᵀ = Q, with Q the signed reversal matrix.

Composing with an entrywise ring endomorphism σ and taking g = σ h reads the equation as the invariance of the σ-sesquilinear form of Gram matrix Q under h, in the transposed form recorded by TauCeti.typeAGraphAutomorphism_eq_iff_transpose_mul_conjugator_mul_eq. That is the shape of a unitarity condition, but not yet that condition: σ is only assumed to be a ring endomorphism, and Q is the reversal matrix with alternating signs, so Qᵀ = (-1) ^ r • Q. Even r therefore makes the form Hermitian; odd r makes it skew-Hermitian, which is again Hermitian exactly where -1 = 1, as in characteristic two.

theorem TauCeti.typeAGraphAutomorphism_eq_iff_transpose_mul_conjugator_mul_eq {A : Type u} [CommRing A] (r : ℕ) (g h : GL (Fin (r + 1)) A) : (typeAGraphAutomorphism r A) g = h ↔ (↑g).transpose * ↑(typeAGraphConjugator r A) * ↑h = ↑(typeAGraphConjugator r A)

The invariance equation of the pinned type-A graph automorphism, transposed. The automorphism carries g to h exactly when gᵀ * Q * h = Q.

The two outer factors of TauCeti.typeAGraphAutomorphism_eq_iff_mul_conjugator_mul_transpose_eq may be exchanged because the square of the signed reversal matrix is a scalar. Composing with an entrywise ring endomorphism σ and taking g = σ h, this is the equation h* * Q * h = Q saying that h is an isometry of the σ-sesquilinear form of Gram matrix Q, with h* = (σ h)ᵀ. It is the classical unitarity condition only where that form is Hermitian, which needs σ an involution, not assumed here, and needs Qᵀ = Q: since Qᵀ = (-1) ^ r • Q, even r gives that outright, while odd r gives a skew-Hermitian form, again Hermitian exactly where -1 = 1, as in characteristic two. For σ the identity the form is bilinear, symmetric for even r and alternating for odd r.

@[simp]

theorem TauCeti.typeAGraphAutomorphism_typeAGraphAutomorphism {A : Type u} [CommRing A] (r : ℕ) (g : GL (Fin (r + 1)) A) : (typeAGraphAutomorphism r A) ((typeAGraphAutomorphism r A) g) = g

Applying the pinned type-A graph automorphism twice is the identity.

@[simp]

theorem TauCeti.typeAGraphAutomorphism_mul_self {A : Type u} [CommRing A] (r : ℕ) : typeAGraphAutomorphism r A * typeAGraphAutomorphism r A = 1

The pinned type-A graph automorphism has order dividing two.

@[simp]

theorem TauCeti.inverseTranspose_transvectionUnit {A : Type u} [CommRing A] {n : Type u_1} [Fintype n] [DecidableEq n] {i j : n} (hij : i ≠ j) (c : A) : Matrix.GeneralLinearGroup.inverseTranspose (transvectionUnit hij c) = transvectionUnit ⋯ (-c)

Inverse transpose swaps the indices of a transvection and negates its parameter.

@[simp]

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

The pinned graph automorphism on an arbitrary root subgroup. For every root ε_i - ε_j of the type-A_r system, that is every pair of distinct matrix indices, the automorphism carries the elementary transvection x_{ij}(c) to x_{rev j, rev i}(ε c) with the sign

ε = (-1) ^ (i + j + 1).

The reversal of the two indices is the reversal of the Bourbaki numbering, and the sign is the one produced by the signed conjugator TauCeti.typeAGraphConjugator of this construction: it is what the alternating diagonal signs of Q contribute once the reversal has moved the transvection. The sign is 1 whenever the sum i + j is odd, which it is on every simple root, where TauCeti.typeAGraphAutomorphism_transvectionUnit records the sign-free equation; it is -1 on the roots with even index sum, for instance on ε_0 - ε_2 once the rank is at least two, and that value differs from 1 exactly when (-1 : A) ≠ 1. Whether some other parametrization of the root subgroups makes every sign trivial at once is not addressed here; for that question see R. W. Carter, Simple Groups of Lie Type, §12.2.

theorem TauCeti.typeAGraphAutomorphism_transvectionUnit {A : Type u} [CommRing A] (r : ℕ) (i : Fin r) (c : A) : (typeAGraphAutomorphism r A) (transvectionUnit ⋯ c) = transvectionUnit ⋯ c

The pinned graph automorphism reverses the positive simple-root subgroups without changing their parameters. In Bourbaki numbering, the node i is carried to i.rev. The sign that TauCeti.typeAGraphAutomorphism_transvectionUnit_of_ne attaches to a general root is trivial here, the two matrix indices i and i + 1 of a simple root having odd sum. That general equation is the @[simp] form, and simp reaches this one through it, so this lemma is not itself simp.

theorem TauCeti.typeAGraphAutomorphism_transvectionUnit_lower {A : Type u} [CommRing A] (r : ℕ) (i : Fin r) (c : A) : (typeAGraphAutomorphism r A) (transvectionUnit ⋯ c) = transvectionUnit ⋯ c

The pinned graph automorphism reverses the negative simple-root subgroups without changing their parameters. As for the positive simple roots, TauCeti.typeAGraphAutomorphism_transvectionUnit_of_ne is the @[simp] form that simp uses to reach this one.

@[simp]

theorem TauCeti.typeAGraphAutomorphism_diagGL {A : Type u} [CommRing A] (r : ℕ) (d : Fin (r + 1) → Aˣ) : (typeAGraphAutomorphism r A) (diagGL d) = diagGL fun (i : Fin (r + 1)) => (d i.rev)⁻¹

On the diagonal torus, the pinned graph automorphism reverses and inverts the diagonal entries.

@[simp]

theorem TauCeti.map_typeAGraphConjugator {A : Type u} [CommRing A] {B : Type u_1} [CommRing B] (f : A →+* B) (r : ℕ) : (Matrix.GeneralLinearGroup.map f) (typeAGraphConjugator r A) = typeAGraphConjugator r B

Entrywise base change carries the signed reversal matrix to the signed reversal matrix.

@[simp]

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

The pinned type-A graph automorphism is natural in the coefficient ring.