Alphabeta Math
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.

Every group admits a presentation

Statement

Every group G is isomorphic to a group given by generators and relations. More precisely, if X is the underlying set of G, the free-group extension of the identity function X→G gives a presentation

G≅⟨X∣ker⁡π⟩.

Facts & Assumptions

Given: A group G and its underlying set X.

[L1]

The reduced-word construction supplies a free group on X, and its universal property extends every function X→G uniquely to a group homomorphism (Reduced words form the free group on an alphabet, Free group on a set of generators).

[L2]

The kernel of a group homomorphism is a normal subgroup (The image of a group homomorphism is a subgroup and its kernel is a normal subgroup).

[L3]

The normal closure of a set is the smallest normal subgroup containing it (The normal closure of a subset of a group).

[L4]

The presentation ⟨X∣R⟩ is the quotient of F(X) by the normal closure of R (Group presentation by generators and relations).

[L5]

A homomorphism induces an isomorphism from its quotient by the kernel onto its image (First isomorphism theorem for groups: G/ker⁡f≅im⁡f).

Proof

technique · direct
1.1

Apply [L1] to the identity function u:X→G to obtain a homomorphism π:F(X)→G satisfying π(x)=x for every x∈X. It is surjective because every element of G is such an x.

L1given
2.1

Put K:=ker⁡π. By [L2], K⊴F(X); since K is itself a normal subgroup containing K, the minimality in [L3] gives ⟨ ⁣⟨K⟩ ⁣⟩F(X)=K.

step 1.1L2L3
3.1

By [L4], ⟨X∣K⟩=F(X)/K. By [L5] and the surjectivity from step 1.1, F(X)/K≅im⁡π=G.

step 1.1step 2.1L4L5
4.1

Hence G≅⟨X∣ker⁡π⟩, as required.

step 3.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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