TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-03

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.

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 \to F^{'}$ such that

$ϕ \circ 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 \to F^{'}$ and construct the unique homomorphism $ϕ : F \to F^{'}$ with $ϕ i = i^{'}$ .

L1givenconstruct

1.2

Apply the universal property of $F^{'}$ to $i : X \to F$ and construct the unique homomorphism $ψ : F^{'} \to F$ with $ψ i^{'} = i$ .

L1givenconstruct

2.1

Both $ψ ϕ$ and ${id}_{F}$ are homomorphisms $F \to 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 \to F^{'}$ equals $ϕ$ by the uniqueness in step 1.1; in particular the displayed isomorphism is unique.

step 1.1step 3.1L1L2discharge-construct: final∎

Depends on

Used by

Dependency tree · two levels

6 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

McKernan, Presentations and Groups of Small Order, Lecture 12 (standard reference, not scraped)