CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11

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.

The center of a free product with at least two nontrivial factors is trivial

Statement

If at least two factors in a free product are nontrivial, then its center is the trivial subgroup.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

Let $G$ be a group (def-group). The center of $G$ is $Z (G) : = {z \in G : z g = g z for every g \in G} .$ Thus $Z (G)$ consists of the elements that commute with every element of $G$ . Its subgroup and normality properties are proved in lem-center-is-normal. (The center $Z (G)$ of a group).

[L2]

For groups as in def-group, a syllable is a tagged pair $(i, g)$ with $i \in I$ and $g \in G_{i} ∖ {e_{i}}$ . A reduced syllable word is a finite list of syllables, indexed by a natural length as in def-natural-numbers, in which adjacent tags differ. The empty list is allowed. At a concatenation seam, adjacent syllables from the same factor are multiplied and an identity result is deleted; this elementary reduction is repeated until the seam is reduced. (Reduced syllable words in a family of groups).

[L3]

Every element of $*_{i \in I} G_{i}$ has a unique reduced syllable expression. The identity is represented by the empty word, and no nonempty reduced word represents the identity. (Normal form theorem for free products).

Proof

technique · contradiction

1.1

Assume for contradiction that a nonidentity central element has reduced word $z = x_{1} \dots x_{n}$ . Choose a nonidentity syllable $g$ from a factor different from the factor of $x_{1}$ .

assume-contragivenL1L2L3

2.1

Then $g z$ is reduced of length $n + 1$ . If the last syllable of $z$ lies in the factor of $g$ , the word $z g$ reduces to length at most $n$ ; otherwise it is reduced of length $n + 1$ but begins in a different factor from $g z$ .

step 1.1

3.1

Normal-form uniqueness gives $g z \neq z g$ in either case, contradicting centrality. Hence only the identity is central.

step 2.1discharge-contradiction∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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

Allen Hatcher, Algebraic Topology, Ch. 1, §1.2, Exercise 1 (standard reference, not scraped)