Transvections in the general linear group

Mathlib's Matrix.transvection i j c = 1 + c Eᵢⱼ is the elementary matrix adding c times the j-th coordinate to the i-th one. For i ≠ j it is invertible, and Mathlib packages it as Matrix.SpecialLinearGroup.transvection, together with its zero, addition and inverse laws; this file views it in GL n A along Matrix.SpecialLinearGroup.toGL as TauCeti.transvectionUnit and packages the resulting one-parameter subgroup as TauCeti.transvectionHom.

Writing xᵢⱼ(c) for the transvection, the relations are

• xᵢⱼ(c) xₖₗ(d) = xₖₗ(d) xᵢⱼ(c) whenever j ≠ k and l ≠ i;
• ⁅xᵢⱼ(c), xⱼₗ(d)⁆ = xᵢₗ(cd) whenever i, j and l are distinct.

They are the Chevalley commutator relations of the general linear group. Reading the pair (i, j) as the root εᵢ - εⱼ of the diagonal torus, the first covers every pair of roots whose sum is neither a root nor zero, and the second every pair whose sum is a root: (εᵢ - εⱼ) + (εⱼ - εₗ) is εᵢ - εₗ. In type A the structure constants are ±1; the chosen orientation in the second relation gives 1, which is why its right-hand side is xᵢₗ(cd).

The one remaining case, xᵢⱼ(c) against xⱼᵢ(d), is deliberately absent: there the sum of the two roots is zero, and no commutator formula in terms of a single root subgroup holds.

The opposite root subgroups nevertheless build the standard Weyl representative nᵢⱼ = xᵢⱼ(1) xⱼᵢ(-1) xᵢⱼ(1). The file records its inverse and its conjugation action on the other transvections; this is the normalizer half of the data pinning the elementary matrices against the torus.

Conjugating a transvection by an invertible diagonal matrix rescales its parameter by the value of the corresponding root: TauCeti.diagGL_mul_transvectionUnit_mul_inv says that t xᵢⱼ(c) t⁻¹ is xᵢⱼ(tᵢ c tⱼ⁻¹). Together with the two relations above these are the equations that pin the elementary matrices against the diagonal torus.

Main definitions

• TauCeti.transvectionUnit: a transvection at a pair of distinct indices, as an element of GL n A, namely Matrix.SpecialLinearGroup.transvection along Matrix.SpecialLinearGroup.toGL.
• TauCeti.transvectionHom: the resulting homomorphism from the additive group of A.
• TauCeti.commutingTransvectionPairHom: the product of two commuting transvection homomorphisms, with a shared parameter.
• TauCeti.transvectionWeylElement: the standard Weyl representative exchanging two indices.

Main results

• TauCeti.toGL_transvection_eq_transvectionUnit: the defining equality relating the special-linear and general-linear transvection APIs.
• TauCeti.transvectionUnit_mem_of_adjacent: a subgroup containing the adjacent transvections in both orientations contains every transvection.
• TauCeti.commute_transvectionUnit: transvections at index pairs that do not chain commute.
• TauCeti.commutatorElement_transvectionUnit and TauCeti.commutatorElement_transvectionUnit_reverse: the commutators of two chaining transvections in either orientation.
• TauCeti.det_transvectionUnit and TauCeti.transvectionUnit_injective: a transvection has determinant 1, and distinct parameters give distinct transvections.
• TauCeti.diagGL_mul_transvectionUnit_mul_inv: conjugation by an invertible diagonal matrix.
• TauCeti.permutationGL_inv_mul_transvectionUnit_mul_permutationGL: conjugation by a permutation matrix relabels the two indices.
• TauCeti.map_transvectionUnit and TauCeti.map_transvectionWeylElement: transvections and their Weyl representatives are natural in the base ring.
• TauCeti.transvectionWeylElement_inv: the representative for the opposite root is the inverse.
• TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_self and TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_symm: the reflection exchanges its two root subgroups and negates their parameters.
• TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_left and TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_right: conjugation by nᵢⱼ moves an occurrence of j to i with unchanged parameter. Applying these at the opposite root describes the reverse index movement by conjugation with nᵢⱼ⁻¹.
• TauCeti.commute_transvectionUnit_transvectionWeylElement and TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_of_ne: a transvection whose two indices avoid i and j commutes with nᵢⱼ, so conjugation by nᵢⱼ fixes it.
• TauCeti.transvectionWeylElement_mul_diagGL_mul_inv: conjugation by nᵢⱼ exchanges the two corresponding diagonal coordinates.

References

• R. W. Carter, Simple Groups of Lie Type (1972), §11.3, where these relations are the type A case of the Chevalley commutator formula.
• J. E. Humphreys, Linear Algebraic Groups (1975), §26.3.

theorem TauCeti.diagonal_mul_transvection_mul_diagonal {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [Fintype n] [CommRing A] {v w : n → A} (hvw : ∀ (a : n), v a * w a = 1) (c : A) : Matrix.diagonal v * Matrix.transvection i j c * Matrix.diagonal w = Matrix.transvection i j (v i * c * w j)

Conjugating a transvection by a diagonal matrix rescales its parameter by the two corresponding diagonal entries. The hypothesis says that the two diagonals are inverse to one another.

Transvections as invertible matrices

def TauCeti.transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : GL n A

A transvection at a pair of distinct indices, as an element of GL n A: Mathlib's Matrix.SpecialLinearGroup.transvection viewed along Matrix.SpecialLinearGroup.toGL. It is the value at c of the root subgroup homomorphism attached to the root εᵢ - εⱼ of the diagonal torus.

Equations

• TauCeti.transvectionUnit hij c = Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij c)

@[simp]

theorem TauCeti.coe_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : ↑(transvectionUnit hij c) = Matrix.transvection i j c

The matrix underlying TauCeti.transvectionUnit is the transvection itself.

theorem TauCeti.toGL_transvection_eq_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : Matrix.SpecialLinearGroup.toGL (Matrix.SpecialLinearGroup.transvection hij c) = transvectionUnit hij c

Viewing a special-linear transvection in the general linear group gives TauCeti.transvectionUnit.

@[simp]

theorem TauCeti.transvectionUnit_zero {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : transvectionUnit hij 0 = 1

The transvection of parameter zero is the identity.

@[simp]

theorem TauCeti.transvectionUnit_add {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c d : A) : transvectionUnit hij (c + d) = transvectionUnit hij c * transvectionUnit hij d

The parameter of a transvection is additive: the root subgroup is one-parameter.

@[simp]

theorem TauCeti.transvectionUnit_inv {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : (transvectionUnit hij c)⁻¹ = transvectionUnit hij (-c)

The inverse of a transvection negates its parameter.

@[simp]

theorem TauCeti.det_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : Matrix.GeneralLinearGroup.det (transvectionUnit hij c) = 1

A transvection has determinant one, so the root subgroup lands in SLₙ.

def TauCeti.transvectionHom {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : Multiplicative A →* GL n A

The transvections at a fixed pair of distinct indices form a one-parameter subgroup of GL n A, isomorphic to the additive group of A. This is the root subgroup of εᵢ - εⱼ.

Equations

• TauCeti.transvectionHom hij = Matrix.SpecialLinearGroup.toGL.comp (Matrix.SpecialLinearGroup.transvectionHom hij)

@[simp]

theorem TauCeti.transvectionHom_apply {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : Multiplicative A) : (transvectionHom hij) c = transvectionUnit hij (Multiplicative.toAdd c)

The value of the root subgroup homomorphism is the transvection of the parameter.

theorem TauCeti.transvectionUnit_injective {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : Function.Injective fun (c : A) => transvectionUnit hij c

Distinct parameters give distinct transvections: the parameter is the (i, j) entry. So the root subgroup is a copy of the additive group of A inside GL n A, not a quotient of it.

theorem TauCeti.transvectionHom_injective {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : Function.Injective ⇑(transvectionHom hij)

The bundled root subgroup homomorphism is injective.

theorem TauCeti.commute_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j k l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (c d : A) : Commute (transvectionUnit hij c) (transvectionUnit hkl d)

Transvections at index pairs that do not chain commute in GL n A.

def TauCeti.commutingTransvectionPairHom {n : Type u_1} [DecidableEq n] {A : Type u} {i j k l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (second : Multiplicative A →* Multiplicative A) : Multiplicative A →* GL n A

Two pointwise commuting transvection homomorphisms, evaluated at a shared parameter after a chosen endomorphism in the second component. This packages the standard construction of a one-parameter subgroup as a product of two commuting elementary one-parameter subgroups.

Equations

• TauCeti.commutingTransvectionPairHom hij hkl hjk hli second = ((TauCeti.transvectionHom hij).noncommCoprod (TauCeti.transvectionHom hkl) ⋯).comp ((MonoidHom.id (Multiplicative A)).prod second)

@[simp]

theorem TauCeti.commutingTransvectionPairHom_apply {n : Type u_1} [DecidableEq n] {A : Type u} {i j k l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (second : Multiplicative A →* Multiplicative A) (c : Multiplicative A) : (commutingTransvectionPairHom hij hkl hjk hli second) c = transvectionUnit hij (Multiplicative.toAdd c) * transvectionUnit hkl (Multiplicative.toAdd (second c))

The commuting-pair homomorphism evaluates to the product of its two transvections.

theorem TauCeti.transvectionUnit_mul_transvectionUnit_eq_mul_mul {n : Type u_1} [DecidableEq n] {A : Type u} {i j l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (c d : A) : transvectionUnit hij c * transvectionUnit hjl d = transvectionUnit hjl d * transvectionUnit hij c * transvectionUnit hil (c * d)

The product of two chaining transvections in GL n A, in the two orders.

theorem TauCeti.commutatorElement_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hjl : j ≠ l) (hil : i ≠ l) (c d : A) : ⁅transvectionUnit hij c, transvectionUnit hjl d⁆ = transvectionUnit hil (c * d)

The Chevalley commutator relation of type A. The commutator of the root subgroup elements xᵢⱼ(c) and xⱼₗ(d), for distinct i, j and l, is xᵢₗ(cd): the root εᵢ - εₗ is the sum of εᵢ - εⱼ and εⱼ - εₗ, and the structure constant is 1.

theorem TauCeti.commutatorElement_transvectionUnit_reverse {n : Type u_1} [DecidableEq n] {A : Type u} {i j k : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hki : k ≠ i) (hkj : k ≠ j) (c d : A) : ⁅transvectionUnit hij c, transvectionUnit hki d⁆ = transvectionUnit hkj (-(d * c))

The reverse-orientation form of the type-A Chevalley commutator relation: [xᵢⱼ(c), xₖᵢ(d)] = xₖⱼ(-(dc)).

Weyl elements

def TauCeti.transvectionWeylElement {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : GL n A

The standard representative in GL n A of the Weyl-group transposition exchanging i and j, written as the three-factor word xᵢⱼ(1) xⱼᵢ(-1) xᵢⱼ(1).

Equations

• TauCeti.transvectionWeylElement hij = TauCeti.transvectionUnit hij 1 * TauCeti.transvectionUnit ⋯ (-1) * TauCeti.transvectionUnit hij 1

theorem TauCeti.transvectionWeylElement_def {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : transvectionWeylElement hij = transvectionUnit hij 1 * transvectionUnit ⋯ (-1) * transvectionUnit hij 1

The transvection Weyl element is its standard three-factor word.

theorem TauCeti.commute_transvectionUnit_transvectionWeylElement {n : Type u_1} [DecidableEq n] {A : Type u} {i j k l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (hik : i ≠ k) (hlj : l ≠ j) (c : A) : Commute (transvectionUnit hkl c) (transvectionWeylElement hij)

A transvection whose two indices both avoid i and j commutes with the Weyl representative exchanging i and j: it commutes with each of the three transvections of the defining word.

@[simp]

theorem TauCeti.transvectionWeylElement_inv {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) : (transvectionWeylElement hij)⁻¹ = transvectionWeylElement ⋯

The inverse of the Weyl representative for εᵢ-εⱼ is the representative for the opposite root εⱼ-εᵢ.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_self {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : transvectionWeylElement hij * transvectionUnit hij c * transvectionWeylElement ⋯ = transvectionUnit ⋯ (-c)

Conjugation by the Weyl representative for εᵢ-εⱼ sends its own root subgroup to the opposite root subgroup and negates the parameter.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_symm {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (hij : i ≠ j) (c : A) : transvectionWeylElement hij * transvectionUnit ⋯ c * transvectionWeylElement ⋯ = transvectionUnit hij (-c)

Conjugation by the Weyl representative for εᵢ-εⱼ sends the opposite root subgroup back to its root subgroup and negates the parameter.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_left {n : Type u_1} [DecidableEq n] {A : Type u} {i j k : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (c : A) : transvectionWeylElement hij * transvectionUnit hjk c * transvectionWeylElement ⋯ = transvectionUnit hik c

Conjugation by the Weyl representative exchanging i and j replaces the left index j of xⱼₖ(c) by i.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_right {n : Type u_1} [DecidableEq n] {A : Type u} {i j k : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkj : k ≠ j) (hki : k ≠ i) (c : A) : transvectionWeylElement hij * transvectionUnit hkj c * transvectionWeylElement ⋯ = transvectionUnit hki c

Conjugation by the Weyl representative exchanging i and j replaces the right index j of xₖⱼ(c) by i.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_transvectionUnit_mul_inv_of_ne {n : Type u_1} [DecidableEq n] {A : Type u} {i j k l : n} [CommRing A] [Fintype n] (hij : i ≠ j) (hkl : k ≠ l) (hjk : j ≠ k) (hli : l ≠ i) (hik : i ≠ k) (hlj : l ≠ j) (c : A) : transvectionWeylElement hij * transvectionUnit hkl c * transvectionWeylElement ⋯ = transvectionUnit hkl c

Conjugation by the Weyl representative exchanging i and j fixes a transvection whose two indices both avoid i and j: the reflection in εᵢ - εⱼ fixes the root εₖ - εₗ.

theorem TauCeti.transvectionUnit_mem_of_adjacent {A : Type u} [CommRing A] {m : ℕ} (H : Subgroup (GL (Fin (m + 1)) A)) (hadjacent : ∀ {i j : Fin (m + 1)} (hij : i ≠ j) (c : A), ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → transvectionUnit hij c ∈ H) {i j : Fin (m + 1)} (hij : i ≠ j) (c : A) : transvectionUnit hij c ∈ H

If a subgroup of GL (Fin (m + 1), A) contains every adjacent transvection in both orientations, then it contains every elementary transvection.

@[simp]

theorem TauCeti.permutationGL_inv_mul_transvectionUnit_mul_permutationGL {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] (σ : Equiv.Perm n) (hij : i ≠ j) (c : A) : (permutationGL σ)⁻¹ * transvectionUnit hij c * permutationGL σ = transvectionUnit ⋯ c

Conjugating the transvection xᵢⱼ(c) by the permutation matrix of σ gives the transvection x_{σ⁻¹ i, σ⁻¹ j}(c).

Naturality in the base ring

@[simp]

theorem TauCeti.map_transvectionUnit {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] {B : Type v} [CommRing B] (f : A →+* B) (hij : i ≠ j) (c : A) : (Matrix.GeneralLinearGroup.map f) (transvectionUnit hij c) = transvectionUnit hij (f c)

A transvection is natural in the base ring: applying a ring homomorphism entrywise to xᵢⱼ(c) gives xᵢⱼ(f c).

@[simp]

theorem TauCeti.map_transvectionWeylElement {n : Type u_1} [DecidableEq n] {A : Type u} {i j : n} [CommRing A] [Fintype n] {B : Type v} [CommRing B] (f : A →+* B) (hij : i ≠ j) : (Matrix.GeneralLinearGroup.map f) (transvectionWeylElement hij) = transvectionWeylElement hij

A transvection Weyl representative is natural in the base ring.

Conjugation by the diagonal torus

theorem TauCeti.diagGL_mul_transvectionUnit_mul_inv {A : Type u} [CommRing A] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (t : Fin N → Aˣ) (c : A) : diagGL t * transvectionUnit hij c * (diagGL t)⁻¹ = transvectionUnit hij (↑(t i) * c * ↑(t j)⁻¹)

Conjugating the root subgroup element xᵢⱼ(c) by the diagonal matrix with entries t rescales the parameter by tᵢ tⱼ⁻¹, the value at t of the root εᵢ - εⱼ. This is the equation pinning the root subgroup against the diagonal torus.

@[simp]

theorem TauCeti.transvectionWeylElement_mul_diagGL_mul_inv {A : Type u} [CommRing A] {N : ℕ} {i j : Fin N} (hij : i ≠ j) (t : Fin N → Aˣ) : transvectionWeylElement hij * diagGL t * transvectionWeylElement ⋯ = diagGL (t ∘ ⇑(Equiv.swap i j))

Conjugating an invertible diagonal matrix by the Weyl representative for εᵢ - εⱼ exchanges its i-th and j-th diagonal entries.