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.
Reduced words form the free group on an alphabet
Statement
Let be a set. The reduced words on form a group when the product of reduced words is their concatenation followed by free reduction. The map sending to the one-letter word has the universal property of the free group on .
Facts & Assumptions
Given: A set , its formal inverse alphabet, and a group with a function .
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).
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).
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).
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
For a word , 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 gives a reduced output , with for every reduced word .
The same induction shows that reading a neighbouring pair or has exactly the same net effect on every preceding stack as omitting that pair. Thus is unchanged by an elementary cancellation or reverse insertion; hence is freely equivalent to , and two freely equivalent reduced words are equal.
Let be the set of reduced words. For reduced , define , let the empty word be , and let be the reversal of with each letter formally inverted. Step 2.1 gives .
The equality in step 3.1 makes the product associative. The empty word is a two-sided identity, and and reduce by successive central cancellations to the empty word; therefore every reduced word has the stated two-sided inverse. Hence is a group.
Send to the one-letter word . For , evaluate a word by replacing with and with and multiplying in order. Each elementary cancellation evaluates to an adjacent inverse pair, so evaluation is unchanged by step 2.1 and defines ; it extends and preserves the product by the definition in step 3.1.
Any homomorphism extending 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 is unique.
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 .
Depends on
Used by
- The word-quotient and reduced-word models are uniquely isomorphic compatibly with X Corollary
- The free-group functor F:Set toGrp and free-module functor R⁽⁻⁾:Set→ R-Mod Example
- Every nonempty reduced word has the form tct⁻¹ with c nonempty and cyclically reduced Lemma
- Every group admits a presentation Theorem
- Free groups are torsion-free Theorem
- Two cyclically reduced words in a free group are conjugate if and only if one is a cyclic permutation of the other Theorem
Cited to discharge well-definedness by Free group on a set of generators and Words in an alphabet with formal inverses, elementary cancellation, and reduced words.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 23 results over 12 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- John McKernan, Presentations and Groups of Small Order, Lecture 12 (standard reference, not scraped)