Alphabeta MathFree Products and Amalgamation
About this page
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.
1 · Prerequisites
Abstract Algebra
Real Analysis
2 · Logical flowchart
3 · Items
Definition
The free product of an arbitrary family of groups
Definition
Reduced syllable words in a family of groups
Lemma
Factor elements act by mutually inverse permutations on reduced syllable words
Theorem
Reduced syllable words form the free product of a family of groups
Theorem
Normal form theorem for free products
Corollary
Finite-order elements of a free product are conjugate into factors
Corollary
The center of a free product with at least two nontrivial factors is trivial
Corollary
Every canonical factor map into a free product is injective
Corollary
Free products are unique up to a unique factor-compatible isomorphism
Corollary
Each factor is a retract of a free product when all other factors are sent trivially
Theorem
A free product has the union presentation of presentations of its factors
Theorem
Free groups on disjoint bases freely multiply to the free group on their union
Corollary
A free product of copies of the infinite cyclic group is a free group
Corollary
The free product of two infinite cyclic groups is the free group on two generators
Definition
Pushouts of group homomorphisms
Theorem
A group pushout is the quotient of a free product by the amalgamating relations
Definition
Free products with amalgamation along monomorphisms
Theorem
A free product with amalgamation has the factor presentations plus the amalgamating relations
Definition
Transversal normal-form data for an amalgamated free product
Lemma
Factor elements act consistently by permutations on amalgamated normal words
Theorem
Normal form theorem for free products with amalgamation
Corollary
The factor maps into a free product with amalgamation are injective
Corollary
The two factor images intersect exactly in the amalgamated subgroup
Corollary
Amalgamation over the trivial group is the ordinary free product
Proposition
The kernels of the amalgamating maps are killed in the opposite canonical maps to a group pushout
Corollary
A pushout along an isomorphism is isomorphic to the other factor
Remark