LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Stable elementary matrices equal the commutator subgroup

Statement

For every associative unital ring $R$ , the stable elementary subgroup $E (R)$ is a normal subgroup of $G L (R)$ and $E (R) = [G L (R), G L (R)] .$ Consequently $G L (R) / E (R)$ is abelian. Moreover, for every $n$ , an upper unitriangular matrix $I_{n} + N$ in specified ordered coordinates, with $N_{i j} = 0$ unless $i < j$ , lies in $E_{n} (R)$ in those coordinates. The matrix of the same automorphism in any other ordered basis lies in the stable subgroup $E (R)$ by normality, and hence lies in $E_{N} (R)$ after some finite stabilization; this need not hold at the original matrix size.

Facts & Assumptions

Given: An associative unital ring $R$ and its stable groups $G L (R) \supseteq E (R)$ and elementary matrices $e_{i j} (r) = I + r E_{i j}$ (Stable general linear and elementary groups for right modules).

[F1]

$E (R)$ is by definition the subgroup generated by all elementary matrices, $e_{i j} (r)^{- 1} = e_{i j} (- r)$ , and matrix multiplication is the group operation, so $[g, h]$ denotes $g h g^{- 1} h^{- 1}$ (Stable general linear and elementary groups for right modules).

[F2]

A normal subgroup is a subgroup closed under conjugation, and the subgroup generated by a family is the smallest subgroup containing it (Normal subgroup: invariance under conjugation, The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

Proof

technique · direct

1.1

Let $i, j, k$ be pairwise distinct and $r, s \in R$ . With $X = r E_{i j}$ and $Y = s E_{j k}$ one has $X^{2} = Y^{2} = 0$ , $X Y = r s E_{i k}$ , and $E_{j k} E_{i j} = E_{i j} E_{i k} = E_{i k} E_{j k} = 0$ , so expanding $(I + X + Y + X Y) (I - X - Y + X Y)$ gives $e_{i j} (r) e_{j k} (s) e_{i j} (- r) e_{j k} (- s) = I + r s E_{i k} = e_{i k} (r s)$ .

givenF1algebra

1.2

For $Z \in {G L}_{m} (R)$ the matrix $diag (Z, Z^{- 1})$ lies in $E_{2 m} (R)$ : with $u (C) = I + \sum_{i, j} c_{i j} E_{i, m + j}$ and $l (C) = I + \sum_{i, j} c_{i j} E_{m + i, j}$ one has $u (Z) l (- Z^{- 1}) u (Z) = (\begin{array}{cc} 0 & Z \\ - Z^{- 1} & 0 \end{array})$ , and each of $u (C), l (C)$ is a product of elementary matrices with distinct indices, while $u (1) l (- 1) u (1) = (\begin{array}{cc} 0 & 1 \\ - 1 & 0 \end{array})$ and multiplying the first displayed block swap by the inverse of the second gives $(\begin{array}{cc} 0 & Z \\ - Z^{- 1} & 0 \end{array}) (\begin{array}{cc} 0 & - 1 \\ 1 & 0 \end{array}) = diag (Z, Z^{- 1})$ . The inverse of the second block swap is elementary because it is the inverse of a product of elementary matrices.

givenF1algebra

1.3

For the upper unitriangular claim, use the specified ordered basis as the coordinates in which the matrix is given; it has the standard form $A = I_{n} + N$ with $N_{i j} = 0$ unless $i < j$ , so it remains to prove directly that this coordinate matrix belongs to $E_{n} (R)$ .

given

2.1

Every elementary matrix is a commutator: for $i \neq k$ and $t \in R$ , stabilize if necessary so that some index $j$ distinct from $i$ and $k$ exists, and apply step 1.1 with $r = t$ and $s = 1$ to get $e_{i k} (t) = [e_{i j} (t), e_{j k} (1)]$ ; hence every generator of $E (R)$ lies in $[G L (R), G L (R)]$ , so $E (R) \subseteq [G L (R), G L (R)]$ .

givenF1step 1.1

2.2

For $X, Y \in {G L}_{n} (R)$ one has $diag (X, X^{- 1}) diag (Y, Y^{- 1}) diag ((Y X)^{- 1}, Y X) = diag (X Y (Y X)^{- 1}, X^{- 1} Y^{- 1} Y X) = diag ([X, Y], 1_{n})$ , which represents $[X, Y]$ in $G L (R)$ ; each factor on the left lies in $E (R)$ by step 1.2, so $[G L (R), G L (R)] \subseteq E (R)$ .

givenF1step 1.2algebra

2.3

Argue by induction on $n$ : for $n = 1$ the matrix $A = I_{1}$ is the empty product of elementary matrices, while for $n \geq 2$ one writes $A = (\begin{array}{cc} A^{'} & v \\ 0 & 1 \end{array})$ with $A^{'}$ upper unitriangular of size $n - 1$ and has $diag (A^{'}, 1)^{- 1} A = (\begin{array}{cc} I_{n - 1} & A^{' - 1} v \\ 0 & 1 \end{array}) = \prod_{i = 1}^{n - 1} (I + (A^{' - 1} v)_{i} E_{i n})$ , a product of elementary matrices because $E_{i n} E_{j n} = 0$ for $i \neq j$ ; the induction hypothesis gives $A^{'} \in E_{n - 1} (R)$ , hence $A \in E_{n} (R)$ in the specified coordinates.

givenF1step 1.3inductionalgebra

3.1

Steps 2.1 and 2.2 give $E (R) = [G L (R), G L (R)]$ , and a commutator subgroup is normal, so $E (R)$ is normal in $G L (R)$ by [F2] and $G L (R) / E (R)$ is abelian because every commutator lies in the kernel of the quotient map.

F2step 2.1step 2.2

4.1

If another ordered basis is used, let $P \in {G L}_{n} (R)$ be the matrix whose columns are that basis in the specified coordinates. The new matrix is $P^{- 1} A P$ . By step 2.3, $A \in E_{n} (R) \subseteq E (R)$ , and by step 3.1 the stable subgroup is normal, so $P^{- 1} A P \in E (R)$ . By the definition of the stable elementary subgroup as the union under stabilization, this matrix belongs to $E_{N} (R)$ for some finite $N$ after stabilization.

F1step 3.1step 2.3

∎

Depends on

Used by

Dependency tree · two levels

9 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Lück, Lemma 2.2, pp.25–26 (standard reference, not scraped)
Lurie, Remark 12, p.4 (standard reference, not scraped)