Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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.

Commutator identities in a group whose derived subgroup is central

Statement

Let G be a group (Group and abelian group) whose derived subgroup [G,G] is contained in the centre Z(G) (Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G], The center Z(G) of a group). If [G,G]≤Z(G) then [xy,w]=[x,w][y,w], [x,yw]=[x,y][x,w], and [xn,y]=[x,y]n=[x,yn] for every integer n and all x,y,w∈G, integer powers being those of Powers gn: natural exponents in a monoid and integer exponents in a group, with g0=e.

Facts & Assumptions

Given: A group G with [G,G]≤Z(G), and elements x,y,w∈G.

[F1]

For g,h∈G the commutator is [g,h]:=ghg−1h−1, and [G,G]:=⟨{[g,h]:g,h∈G}⟩ is the subgroup generated by all commutators (Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G]).

[F2]

Z(G):={z∈G:zg=gz for every g∈G} (The center Z(G) of a group).

[L1]

For all m,n∈Z one has gm+n=gmgn and g−m=(gm)−1 (Exponent laws in a group: gm+n=gmgn and (gm)n=gmn for all m,n∈Z, and (gh)n=gnhn when g and h commute).

[L2]

(gh)−1=h−1g−1 (In a group e−1=e, (g−1)−1=g and (gh)−1=h−1g−1, the order of the last product being essential).

Proof

technique · direct
1.1F1F2given

Every commutator [g,h] lies in [G,G], hence in Z(G), so it commutes with every element of G and may be moved to any position in a product without changing that product.

2.1F1L2step 1.1algebra

Expanding, [xy,w]=(xy)w(xy)−1w−1=xywy−1x−1w−1=x (ywy−1w−1) wx−1w−1=x[y,w]wx−1w−1=[y,w] xwx−1w−1=[y,w][x,w]=[x,w][y,w], the last two equalities moving the central factor [y,w] past x and then past [x,w].

2.2F1L2step 1.1algebra

Expanding in the second variable, [x,yw]=x(yw)x−1(yw)−1=xywx−1w−1y−1=(xyx−1)(xwx−1w−1)y−1=(xyx−1)[x,w]y−1=[x,w] xyx−1y−1=[x,y][x,w], where the central factor [x,w] is moved past y−1 and then past [x,y].

3.1F1L1step 2.1algebra

For n∈N the identity [xn,y]=[x,y]n follows by induction: at n=0 both sides are the identity, since x0 is the identity and [e,y]=eye−1y−1=e, and [xn+1,y]=[xnx,y]=[xn,y][x,y]=[x,y]n[x,y]=[x,y]n+1.

4.1L1step 2.1step 2.2step 3.1algebra∎

For a negative integer n put k=−n; then e=[x0,y]=[xkx−k,y]=[xk,y][x−k,y] by step 2.1, so [xn,y]=[x−k,y]=([x,y]k)−1=[x,y]−k=[x,y]n, and the identity [x,yn]=[x,y]n is obtained the same way from step 2.2.

Remarks

The hypothesis [G,G]≤Z(G) is exactly the vanishing of the third term of the lower central series: γ3(G)=[G,[G,G]] is trivial precisely when every commutator commutes with every element of G (Subgroup commutators and the lower central series).

The first two identities are additivity in each variable separately, and they fail without the hypothesis: in general [xy,w]=x[y,w]x−1⋅[x,w], and the conjugating factor is what the hypothesis removes.

Depends on

Used by

Dependency tree · two levels

26 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