Alphabeta Math
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.

✓ 21 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 21 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Free Groups and Presentations

1 · Prerequisites

2 · Summary

Groups, homomorphisms, kernels, quotient groups, and isomorphisms supply the algebraic framework for the constructions here. The development draws on the quotient group and its canonical projection, the universal property of a quotient by a normal subgroup, the normal closure of a subset, the commutator subgroup, generated subgroups, and symmetric groups. Cyclic groups, direct products, and the residue classes modulo a positive integer with their standard representatives supply the targets of the worked presentations, while the induction principle for the natural numbers and elementary counting of finite sets support the arguments about finite bases and finite presentations.

Words in an alphabet with formal inverses and their free equivalence open the page. Free equivalence is an equivalence relation compatible with concatenation, so the words modulo free equivalence form a group. Formal letters act on reduced words by mutually inverse permutations, and evaluating the induced action at the empty word shows that each class holds exactly one reduced word. Evaluation of word classes in a target group proves the universal property, so this quotient is a free group; the normal form makes its generator map injective, and uniqueness identifies it with the reduced-word model. Free bases, rank for a finite basis, relators and presentations, von Dyck's theorem, abelianisation, Tietze transformations, and cyclic reduction follow, closing with torsion-freeness and a conjugacy criterion for cyclically reduced words.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Words in an alphabet with formal inverses, elementary cancellation, and reduced words

Definition

For a set X, form a disjoint copy X−1={x−1:x∈X} of formal inverses. A word on X is a finite string of letters from X⊔X−1; the string of length zero is the empty word.

An elementary cancellation deletes two adjacent letters xx−1 or x−1x. A word is reduced if no elementary cancellation applies. Words are freely equivalent if one can be transformed into the other by finitely many elementary cancellations and their reverse insertions. The reduction and uniqueness facts needed for the free-group construction are proved in Reduced words form the free group on an alphabet ↗.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Free group on a set of generators

Definition

A free group on a set X is a group F(X) together with a map i:X→F(X) such that, for every group G and every function u:X→G, there is a unique group homomorphism u^:F(X)→G satisfying

u^∘i=u.

The reduced-word construction supplies such a group; the construction and its universal property are established in Reduced words form the free group on an alphabet ↗. When no ambiguity arises, x∈X is identified with its image i(x).

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Reduced words form the free group on an alphabet

Statement

Let X be a set. The reduced words on X⊔X−1 form a group when the product of reduced words is their concatenation followed by free reduction. The map sending x∈X to the one-letter word x has the universal property of the free group on X.

Facts & Assumptions

Given: A set X, its formal inverse alphabet, and a group G with a function u:X→G.

[L1]

Words, elementary cancellations, reduced words, and free equivalence are as in the reduced-word definition (Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

[L2]

Induction proves a property of every finite word once it is proved for the empty word and preserved when one letter is appended (The principle of mathematical induction).

[L3]

A group has an associative operation with an identity and two-sided inverses, and a homomorphism preserves products (Group and abelian group, Monoid homomorphism and group homomorphism).

[L4]

The free-group universal property is the extension-and-uniqueness condition in the definition of a free group (Free group on a set of generators).

Proof

technique · direct
1.1

For a word w, read its letters from left to right while maintaining a reduced stack: append a new letter unless it is the formal inverse of the stack's last letter, in which case delete that last letter. Induction on the length of w gives a reduced output red⁡(w), with red⁡(r)=r for every reduced word r.

L1L2
2.1

The same induction shows that reading a neighbouring pair aa−1 or a−1a has exactly the same net effect on every preceding stack as omitting that pair. Thus red⁡ is unchanged by an elementary cancellation or reverse insertion; hence w is freely equivalent to red⁡(w), and two freely equivalent reduced words are equal.

step 1.1L1L2
3.1

Let F(X) be the set of reduced words. For reduced r,s, define r⋅s:=red⁡(rs), let the empty word be e, and let r−1 be the reversal of r with each letter formally inverted. Step 2.1 gives red⁡(red⁡(rs)t)=red⁡(rst)=red⁡(rred⁡(st)).

step 2.1L1
4.1

The equality in step 3.1 makes the product associative. The empty word is a two-sided identity, and rr−1 and r−1r reduce by successive central cancellations to the empty word; therefore every reduced word has the stated two-sided inverse. Hence F(X) is a group.

step 3.1L1L3
4.2

Send x∈X to the one-letter word x. For u:X→G, evaluate a word by replacing x with u(x) and x−1 with u(x)−1 and multiplying in order. Each elementary cancellation evaluates to an adjacent inverse pair, so evaluation is unchanged by step 2.1 and defines u^:F(X)→G; it extends u and preserves the product by the definition in step 3.1.

step 2.1step 3.1L1L3given
5.1

Any homomorphism h:F(X)→G extending u is forced, by writing each reduced word as its ordered product of one-letter words and their inverses, to agree with the evaluation map of step 4.2. Thus u^ is unique.

step 4.1step 4.2L3
6.1

Steps 4.1--5.1 establish the group and the extension-and-uniqueness property of [L4], so the reduced-word group is the free group on X.

step 4.1step 4.2step 5.1L4∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-03Open item page →

Group presentation by generators and relations

Definition

Let F(X) be a free group and let R⊆F(X) be a set of words, called relations. The group with presentation

⟨X∣R⟩:=F(X)/⟨ ⁣⟨R⟩ ⁣⟩F(X)

is the quotient by the normal closure of R. The members of X are its generators. In this quotient, every relation in R becomes the identity, as do all consequences forced by normality.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Free groups on the same set are uniquely isomorphic compatibly with their generators

Statement

If (F,i) and (F′,i′) are free groups on the same set X, then there is a unique group isomorphism ϕ:F→F′ such that

ϕ∘i=i′.

Facts & Assumptions

Given: Two free groups (F,i) and (F′,i′) on X.

[L1]

A map from the generators of a free group extends uniquely to a group homomorphism (Free group on a set of generators).

[L2]

A group isomorphism is a bijective group homomorphism (Group isomorphisms, automorphisms and the set Aut⁡(G)).

Proof

technique · constructive
1.1

Apply the universal property of F to i′:X→F′ and construct the unique homomorphism ϕ:F→F′ with ϕi=i′.

L1givenconstruct
1.2

Apply the universal property of F′ to i:X→F and construct the unique homomorphism ψ:F′→F with ψi′=i.

L1givenconstruct
2.1

Both ψϕ and id⁡F are homomorphisms F→F whose composites with i equal i, so uniqueness in the universal property gives ψϕ=id⁡F.

step 1.1step 1.2L1
2.2

Symmetrically, ϕψ=id⁡F′.

step 1.1step 1.2L1
3.1

Thus ϕ is bijective, hence a group isomorphism.

step 2.1step 2.2L2
4.1

Any generator-compatible homomorphism F→F′ equals ϕ by the uniqueness in step 1.1; in particular the displayed isomorphism is unique.

step 1.1step 3.1L1L2discharge-construct: final∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Every group admits a presentation

Statement

Every group G is isomorphic to a group given by generators and relations. More precisely, if X is the underlying set of G, the free-group extension of the identity function X→G gives a presentation

G≅⟨X∣ker⁡π⟩.

Facts & Assumptions

Given: A group G and its underlying set X.

[L1]

The reduced-word construction supplies a free group on X, and its universal property extends every function X→G uniquely to a group homomorphism (Reduced words form the free group on an alphabet, Free group on a set of generators).

[L2]

The kernel of a group homomorphism is a normal subgroup (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).

[L3]

The normal closure of a set is the smallest normal subgroup containing it (The normal closure of a subset of a group).

[L4]

The presentation ⟨X∣R⟩ is the quotient of F(X) by the normal closure of R (Group presentation by generators and relations).

[L5]

A homomorphism induces an isomorphism from its quotient by the kernel onto its image (First isomorphism theorem for groups: G/ker⁡f≅im⁡f).

Proof

technique · direct
1.1

Apply [L1] to the identity function u:X→G to obtain a homomorphism π:F(X)→G satisfying π(x)=x for every x∈X. It is surjective because every element of G is such an x.

L1given
2.1

Put K:=ker⁡π. By [L2], K⊴F(X); since K is itself a normal subgroup containing K, the minimality in [L3] gives ⟨ ⁣⟨K⟩ ⁣⟩F(X)=K.

step 1.1L2L3
3.1

By [L4], ⟨X∣K⟩=F(X)/K. By [L5] and the surjectivity from step 1.1, F(X)/K≅im⁡π=G.

step 1.1step 2.1L4L5
4.1

Hence G≅⟨X∣ker⁡π⟩, as required.

step 3.1∎
PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Free equivalence is an equivalence relation and concatenation respects it

Statement

For words on X⊔X−1, free equivalence is an equivalence relation in the sense of Equivalence relation, equivalence class, and the quotient set A/∼. It is also a congruence for concatenation: if w∼w′ and v∼v′, then wv∼w′v′.

Facts & Assumptions

Given: A set X and finite words u,v,w,w′,v′ on X⊔X−1.

[F1]

Words are freely equivalent if one can be transformed into the other by finitely many elementary cancellations and their reverse insertions (Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

Proof

technique · direct
1.1

The empty sequence of elementary moves carries every word w to itself, so w∼w.

F1
1.2

If a finite sequence of elementary moves carries w to w′, reversing its order and interchanging every cancellation with the corresponding insertion gives a finite sequence from w′ to w; hence w∼w′ implies w′∼w.

F1
1.3

If w∼w′ and w′∼w′′, concatenating the two finite move sequences gives a finite move sequence from w to w′′; hence free equivalence is transitive.

F1
1.4

If one elementary move changes w to w′, then the same adjacent pair can be deleted or inserted inside uwv, so the move changes uwv to uw′v; applying this to every move in a finite sequence gives w∼w′⇒uwv∼uw′v.

F1
2.1

If w∼w′ and v∼v′, step 1.4 gives wv∼w′v and w′v∼w′v′; transitivity gives wv∼w′v′. Thus steps 1.1 through 1.3 prove that ∼ is an equivalence relation, and this step proves the congruence claim.

step 1.1step 1.2step 1.3step 1.4∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

The word-quotient model Fword(X):=W(X)/∼ with multiplication induced by concatenation

Definition

Let W(X) be the set of all finite words on X⊔X−1, including the empty word ε, and let ∼ be free equivalence as in Words in an alphabet with formal inverses, elementary cancellation, and reduced words. By Free equivalence is an equivalence relation and concatenation respects it, this is an equivalence relation and concatenation respects it.

Throughout, a−1 denotes the partner of a formal letter a∈X⊔X−1 under the pairing that matches each x∈X with x−1∈X−1, so (x−1)−1=x and an elementary cancellation deletes an adjacent pair aa−1 for any formal letter a.

The word-quotient model on X is the quotient set

Fword(X):=W(X)/∼.

The class of a word w is denoted [w]. Define

[w][v]:=[wv],1:=[ε],

and define the generator map iword:X→Fword(X) by iword(x)=[x]. The congruence property makes the displayed product independent of the representatives.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Fword(X) is a group under [w][v]=[wv]

Statement

For every set X, Fword(X) is a group under [w][v]=[wv]. Its identity is the empty-word class [ε], and if w=a1⋯an, then

[w]−1=[an−1⋯a1−1].

Facts & Assumptions

Given: A set X, the quotient Fword(X)=W(X)/∼, and the class product of The word-quotient model Fword(X):=W(X)/∼ with multiplication induced by concatenation.

[L1]

If w∼w′ and v∼v′, then wv∼w′v′ (Free equivalence is an equivalence relation and concatenation respects it).

[F1]

A group is a monoid (G,∗,e) in which every element is invertible (Group and abelian group).

Proof

technique · direct
1.1

If [w]=[w′] and [v]=[v′], then w∼w′ and v∼v′, so [L1] gives wv∼w′v′ and therefore [wv]=[w′v′]; the class product is well-defined.

L1given
2.1

Literal string concatenation is associative, so for all word classes ([u][v])[w]=[(uv)w]=[u(vw)]=[u]([v][w]).

step 1.1algebra
2.2

The empty word satisfies εw=w=wε, so [ε][w]=[w]=[w][ε].

step 1.1algebra
3.1

For w=a1⋯an, put w∗=an−1⋯a1−1; successive cancellations from the central seam carry both ww∗ and w∗w to ε, including when n=0, so [w][w∗]=[ε]=[w∗][w].

givenstep 2.2
4.1

The product is well-defined and associative, [ε] is a two-sided identity, and every [w] has the two-sided inverse [w∗]; these are the group requirements in [F1].

F1step 1.1step 2.1step 2.2step 3.1∎
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Formal letters act by mutually inverse permutations on the set of reduced words

Statement

Let R(X) be the set of reduced words on X⊔X−1. For each formal letter a, there is a permutation λa of R(X) such that λa−1=λa−1. If w=a1⋯an, define Λw:=λa1∘⋯∘λan and Λε:=id⁡R(X). Then Λr(ε)=r for every reduced word r.

Freely equivalent words induce the same permutation of the set of reduced words.

Facts & Assumptions

Given: A set X, the set R(X) of reduced words, and a formal letter a∈X⊔X−1.

[F1]

A word is reduced if no elementary cancellation applies (Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

[F2]
[L1]

If a property P satisfies P(0) and P(n)⇒P(n+1) for every natural number n, then P(n) holds for every n∈N (The principle of mathematical induction).

Proof

technique · constructive
1.1

For r∈R(X), define λa(r) by deleting the first letter when r begins with a−1, and by prepending a otherwise; in the second case the only new seam is not an inverse pair, so the output is reduced, while deletion from a reduced word also leaves a reduced word.

F1givenconstruct
2.1

If r=a−1s is reduced, then s does not begin with a, so λa(r)=s and λa−1(s)=a−1s=r. If r does not begin with a−1, then λa(r)=ar begins with a, so λa−1(ar)=r. Thus λa−1∘λa=id⁡, and replacing a by a−1 gives λa∘λa−1=id⁡.

F1step 1.1
3.1

Hence each λa is a bijection of R(X), so it is a permutation by [F2], and λa−1=λa−1.

F2step 2.1
4.1

For a word w=a1⋯an, construct Λw=λa1∘⋯∘λan, with the empty composite equal to the identity. Composition acts from right to left. If the suffix ak+1⋯an of a reduced word has already been obtained from ε, then it does not begin with ak−1, so λak prepends ak. Induction on the suffix length using [L1] therefore gives Λr(ε)=r for every reduced r, including r=ε.

F1L1step 1.1step 3.1construct
5.1

Inserting or deleting an adjacent pair aa−1 inserts or deletes the adjacent composite λa∘λa−1=id⁡ inside Λw; therefore one elementary move leaves Λw unchanged, and so does any finite sequence of such moves.

step 3.1step 4.1discharge-construct∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every class in W(X)/∼ contains exactly one reduced word

Statement

Every class in W(X)/∼ contains exactly one reduced word.

Facts & Assumptions

Given: A set X, a word w on X⊔X−1, and its class [w]∈W(X)/∼.

[F1]

An elementary cancellation deletes two adjacent letters xx−1 or x−1x; a word is reduced if no elementary cancellation applies; and words are freely equivalent if one can be transformed into the other by finitely many elementary cancellations and their reverse insertions (Words in an alphabet with formal inverses, elementary cancellation, and reduced words).

[L1]

For every reduced word r, one has Λr(ε)=r, and freely equivalent words induce the same permutation of the set of reduced words (Formal letters act by mutually inverse permutations on the set of reduced words).

[L2]

If a property P satisfies P(0) and P(n)⇒P(n+1) for every natural number n, then P(n) holds for every n∈N (The principle of mathematical induction).

[L3]

Free equivalence is an equivalence relation, and if w∼w′ and v∼v′ then wv∼w′v′ (Free equivalence is an equivalence relation and concatenation respects it).

Proof

technique · induction
1.1

The empty word is reduced and freely equivalent to itself, establishing the existence claim for words of length zero.

baseF1
1.2

Assume every word of length n is freely equivalent to a reduced word, and write a word of length n+1 as ua with ∣u∣=n; by the induction hypothesis, u∼r for some reduced r, so the congruence property of [L3], applied with the one-letter word a on the right, gives ua∼ra.

ihL3
1.3

If reduced words r and s lie in the same class, then r∼s, so [L1] gives Λr=Λs.

L1given
2.1

If r is empty or its last letter is not a−1, then ra is reduced; otherwise r=r′a−1 and one elementary cancellation carries ra=r′a−1a to the reduced word r′. Thus every word is freely equivalent to a reduced word.

step 1.2F1L2
2.2

Applying the equal permutations of step 1.3 to the empty word gives r=Λr(ε)=Λs(ε)=s, because the construction in [L1] recovers every reduced word from ε.

step 1.3L1
3.1

Consequently every class [w] contains at least one reduced representative.

step 2.1given
4.1

Step 3.1 gives existence and step 2.2 gives uniqueness, so each class contains exactly one reduced word.

step 3.1step 2.2discharge-induction∎

Remarks

The same normal-form fact already occurs inside the proof of Reduced words form the free group on an alphabet, where invariance of a stack-reduction map proves it by a different route. The present Statement gives that fact a citable, model-specific form for W(X)/∼; it is not a claim of mathematical novelty.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The word-quotient group W(X)/∼ satisfies the universal property of the free group on X

Statement

For every set X, the group Fword(X)=W(X)/∼ together with iword(x)=[x] is a free group on X in the sense of Free group on a set of generators.

Facts & Assumptions

Given: A set X, a group G, and a function u:X→G.

[L1]

Fword(X) is a group under [w][v]=[wv], with identity the empty-word class [ε] and [a1⋯an]−1=[an−1⋯a1−1] (Fword(X) is a group under [w][v]=[wv]).

[F1]

A group homomorphism f:G→H satisfies f(xy)=f(x)f(y) for all x,y∈G, and consequently preserves the identity and inverses (Monoid homomorphism and group homomorphism).

[F2]

In a group, for every x there is y with yx=e=xy (Group and abelian group).

[F3]

A free group on X is a group with a map from X for which every function from X to a group extends uniquely to a group homomorphism (Free group on a set of generators).

Proof

technique · constructive
1.1

Extend u to formal letters by u~(x)=u(x) and u~(x−1)=u(x)−1, and for w=a1⋯an define E(w)=u~(a1)⋯u~(an), with E(ε)=eG.

F2givenconstruct
2.1

An elementary insertion or cancellation changes this product only by inserting or deleting an adjacent factor u(x)u(x)−1 or u(x)−1u(x), which equals eG; hence one elementary move leaves E(w) unchanged.

F2step 1.1
3.1

A finite sequence of elementary moves therefore preserves evaluation, so u^([w]):=E(w) is well-defined on equivalence classes.

step 2.1construct
4.1

For words w,v, one has E(wv)=E(w)E(v), so [L1] and [F1] show that u^ is a homomorphism; moreover u^([x])=u(x), so it extends u.

L1F1step 3.1
5.1

If h:Fword(X)→G is any homomorphism with h([x])=u(x), then [F1] gives h([x−1])=h([x]−1)=u(x)−1. For w=a1⋯an, the class [w] is the ordered product of its one-letter classes, so [F1] forces h([w])=u~(a1)⋯u~(an)=u^([w]); hence h=u^.

L1F1step 4.1
6.1

The homomorphism of step 4.1 exists for every G and u, and step 5.1 makes it unique; by [F3], (Fword(X),iword) is a free group on X, including when X is empty.

F3step 4.1step 5.1discharge-construct∎
CorollaryStatement: AI-generatedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

The generator map X→W(X)/∼ is injective

Statement

The generator map iword:X→Fword(X) of The word-quotient group W(X)/∼ satisfies the universal property of the free group on X, given by iword(x)=[x], is injective.

Facts & Assumptions

Given: Elements x,y∈X with [x]=[y] in Fword(X).

[L1]

Every class in W(X)/∼ contains exactly one reduced word (Every class in W(X)/∼ contains exactly one reduced word).

Proof

technique · direct
1.1

The one-letter words x and y are reduced and lie in the same class, so uniqueness in [L1] gives x=y.

L1given
2.1

Thus iword(x)=iword(y) implies x=y, which is injectivity; when X is empty the assertion is vacuous.

step 1.1∎
CorollaryStatement: AI-generatedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

The word-quotient and reduced-word models are uniquely isomorphic compatibly with X

Statement

Let Fred(X) be the reduced-word group of Reduced words form the free group on an alphabet. There is a unique group isomorphism

Φ:Fword(X)⟶Fred(X)

such that Φ([x])=x for every x∈X. It sends each word class to its unique reduced representative, so the quotient-of-words and reduced-word constructions are compatible models of the same free group rather than rival definitions.

Facts & Assumptions

Given: A set X, the word-quotient free group, and the reduced-word free group on X.

[L1]

If (F,i) and (F′,i′) are free groups on the same set X, then there is a unique group isomorphism ϕ:F→F′ compatible with the two generator maps (Free groups on the same set are uniquely isomorphic compatibly with their generators).

[L2]

Reduced words form a group whose product is concatenation followed by free reduction, and the map sending x∈X to the one-letter word x has the universal property of the free group on X (Reduced words form the free group on an alphabet).

[L3]

Every class in W(X)/∼ contains exactly one reduced word (Every class in W(X)/∼ contains exactly one reduced word).

[L4]

The word-quotient group together with x↦[x] is a free group on X (The word-quotient group W(X)/∼ satisfies the universal property of the free group on X).

Proof

technique · direct
1.1

By [L4] and [L2], both displayed models are free groups on the same set X, so [L1] gives a unique compatible isomorphism Φ:Fword(X)→Fred(X).

L1L2L4
2.1

Compatibility gives Φ([x])=x, and preservation of inverses gives Φ([x−1])=x−1. Thus Φ([a1⋯an]) is the reduced product of the one-letter words a1,…,an. It is freely equivalent to a1⋯an and hence is the unique reduced representative of that class by [L3], including the empty class.

step 1.1L2L3∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

A free basis of a group

Definition

Let F be a group and let B⊆F. Write i:B↪F for the inclusion. The subset B is a free basis of F if (F,i) is a free group on the set B in the sense of Free group on a set of generators. Equivalently, for every group G and every function u:B→G, there is a unique group homomorphism u^:F→G whose restriction to B is u.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Any two finite free bases of the same group have the same cardinality

Statement

If B and C are finite free bases of the same group F, then ∣B∣=∣C∣.

Facts & Assumptions

Given: A group F with finite free bases B and C, and the group C2:=Sym⁡({0,1}).

[L1]

If A and B are finite, then AB is finite and ∣AB∣=∣A∣∣B∣ (The set AB of functions B→A between finite sets is finite, with ∣AB∣=∣A∣∣B∣).

[L2]

For m,n∈N, the natural number mn and the real number mn agree under the canonical inclusion N⊆R (Exponentiation of natural numbers, mn, and its agreement with the integer power in R).

[L3]

If a>1, then am<an whenever m<n in N (Monotonicity of x↦xn and of n↦an).

[L4]

For naturals m,n, exactly one of m<n, m=n, m>n holds (Trichotomy of the order on N).

[F1]

If A is finite and f:A→B is a bijection, then B is finite and ∣B∣=∣A∣ (The cardinality ∣A∣ of a finite set).

Proof

technique · direct
1.1

Every permutation of {0,1} is determined by the image of 0: it is either the identity or the transposition (0 1), and these two maps are distinct; hence C2 is a group with exactly two elements.

L5algebra
2.1

Restriction to B maps Hom⁡(F,C2) to the function set C2B, and the free-basis property gives a unique homomorphic extension of every function B→C2; restriction and extension are inverse maps, so restriction is a bijection Hom⁡(F,C2)→C2B; [L1] counts ∣C2B∣=2∣B∣ and [F1] transports that count along the bijection, giving ∣Hom⁡(F,C2)∣=2∣B∣, including B=∅.

F1L1step 1.1given
3.1

Applying the same restriction-extension bijection to C gives ∣Hom⁡(F,C2)∣=2∣C∣, and therefore 2∣B∣=2∣C∣ as natural numbers.

step 2.1given
4.1

If ∣B∣<∣C∣, then [L2] lets the equality of step 3.1 be read in R, and [L3] applied to the base 2>1 gives 2∣B∣<2∣C∣, contradicting step 3.1; the case ∣C∣<∣B∣ is symmetric, so trichotomy [L4] forces ∣B∣=∣C∣.

L2L3L4step 3.1algebra
5.1

Thus any two finite free bases of F, including empty bases, have the same cardinality.

step 4.1∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

The rank of a free group admitting a finite basis

Definition

A free group F has finite rank if it admits a finite free basis. In that case its rank is

rank⁡(F):=∣B∣,

where B is any finite free basis of F. This is well-defined by Any two finite free bases of the same group have the same cardinality.

This definition is deliberately restricted to free groups that admit a finite free basis. It neither defines rank for a free group whose bases are infinite nor asserts that arbitrary infinite free bases have the same cardinality.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Relators and relations; finitely generated, finitely related, and finite presentations

Definition

In a presentation ⟨X∣R⟩ as in Group presentation by generators and relations, an element r∈R⊆F(X) is called a defining relator. The equation r=1 that it imposes in the quotient is a defining relation. More generally, an equation u=v may be recorded by the relator u−1v. The published definition uses the common looser convention of calling the members of R relations; both conventions define the same quotient group.

A presentation is finitely generated when X is finite, finitely related when R is finite, and finite when both X and R are finite. A group is called finitely generated, finitely related, or finitely presented when it admits a presentation with the corresponding property. For finitely generated groups this agrees with generation by a finite subset in the sense of The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

The normal closure of R is the set of finite products of conjugates of elements of R and their inverses

Statement

Let G be a group and R⊆G. Then

⟨ ⁣⟨R⟩ ⁣⟩G={g1r1ε1g1−1⋯gnrnεngn−1:n∈N, gi∈G, ri∈R, εi∈{1,−1}}.

For n=0 the displayed product is the identity. Replacing every conjugator gi by gi−1 gives the equivalent convention gi−1riεigi.

Facts & Assumptions

Given: A group G, a subset R⊆G, and the set P of displayed finite products.

[F1]

Group multiplication is associative: (xy)z=x(yz) for all x,y,z∈G (Group and abelian group).

[F2]

A subset of a group is a subgroup when it contains the identity and is closed under products and inverses (Subgroup).

[F3]

A subgroup N≤G is normal when gNg−1=N for every g∈G (Normal subgroup: invariance under conjugation).

[L1]

The normal closure of R is the smallest normal subgroup of G containing R (The normal closure of a subset of a group).

Proof

technique · direct
1.1

The empty product puts the identity in P; concatenating two finite products keeps them in P; and [L2] shows that the inverse of a product is the reverse product of factors (grεg−1)−1=gr−εg−1. Thus P is a subgroup of G by [F2].

F1F2L2
1.2

Each r∈R is the one-factor product ere−1, so R⊆P.

given
1.3

Conversely, the normal subgroup ⟨ ⁣⟨R⟩ ⁣⟩G contains every ri±1 and, by normality, every conjugate giri±1gi−1; subgroup closure then contains every finite product in P, including the empty product, so P⊆⟨ ⁣⟨R⟩ ⁣⟩G.

F2F3L1
2.1

For h∈G, conjugating a displayed product by h replaces each factor giriεigi−1 by (hgi)riεi(hgi)−1; hence hPh−1⊆P. Applying the same inclusion with h−1 and conjugating by h gives the reverse inclusion, so hPh−1=P and [F3] makes P normal.

F1F3step 1.1
3.1

Since P is a normal subgroup containing R, minimality in [L1] gives ⟨ ⁣⟨R⟩ ⁣⟩G⊆P.

L1step 1.2step 2.1
4.1

The inclusions of steps 3.1 and 1.3 give the displayed equality.

step 3.1step 1.3∎
PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

In ⟨X∣R⟩, the words u and v represent the same element if and only if u−1v∈⟨ ⁣⟨R⟩ ⁣⟩

Statement

Let u,v∈F(X) and put N=⟨ ⁣⟨R⟩ ⁣⟩F(X). The words u and v represent the same element of ⟨X∣R⟩ if and only if

u−1v∈⟨ ⁣⟨R⟩ ⁣⟩F(X).

By The normal closure of R is the set of finite products of conjugates of elements of R and their inverses, the membership condition is equivalent to expressing u−1v as a finite product of conjugates of relators and their inverses.

Facts & Assumptions

Given: A presentation ⟨X∣R⟩ and words u,v∈F(X).

[F1]

⟨X∣R⟩=F(X)/⟨ ⁣⟨R⟩ ⁣⟩F(X) (Group presentation by generators and relations).

[F2]

If N⊴G, then the elements of G/N are the left cosets gN (The quotient group G/N and coset product (gN)(hN)=ghN).

[L1]

For a subgroup H of a group, aH=bH if and only if a−1b∈H (x∈aH iff a−1x∈H, and aH=bH iff a−1b∈H).

Proof

technique · direct
1.1

Set N=⟨ ⁣⟨R⟩ ⁣⟩F(X); by [F1] and [F2], the elements represented by u and v are the quotient cosets uN and vN.

F1F2given
2.1

By [L1], uN=vN if and only if u−1v∈N.

L1step 1.1
3.1

Substituting the definition of N into step 2.1 proves both directions of the stated equivalence.

step 2.1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group

Statement

Let ⟨X∣R⟩ be a presentation, let H be a group, and let u:X→H be a function. If the evaluation of every r∈R under u is eH, then there is a unique homomorphism

u‾:⟨X∣R⟩⟶H

with u‾([x])=u(x) for every x∈X. Moreover, u‾ is surjective if and only if u(X) generates H.

Facts & Assumptions

Given: A presentation ⟨X∣R⟩, a group H, and a function u:X→H whose evaluation sends every r∈R to eH.

[L1]

If N⊴G, f:G→H is a homomorphism, and N⊆ker⁡f, then there is a unique homomorphism fˉ:G/N→H with f=fˉ∘π (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

[L2]

For every group G and every function u:X→G, there is a unique group homomorphism u^:F(X)→G extending u (Free group on a set of generators).

[L3]

For a normal subgroup N⊴G, the canonical projection π:G→G/N is surjective (The canonical projection π:G→G/N, π(g)=gN, is a surjective group homomorphism).

[F1]

The normal closure of R is the smallest normal subgroup containing R (The normal closure of a subset of a group).

[F2]

The subgroup ⟨S⟩ is the smallest subgroup containing S (The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups).

[L4]

For every group homomorphism f:G→H, one has im⁡f≤H and ker⁡f⊴G (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).

[F3]

A group homomorphism preserves products, identities, and inverses, and a composite of group homomorphisms is a group homomorphism (Monoid homomorphism and group homomorphism).

[F4]

The presented group is ⟨X∣R⟩=F(X)/⟨ ⁣⟨R⟩ ⁣⟩F(X) (Group presentation by generators and relations).

Proof

technique · constructive
1.1

By [L2], construct the unique homomorphism f:F(X)→H whose value on each free generator x is u(x).

L2givenconstruct
1.2

The free generators generate F(X): if K=⟨X⟩≤F(X), the map X→K extends by [L2] to a:F(X)→K, and inclusion j:K↪F(X) makes j∘a agree with id⁡F(X) on X, so uniqueness gives j∘a=id⁡F(X) and K=F(X). By [L3], the canonical quotient map π:F(X)→⟨X∣R⟩ is surjective; since it sends X to the classes [x], [F2] and [F3] show that these classes generate the presented group.

L2L3F2F3construct
2.1

The hypothesis puts every r∈R in ker⁡f; [L4] makes the kernel normal, so the minimality in [F1] gives ⟨ ⁣⟨R⟩ ⁣⟩F(X)⊆ker⁡f.

F1L4step 1.1given
3.1

By [F4], apply [L1] to factor f uniquely through F(X)/⟨ ⁣⟨R⟩ ⁣⟩=⟨X∣R⟩, obtaining u‾ with u‾([x])=u(x).

F4L1step 2.1construct
4.1

If h:⟨X∣R⟩→H also has h([x])=u(x), then [F3] makes h∘π:F(X)→H a homomorphism extending u, so [L2] gives h∘π=f=u‾∘π; uniqueness of the factorisation in [L1] gives h=u‾.

L1L2F3step 3.1
5.1

By [L4], im⁡u‾ is a subgroup containing every u(x), so [F2] gives ⟨u(X)⟩⊆im⁡u‾. Conversely, put K=⟨u(X)⟩. By [F3], u‾−1(K) is a subgroup of the domain, and it contains every [x]; step 1.2 and [F2] therefore give u‾−1(K)=⟨X∣R⟩. Hence im⁡u‾⊆K, so im⁡u‾=⟨u(X)⟩. Thus u‾ is surjective exactly when u(X) generates H.

F2L4F3step 1.2step 3.1discharge-construct∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every finite group has a finite presentation from its multiplication table

Statement

Every finite group G has the finite multiplication-table presentation

G≅⟨xg (g∈G) | xgxhxgh−1 (g,h∈G)⟩.

Facts & Assumptions

Given: A finite group G and a distinct formal symbol xg for each g∈G.

[L1]

A map u:X→H that sends every relator in R to the identity extends uniquely to a homomorphism ⟨X∣R⟩→H (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

[F1]

A presentation ⟨X∣R⟩ is finite when both X and R are finite (Relators and relations; finitely generated, finitely related, and finite presentations).

[F2]

A set is finite when it is in bijection with a natural number; and if A is finite and f:A→B is a bijection, then B is finite (The cardinality ∣A∣ of a finite set).

[F4]

Every nonempty subset of N has a least element (The well-ordering principle).

[F5]

In ⟨X∣R⟩ every relator of R becomes the identity (Group presentation by generators and relations).

Proof

technique · constructive
1.1

Let X={xg:g∈G} and R={xgxhxgh−1:(g,h)∈G×G}. The map g↦xg is a bijection, so [F2] makes X finite. By [L2], G×G is finite, so by [F2] fix a bijection c:G×G→n for some n∈N, and let q send (g,h) to xgxhxgh−1, so that R is the image of q. Sending each r∈R to the least element of the nonempty set {k<n:q(c−1(k))=r}, which exists by [F4], is an injection of R into n; it is a bijection onto its image, that image is finite by [F3], and [F2] transports finiteness back, so R is finite.

F2F3F4L2givenconstruct
2.1

The assignment xg↦g sends each relator xgxhxgh−1 to gh(gh)−1=eG, so [L1] gives a homomorphism π:P:=⟨X∣R⟩→G.

L1step 1.1construct
3.1

By [F5] every relator of R is the identity in P, so [xg][xh][xgh]−1=e and hence [xg][xh]=[xgh]; therefore σ:G→P, σ(g)=[xg], is a homomorphism.

F5step 1.1step 2.1construct
4.1

The composite π∘σ fixes every g∈G; the composite σ∘π fixes every generator class [xg], and uniqueness in [L1] makes it the identity on P. Thus π and σ are inverse isomorphisms.

L1step 2.1step 3.1
5.1

Both X and R are finite and P≅G, so [F1] shows that G has the displayed finite presentation, including when G is the one-element group.

F1step 1.1step 4.1discharge-construct∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

The abelianisation Gab:=G/[G,G] and its canonical map

Definition

Let G be a group. Its abelianisation is the quotient

Gab:=G/[G,G],

where [G,G] is the commutator subgroup of Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G]. This subgroup is normal by The commutator subgroup is normal, so the quotient is defined. The abelianisation map is the canonical surjective homomorphism

qG:G⟶Gab,qG(g)=g[G,G],

of The canonical projection π:G→G/N, π(g)=gN, is a surjective group homomorphism.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Free abelian group on a set

Definition

A free abelian group on a set X is an abelian group A(X) together with a map i:X→A(X) such that, for every abelian group B and every function u:X→B, there is a unique group homomorphism u^:A(X)→B satisfying

u^∘i=u.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The abelianisation of a free group on X is a free abelian group on X

Statement

Let (F(X),i) be a free group on X, let q:F(X)→F(X)ab be the abelianisation map, and put iab=q∘i. Then (F(X)ab,iab) is a free abelian group on X.

Facts & Assumptions

Given: A free group (F(X),i), its quotient F(X)ab=F(X)/[F(X),F(X)], its canonical quotient map q, and iab=q∘i.

[L1]

For N⊴G, the quotient G/N is abelian if and only if [G,G]⊆N (G/N is abelian if and only if [G,G]⊆N).

[L2]

If a homomorphism f:G→H kills a normal subgroup N, then it factors uniquely through G/N (A homomorphism that kills a normal subgroup factors uniquely through the quotient group).

[F1]

A free abelian group on X is an abelian group A(X) with a map from X such that every function from X to an abelian group extends uniquely to a homomorphism from A(X) (Free abelian group on a set).

[F2]

The commutator subgroup [G,G] is the subgroup generated by all commutators [g,h] (Commutators [g,h]=ghg−1h−1 and the commutator subgroup [G,G]).

Proof

technique · constructive
1.1

Taking N=[F(X),F(X)] in [L1] shows that F(X)ab is abelian.

L1given
1.2

Let A be an abelian group and u:X→A a function; the free-group property gives a unique homomorphism f:F(X)→A extending u, and f([g,h])=f(g)f(h)f(g)−1f(h)−1=eA because A is abelian, so every commutator lies in the subgroup ker⁡f; since [F(X),F(X)] is generated by those commutators by [F2], minimality gives [F(X),F(X)]⊆ker⁡f.

F2given
2.1

By [L2], construct a homomorphism f‾:F(X)ab→A with f=f‾∘q; then f‾∘iab=f‾∘q∘i=f∘i=u.

L2step 1.2construct
3.1

If h:F(X)ab→A also extends u, then h∘q and f‾∘q are homomorphisms F(X)→A agreeing with u on X, so free-group uniqueness makes them equal; both h and f‾ therefore factor the same map through the quotient, and uniqueness in [L2] gives h=f‾.

L2step 2.1given
4.1

Steps 1.1, 2.1, and 3.1 give the abelian target, extension, and uniqueness clauses in [F1], so F(X)ab is free abelian on X; for X=∅ both universal properties yield the trivial group.

F1step 1.1step 2.1step 3.1discharge-construct∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Tietze transformations: dictionary generators, redundant relators, renaming, and their inverses

Definition

Let P=⟨X∣R⟩ be a formal presentation. A Tietze transformation in the reversible three-type package is one of the following moves.

  1. A dictionary-generator move chooses a symbol y∉X and a word w∈F(X) and replaces P by ⟨X∪{y}∣R∪{y−1w}⟩. Its inverse may delete y and the relator y−1w only when w contains no y and y occurs in no other remaining relator.
  2. A redundant-relator move chooses r∈⟨ ⁣⟨R⟩ ⁣⟩F(X) (The normal closure of a subset of a group) and replaces R by R∪{r}. Its inverse may delete a relator r only when r∈⟨ ⁣⟨R∖{r}⟩ ⁣⟩F(X), so it is already a consequence of the relators that remain.
  3. A renaming move chooses a bijection α:X→Y and replaces every letter x±1 in every relator by α(x)±1. Its inverse is legal precisely because α−1:Y→X is a bijection.

For finite presentations this package has exactly the same reachability as the classical four moves: add or delete a generator with a dictionary relation, and add or delete a consequence relator. The first two types and their stated inverses are those four moves. Conversely, consider first a renaming bijection α:X→Y with X∩Y=∅. For each x∈X, put y=α(x) and add the fresh generator y with dictionary relator y−1x. These dictionaries make r and its renamed word α(r) equal in the presented group for every r∈R. Hence each α(r) may be added as a consequence relator; once every renamed relator has been added, each old relator r is a consequence of the renamed relators and the dictionaries and may be deleted. Finally, for each pair (x,y), add x−1y, delete its inverse y−1x, and then delete x using the dictionary x−1y. At that point x occurs in no other relator, so every inverse move is legal. The result is ⟨Y∣α(R)⟩.

For a general bijection, choose a finite set Z disjoint from X∪Y and factor the renaming as X→Z→Y. The preceding construction simulates both factors. Thus including renaming as a single move changes the packaging, but not finite-presentation reachability.

PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

Each Tietze transformation preserves the isomorphism type of the presented group

Statement

Each dictionary-generator, redundant-relator, or renaming transformation of Tietze transformations: dictionary generators, redundant relators, renaming, and their inverses, in either legal direction, carries a presentation to a presentation of an isomorphic group.

Facts & Assumptions

Given: A formal presentation P=⟨X∣R⟩ and one legal Tietze transformation applied to it.

[L1]

A map u:X→H that sends every relator in R to the identity extends uniquely to a homomorphism ⟨X∣R⟩→H (Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group).

[F1]

The normal closure of R is the smallest normal subgroup containing R (The normal closure of a subset of a group).

Proof

technique · constructive
1.1

For a dictionary move adjoining y with y=w(X), [L1] gives a homomorphism from the enlarged presentation to the original one by fixing every old generator and sending y to the element represented by w; [L1] also gives a homomorphism in the other direction from the inclusion of the old generators, and their composites fix every generator, so uniqueness makes them inverse isomorphisms. The stated inverse condition removes exactly such a generator after all other occurrences of it have disappeared.

L1givenconstruct
1.2

If r∈⟨ ⁣⟨R⟩ ⁣⟩, then ⟨ ⁣⟨R∪{r}⟩ ⁣⟩=⟨ ⁣⟨R⟩ ⁣⟩: one inclusion follows from R⊆R∪{r} and the other because the old normal closure already contains every new generator of the closure. Thus adding r leaves the quotient unchanged, and the inverse condition states exactly that the same equality remains true after r is deleted.

F1given
1.3

For a renaming bijection α:X→Y, the maps x↦α(x) and y↦α−1(y) send the corresponding relators to the identity, so [L1] extends them to homomorphisms between the two presented groups; their composites fix all generators and are identities by uniqueness.

L1givenconstruct
2.1

Each allowed forward move is covered by steps 1.1 through 1.3, and each inverse is legal under the side condition that makes it the reverse of the same construction; hence every Tietze transformation preserves the presented group's isomorphism type.

step 1.1step 1.2step 1.3discharge-construct∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Two finite presentations define isomorphic groups if and only if a finite sequence of Tietze transformations and inverses connects them

Statement

Let P=⟨X∣R⟩ and Q=⟨Y∣S⟩ be finite presentations. They present isomorphic groups if and only if a finite sequence of the transformations and legal inverses of Tietze transformations: dictionary generators, redundant relators, renaming, and their inverses connects P to Q.

Facts & Assumptions

Given: Finite presentations P=⟨X∣R⟩ and Q=⟨Y∣S⟩.

[L1]

Each Tietze transformation preserves the isomorphism type of the presented group (Each Tietze transformation preserves the isomorphism type of the presented group).

[L2]

In ⟨Z∣T⟩, words u and v represent the same element if and only if u−1v∈⟨ ⁣⟨T⟩ ⁣⟩ (In ⟨X∣R⟩, the words u and v represent the same element if and only if u−1v∈⟨ ⁣⟨R⟩ ⁣⟩).

[L3]

The canonical map from a group to a quotient group is surjective (The canonical projection π:G→G/N, π(g)=gN, is a surjective group homomorphism).

[L4]

If a property P satisfies P(0) and P(n)⇒P(n+1) for every natural number n, then P(n) holds for every n∈N (The principle of mathematical induction).

Proof

technique · constructive
1.1

If a finite sequence of Tietze transformations connects P to Q, composing the isomorphisms supplied by [L1] along that sequence gives an isomorphism between the groups they present; the zero-move case is the identity isomorphism.

L1L4
1.2

Conversely, fix an isomorphism ϕ:GP→GQ. If X∩Y≠∅, first apply one renaming transformation to Q, replacing Y by a finite set disjoint from X, and compose ϕ with the induced isomorphism. Write Q=⟨Y∣S⟩ for this renamed presentation; after connecting P to it, the inverse renaming returns to the original Q. By surjectivity in [L3], for each x∈X choose a word vx(Y) representing ϕ([x]), and for each y∈Y choose a word wy(X) representing ϕ−1([y]); only the finitely many choices indexed by X∪Y are made, successively by [L4].

L1L3L4givenchoose
2.1

Starting from P, add every y∈Y by the dictionary relation dy:=y−1wy(X). In the resulting presentation, vx(Y) and x represent the same element because eliminating the new letters sends vx(Y) to the representative of ϕ−1(ϕ([x]))=[x]; hence [L2] makes dx:=x−1vx(Y) a redundant relator. Add every dx, and then add every s∈S, which is redundant because eliminating Y evaluates it as ϕ−1([s])=1. This is a finite legal sequence from P to C:=⟨X∪Y∣R∪S∪{dx:x∈X}∪{dy:y∈Y}⟩.

L2step 1.2L4construct
2.2

Starting from Q, add every x∈X by the dictionary relation dx=x−1vx(Y). In that presentation, wy(X) and y represent the same element because eliminating X evaluates wy(X) as ϕ(ϕ−1([y]))=[y], so [L2] licenses adding every dy; each r∈R is then redundant because eliminating X evaluates it as ϕ([r])=1. Thus another finite legal sequence runs from Q to the same presentation C.

L2step 1.2L4construct
3.1

Reverse the sequence of step 2.2. Each relator is deleted in reverse order while the earlier relators that originally forced it remain, so the redundant-relator inverse condition is satisfied. Each dictionary generator is deleted only after every later-added relator containing it has been removed, leaving that generator in its dictionary relation alone, so the dictionary inverse condition is satisfied. Hence there is a finite legal sequence from C to the renamed Q. Concatenate it with step 2.1 and, when step 1.2 used a renaming, append that renaming's legal inverse. The resulting finite sequence connects the original P to the original Q.

step 1.2step 2.1step 2.2L4
4.1

Step 1.1 proves the forward implication and steps 1.2 through 3.1 construct the reverse implication, so the two conditions are equivalent.

step 1.1step 3.1discharge-construct∎

Remarks

The finiteness hypothesis is used to make the representative selections and the additions in steps 1.2 through 2.2 into finite sequences. No choice principle is used: each selection is from a single nonempty fibre, repeated a finite number of times.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Cyclically reduced words

Definition

A reduced word is cyclically reduced when it is empty or its first letter is not the formal inverse of its last letter. Equivalently, every cyclic rotation of the word is reduced.

If w=pq as a literal concatenation of words, the word qp is a cyclic permutation of w. This includes w itself by taking p or q empty.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every nonempty reduced word has the form tct−1 with c nonempty and cyclically reduced

Statement

Every nonempty reduced word w has a literal factorisation

w=tct−1

in which c is nonempty and cyclically reduced. The displayed concatenation is the original reduced word, with no hidden cancellation. In particular, w is conjugate to c in the reduced-word free group.

Facts & Assumptions

Given: A nonempty reduced word w on X⊔X−1.

[F1]

A reduced word is cyclically reduced when it is empty or its first letter is not the formal inverse of its last letter (Cyclically reduced words).

[L1]

If a property P satisfies P(0) and P(n)⇒P(n+1) for every natural number n, then P(n) holds for every n∈N (The principle of mathematical induction).

[L2]

The reduced words on X⊔X−1 form a group when the product of reduced words is their concatenation followed by free reduction, and the map sending x∈X to the one-letter word x has the universal property of the free group on X (Reduced words form the free group on an alphabet).

Proof

technique · induction
1.1

A reduced word of length one is nonempty and cyclically reduced, so the assertion holds with t=ε and c=w.

baseF1
1.2

Assume the assertion for all nonempty reduced words shorter than w. If w is cyclically reduced, take t=ε and c=w.

ihF1
1.3

If w is not cyclically reduced, [F1] says that its first and last letters are inverse, so w=aua−1 literally; reducedness of w makes u nonempty and reduced, and ∣u∣=∣w∣−2.

F1given
2.1

Apply [L1] to the property that the assertion holds at every length at most n. The induction hypothesis then applies to the shorter word u, so write u=t′c(t′)−1 with c nonempty and cyclically reduced; then w=(at′)c(at′)−1 literally.

step 1.2step 1.3L1
3.1

The alternatives in steps 1.2 and 2.1 cover every nonempty reduced word and give the required factorisation, including the one-letter boundary.

step 1.1step 1.2step 2.1
4.1

In the group of [L2] the product of reduced words is their concatenation followed by free reduction. The concatenation t c t−1 is the reduced word w of step 3.1, so no reduction occurs there and that product is w; the concatenation t t−1 reduces to the empty word, which is the identity because concatenating it with any reduced word changes nothing, so t−1 is the inverse of t. Hence w=tct−1 exhibits w as a conjugate of c in that group.

L2step 3.1algebradischarge-induction∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Free groups are torsion-free

Statement

Every free group is torsion-free: if g is not the identity and n≥1 is a natural number, then gn is not the identity. Equivalently, every nonidentity element has infinite order in the sense of The order ∣G∣ of a finite group and the order ord⁡(g) of an element, with ord⁡(g)=∞ when no positive power of g is the identity.

Facts & Assumptions

Given: A free group F on a set X, a nonidentity element g∈F, and a natural number n≥1.

[L1]

Every nonempty reduced word has the form tct−1 with c nonempty and cyclically reduced (Every nonempty reduced word has the form tct−1 with c nonempty and cyclically reduced).

[L2]

The reduced words on X⊔X−1 form a group when the product of reduced words is their concatenation followed by free reduction, and the map sending x∈X to the one-letter word x has the universal property of the free group on X (Reduced words form the free group on an alphabet).

[L3]

Free groups on the same set are uniquely isomorphic compatibly with their generators (Free groups on the same set are uniquely isomorphic compatibly with their generators).

[F1]

A reduced word is cyclically reduced when it is empty or its first letter is not the formal inverse of its last letter (Cyclically reduced words).

Proof

technique · direct
1.1

First work in the reduced-word model and let w be a nonidentity element. Then w is itself a nonempty reduced word, and [L1] gives a literal reduced factorisation w=tct−1 with c nonempty and cyclically reduced.

L1L2given
2.1

For every n≥1, the literal concatenation cn is reduced and nonempty: each copy is reduced, and the seam between consecutive copies does not cancel because the last letter of c is not the inverse of its first.

F1step 1.1
3.1

In the product wn, the adjacent factors t−1t cancel between copies, leaving tcnt−1; its two outer seams are the same seams as in the reduced word tct−1, so it is reduced and nonempty by step 2.1, and [L2] therefore shows that wn is not the identity.

L2step 1.1step 2.1
4.1

The reduced-word model is a free group on X by [L2], so [L3] gives a generator-compatible isomorphism from an arbitrary free group on X onto it; transporting g along that isomorphism, which preserves the identity and natural powers, step 3.1 gives gn≠e.

L2L3step 3.1
5.1

Thus no nonidentity element has a positive power equal to the identity, so by [F2] every nonidentity element has infinite order and every free group, including the trivial free group on the empty set, is torsion-free.

F2step 4.1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Two cyclically reduced words in a free group are conjugate if and only if one is a cyclic permutation of the other

Statement

Let u and v be cyclically reduced words on X⊔X−1. In the reduced-word free group on X, the elements represented by u and v are conjugate if and only if v is a cyclic permutation of u.

Through the unique generator-compatible isomorphism, the same criterion holds for elements represented by cyclically reduced words in any free group on X.

Facts & Assumptions

Given: Cyclically reduced words u and v on X⊔X−1.

[L1]

The reduced words on X⊔X−1 form a group under concatenation followed by free reduction, and the map sending x∈X to the one-letter word x has the universal property of the free group on X (Reduced words form the free group on an alphabet).

[F1]

A reduced word is cyclically reduced when it is empty or its first letter is not the formal inverse of its last letter (Cyclically reduced words).

[L2]

Free groups on the same set are uniquely isomorphic compatibly with their generators (Free groups on the same set are uniquely isomorphic compatibly with their generators).

[L3]

If a property P satisfies P(0) and P(n)⇒P(n+1) for every natural number n, then P(n) holds for every n∈N (The principle of mathematical induction).

Proof

technique · induction
1.1

If u=pq literally and v=qp, then p−1up=p−1pqp freely reduces to qp=v, so every cyclic permutation of u is conjugate to u.

L1
1.2

For the converse, suppose v=t−1ut in the reduced-word group and take t reduced. If t=ε, then u=v as elements of the underlying set of reduced words in [L1], which is a cyclic permutation obtained by taking an empty prefix.

baseL1
1.3

Assume the converse holds for conjugators shorter than a nonempty reduced word t=at′, where a is its first letter.

ih
2.1

If neither seam in the literal word t−1ut cancels, that word is reduced and begins with the inverse of its last letter, so [F1] says it is not cyclically reduced; but by [L1] this reduced word is the group product t−1ut and hence equals the cyclically reduced word v, a contradiction. Thus at least one of the two seams cancels.

F1L1step 1.3
3.1

If the right seam cancels, write u=u′a−1; then t−1ut freely reduces to (t′)−1(a−1u′)t′, where a−1u′ is a cyclic permutation of u. If the left seam cancels, write u=au′; then it freely reduces to (t′)−1(u′a)t′, where u′a is a cyclic permutation of u. In either case the shifted word is cyclically reduced and the conjugator t′ is shorter.

step 2.1L1
4.1

Apply [L3] to the property that the converse holds for every conjugator of length at most n. The induction hypothesis makes v a cyclic permutation of the shifted word in step 3.1; cyclic permutations compose, so v is a cyclic permutation of u.

step 1.3step 3.1L3
5.1

If one of u,v is empty, conjugacy forces both to be the identity element, which is the empty word in the reduced-word group of [L1]. Combining this boundary with steps 1.1 and 4.1 proves both directions in the reduced-word model, and [L2] transports the criterion to every free group on X.

step 1.1step 4.1L1L2discharge-induction∎

5 · Examples, counterexamples and false statements

None yet.

Sources