Commutators of matrix units

This file computes brackets of single-entry matrices over an arbitrary ring. The basic Matrix.lie_single_single formula gives the two possible compositions of matrix units. Its specializations express off-diagonal units and diagonal differences as commutators, and compute their brackets used in standard sl₂ triples. The double-bracket identity Matrix.lie_single_lie_single_of_ne extracts one matrix entry, which is useful for studying ideals of matrix Lie algebras.

These identities concern the underlying Lie ring, so they do not require commutative coefficients or a choice of scalar ring for a Lie algebra.

@[simp]

theorem Matrix.lie_single_single {R : Type u_1} [Ring R] {n : Type u_2} [DecidableEq n] [Fintype n] (a b i j : n) (c d : R) : ⁅single a b c, single i j d⁆ = (if b = i then single a j (c * d) else 0) - if j = a then single i b (d * c) else 0

The commutator of two single-entry matrices is the difference of the two possible composites.

theorem Matrix.lie_single_self_single_of_ne {R : Type u_1} [Ring R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) (c : R) : ⁅single i i 1, single i j c⁆ = single i j c

An off-diagonal matrix unit is a commutator: Eᵢⱼ = ⁅Eᵢᵢ, Eᵢⱼ⁆ when i ≠ j.

theorem Matrix.lie_single_single_eq_sub {R : Type u_1} [Ring R] {n : Type u_2} [DecidableEq n] [Fintype n] (i j : n) (c : R) : ⁅single i j c, single j i 1⁆ = single i i c - single j j c

A difference of diagonal matrix units is a commutator: Eᵢᵢ - Eⱼⱼ = ⁅Eᵢⱼ, Eⱼᵢ⁆.

theorem Matrix.lie_single_self_sub_single_self_single {R : Type u_1} [Ring R] {n : Type u_2} [DecidableEq n] [Fintype n] {p q : n} (hpq : p ≠ q) (c : R) : ⁅single p p 1 - single q q 1, single p q c⁆ = single p q (2 * c)

A difference of diagonal matrix units doubles the matrix unit between them.

theorem Matrix.lie_single_lie_single_of_ne {R : Type u_1} [Ring R] {n : Type u_2} [DecidableEq n] [Fintype n] {i j : n} (hij : i ≠ j) (x : Matrix n n R) : ⁅single j i 1, ⁅single j i 1, x⁆⁆ = single j i (-(2 * x i j))

Bracketing twice against an off-diagonal matrix unit isolates the transposed entry.