Elementary matrices over a ring and Whitehead's lemma

For a possibly noncommutative ring A and distinct indices i ≠ j, the elementary matrix eᵢⱼ(a) = 1 + a Eᵢⱼ is the transvection TauCeti.transvectionUnit, invertible with inverse eᵢⱼ(-a). The subgroup E n A of GL n A generated by these matrices is the elementary subgroup. Algebraic K₁ is the quotient GL_∞(A) / E_∞(A) of the stable general linear group by the stable elementary subgroup, and this file supplies the finite-size facts which make that quotient a well-defined abelian group:

• E n A is perfect as soon as n has at least three elements: each generator is the commutator ⁅eᵢₗ(a), eₗⱼ(1)⁆ for an index l distinct from i and j. Hence E n A lies in the commutator subgroup of GL n A.
• Whitehead's lemma. For u invertible of size m, the block diagonal matrix u ⊕ u⁻¹ is elementary of size m ⊕ m. Consequently, for a commutator ⁅u, v⁆ of GL m A, the stabilization ⁅u, v⁆ ⊕ 1 is elementary, and for e ∈ E m A and g ∈ GL m A the stabilization of the conjugate g e g⁻¹ is elementary.

Thus, after stabilization, the elementary subgroup is normalized by every invertible matrix and agrees with the commutator subgroup; these are the relations through which homomorphisms on invertible matrices, such as Connes' odd pairing with cyclic cohomology, descend to K₁.

Main definitions

• TauCeti.elementarySubgroup: the subgroup of GL n A generated by elementary matrices.
• TauCeti.fromBlocksGL: the block diagonal homomorphism GL m A × GL k A →* GL (m ⊕ k) A.
• Matrix.upperBlockGL, Matrix.lowerBlockGL: the block unipotent matrices fromBlocks 1 X 0 1 and fromBlocks 1 0 Y 1.

Main results

• TauCeti.commutator_elementarySubgroup_self: ⁅E n A, E n A⁆ = E n A when 3 ≤ card n.
• TauCeti.elementarySubgroup_le_commutator: E n A ≤ ⁅GL n A, GL n A⁆ when 3 ≤ card n.
• Equiv.map_reindexGL_elementarySubgroup: relabelling the indices preserves the elementary subgroup.
• Matrix.upperBlockGL_mem_elementarySubgroup, Matrix.lowerBlockGL_mem_elementarySubgroup: block unipotent matrices are elementary.
• TauCeti.fromBlocksGL_inv_mem_elementarySubgroup: Whitehead's lemma, u ⊕ u⁻¹ ∈ E.
• TauCeti.map_commutator_le_elementarySubgroup: the stabilized commutator subgroup is elementary.
• TauCeti.fromBlocksGL_conj_mem_elementarySubgroup: the stabilization of a conjugate of an elementary matrix is elementary.

References

• J. Milnor, Introduction to Algebraic K-Theory, Annals of Mathematics Studies 72 (1971), §3, Lemma 3.1 (Whitehead) and Proposition 3.2.
• J. Rosenberg, Algebraic K-Theory and Its Applications, GTM 147 (1994), §2.1.

The elementary subgroup

def TauCeti.elementarySubgroup (n : Type u_1) [DecidableEq n] [Fintype n] (A : Type u_2) [Ring A] : Subgroup (GL n A)

The elementary subgroup of GL n A: the subgroup generated by the elementary matrices 1 + a Eᵢⱼ with i ≠ j.

theorem TauCeti.elementarySubgroup_def (n : Type u_1) [DecidableEq n] [Fintype n] (A : Type u_2) [Ring A] : elementarySubgroup n A = Subgroup.closure {g : GL n A | ∃ (i : n) (j : n) (hij : i ≠ j) (a : A), transvectionUnit hij a = g}

The elementary subgroup is the subgroup generated by the elementary matrices.

theorem TauCeti.transvectionUnit_mem_elementarySubgroup {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u_2} [Ring A] {i j : n} (hij : i ≠ j) (a : A) : transvectionUnit hij a ∈ elementarySubgroup n A

Elementary matrices lie in the elementary subgroup.

theorem TauCeti.elementarySubgroup_le_iff {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u_2} [Ring A] {H : Subgroup (GL n A)} : elementarySubgroup n A ≤ H ↔ ∀ (i j : n) (hij : i ≠ j) (a : A), transvectionUnit hij a ∈ H

The elementary subgroup is contained in a subgroup exactly when every elementary matrix is.

theorem TauCeti.commutator_elementarySubgroup_self {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u_2} [Ring A] (hn : 3 ≤ Fintype.card n) : ⁅elementarySubgroup n A, elementarySubgroup n A⁆ = elementarySubgroup n A

The elementary subgroup is perfect in size at least three: each elementary matrix eᵢⱼ(a) is the commutator ⁅eᵢₗ(a), eₗⱼ(1)⁆ for an index l distinct from i and j.

theorem TauCeti.elementarySubgroup_le_commutator {n : Type u_1} [DecidableEq n] [Fintype n] {A : Type u_2} [Ring A] (hn : 3 ≤ Fintype.card n) : elementarySubgroup n A ≤ commutator (GL n A)

In size at least three, the elementary subgroup lies in the commutator subgroup of GL n A.

Block matrices

def TauCeti.fromBlocksGL {A : Type u_2} [Ring A] {m : Type u_3} {k : Type u_4} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] : GL m A × GL k A →* GL (m ⊕ k) A

The block diagonal homomorphism (u, v) ↦ u ⊕ v from GL m A × GL k A to GL (m ⊕ k) A.

@[simp]

theorem TauCeti.coe_fromBlocksGL {A : Type u_2} [Ring A] {m : Type u_3} {k : Type u_4} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (u : GL m A × GL k A) : ↑(fromBlocksGL u) = Matrix.fromBlocks (↑u.1) 0 0 ↑u.2

The matrix underlying a block diagonal invertible matrix.

def Matrix.upperBlockGL {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X : Matrix m k A) : GL (m ⊕ k) A

The block unipotent matrix fromBlocks 1 X 0 1, with inverse fromBlocks 1 (-X) 0 1.

def Matrix.lowerBlockGL {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (Y : Matrix k m A) : GL (m ⊕ k) A

The block unipotent matrix fromBlocks 1 0 Y 1, with inverse fromBlocks 1 0 (-Y) 1.

@[simp]

theorem Matrix.coe_upperBlockGL {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X : Matrix m k A) : ↑X.upperBlockGL = fromBlocks 1 X 0 1

The matrix underlying an upper block unipotent matrix.

@[simp]

theorem Matrix.coe_lowerBlockGL {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (Y : Matrix k m A) : ↑Y.lowerBlockGL = fromBlocks 1 0 Y 1

The matrix underlying a lower block unipotent matrix.

@[simp]

theorem Matrix.upperBlockGL_zero {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] : upperBlockGL 0 = 1

The upper block unipotent matrix of the zero block is the identity.

@[simp]

theorem Matrix.lowerBlockGL_zero {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] : lowerBlockGL 0 = 1

The lower block unipotent matrix of the zero block is the identity.

@[simp]

theorem Matrix.upperBlockGL_add {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X Y : Matrix m k A) : (X + Y).upperBlockGL = X.upperBlockGL * Y.upperBlockGL

Upper block unipotent matrices multiply by adding their blocks.

@[simp]

theorem Matrix.lowerBlockGL_add {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X Y : Matrix k m A) : (X + Y).lowerBlockGL = X.lowerBlockGL * Y.lowerBlockGL

Lower block unipotent matrices multiply by adding their blocks.

@[simp]

theorem Matrix.upperBlockGL_inv {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X : Matrix m k A) : X.upperBlockGL⁻¹ = (-X).upperBlockGL

The inverse of an upper block unipotent matrix negates its block.

@[simp]

theorem Matrix.lowerBlockGL_inv {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (Y : Matrix k m A) : Y.lowerBlockGL⁻¹ = (-Y).lowerBlockGL

The inverse of a lower block unipotent matrix negates its block.

theorem Matrix.upperBlockGL_mem_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (X : Matrix m k A) : X.upperBlockGL ∈ TauCeti.elementarySubgroup (m ⊕ k) A

Upper block unipotent matrices are elementary: they are products of the commuting elementary matrices 1 + X a b E_(inl a, inr b).

theorem Matrix.lowerBlockGL_mem_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] (Y : Matrix k m A) : Y.lowerBlockGL ∈ TauCeti.elementarySubgroup (m ⊕ k) A

Lower block unipotent matrices are elementary: they are products of the commuting elementary matrices 1 + Y b a E_(inr b, inl a).

theorem TauCeti.map_elementarySubgroup_le_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} {k : Type u_3} [DecidableEq m] [Fintype m] [DecidableEq k] [Fintype k] : Subgroup.map (fromBlocksGL.comp (MonoidHom.inl (GL m A) (GL k A))) (elementarySubgroup m A) ≤ elementarySubgroup (m ⊕ k) A

Placing an elementary matrix in the upper left block gives an elementary matrix: the stabilization e ↦ e ⊕ 1 maps the elementary subgroup into the elementary subgroup.

theorem TauCeti.fromBlocksGL_inv_mem_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} [DecidableEq m] [Fintype m] (u : GL m A) : fromBlocksGL (u, u⁻¹) ∈ elementarySubgroup (m ⊕ m) A

Whitehead's lemma. For an invertible matrix u, the block diagonal matrix u ⊕ u⁻¹ is elementary: it is the product of six block unipotent matrices, u ⊕ u⁻¹ = U(u) L(-u⁻¹) U(u) U(-1) L(1) U(-1).

theorem TauCeti.fromBlocksGL_commutatorElement_mem_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} [DecidableEq m] [Fintype m] (u v : GL m A) : fromBlocksGL (⁅u, v⁆, 1) ∈ elementarySubgroup (m ⊕ m) A

Commutators are stably elementary. For invertible matrices u and v, the stabilized commutator ⁅u, v⁆ ⊕ 1 is elementary, being (uv ⊕ (uv)⁻¹) (u⁻¹ ⊕ u) (v⁻¹ ⊕ v).

theorem TauCeti.map_commutator_le_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} [DecidableEq m] [Fintype m] : Subgroup.map (fromBlocksGL.comp (MonoidHom.inl (GL m A) (GL m A))) (commutator (GL m A)) ≤ elementarySubgroup (m ⊕ m) A

The stabilization u ↦ u ⊕ 1 maps the commutator subgroup of GL m A into the elementary subgroup of GL (m ⊕ m) A.

theorem TauCeti.fromBlocksGL_conj_mem_elementarySubgroup {A : Type u_1} [Ring A] {m : Type u_2} [DecidableEq m] [Fintype m] (g : GL m A) {e : GL m A} (he : e ∈ elementarySubgroup m A) : fromBlocksGL (g * e * g⁻¹, 1) ∈ elementarySubgroup (m ⊕ m) A

The elementary subgroup is stably normal. For e elementary and g invertible, the stabilized conjugate g e g⁻¹ ⊕ 1 is elementary, being (g ⊕ g⁻¹) (e ⊕ 1) (g ⊕ g⁻¹)⁻¹.

theorem Equiv.map_reindexGL_elementarySubgroup {n : Type u_1} {m : Type u_2} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] {A : Type u_3} [Ring A] (e : n ≃ m) : Subgroup.map (e.reindexGL A).toMonoidHom (TauCeti.elementarySubgroup n A) = TauCeti.elementarySubgroup m A

Relabelling the indices along an equivalence maps the elementary subgroup onto the elementary subgroup.