Alphabeta MathHow 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.
Free group on a set of generators
Definition
A free group on a set is a group together with a map such that, for every group and every function , there is a unique group homomorphism satisfying
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, is identified with its image .
Depends on
Used by
- A free product of copies of the infinite cyclic group is a free group Corollary
- A free basis of a group Definition
- Group presentation by generators and relations Definition
- The free-group functor F:Set toGrp and free-module functor R⁽⁻⁾:Set→ R-Mod Example
- Every group admits a presentation Theorem
- Free groups on disjoint bases freely multiply to the free group on their union Theorem
- Free groups on the same set are uniquely isomorphic compatibly with their generators Theorem
- Reduced words form the free group on an alphabet Theorem
- The abelianisation of a free group on X is a free abelian group on X Theorem
- The word-quotient group W(X)/∼ satisfies the universal property of the free group on X Theorem
- Von Dyck's theorem: maps of generators that satisfy the relators extend uniquely from a presented group Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 17 results over 11 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
- McKernan, Presentations and Groups of Small Order, Lecture 12 (standard reference, not scraped)