TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-28

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 Reidemeister-Schreier presentation theorem

Statement

Let $G = ⟨ X ∣ R ⟩$ be a group presentation, let $π : F (X) \to G$ be the canonical quotient map, and let $H \leq G$ . Put $H^{'} = π^{- 1} (H) \leq F (X)$ , and choose a Schreier system $T$ for the right cosets of $H^{'}$ in $F (X)$ . If $S$ denotes the nontrivial Schreier generators and $τ$ the corresponding rewriting map, then $H$ has presentation

$H ≅ ⟨ S ∣ τ (t r t^{- 1}) for t \in T, r \in R ⟩ .$

Facts & Assumptions

Given: A presentation $G = ⟨ X ∣ R ⟩$ , the quotient map $π : F (X) \to G$ , a subgroup $H \leq G$ , the preimage $H^{'} = π^{- 1} (H)$ , a Schreier system $T$ , and its nontrivial Schreier generators $S$ .

[L1]

A presentation is the quotient $F (X) / ⟨ ⁣ ⟨ R ⟩ ⁣ ⟩$ (Group presentation by generators and relations).

[L2]

Elements of a normal closure are exactly finite products of conjugates of the generating relators and their inverses (The normal closure of $R$ is the set of finite products of conjugates of elements of $R$ and their inverses).

[L3]

For a Schreier system, the nontrivial Schreier generators form a free basis of the subgroup (Under the stated choice boundary, every subgroup of a free group is free with its nontrivial Schreier generators as a basis).

[L4]

For a word $w = a_{1} \dots a_{n}$ , the Schreier rewrite $τ (w) = σ_{1} \dots σ_{n}$ is defined from the successive representatives $t_{j} = \overline{a_{1} \dots a_{j}}$ ; if $w$ represents an element of $H^{'}$ , then $t_{n} = 1$ (The Schreier rewriting map).

[L5]

The first isomorphism theorem identifies a quotient by a kernel with the image (First isomorphism theorem for groups: $G / \ker f ≅ im f$ ).

[L6]

Schreier generators are the elements $s (u, x) = u x {\overline{u x}}^{- 1}$ (Schreier generators in the right-coset convention).

Proof

technique · direct

1.1L3givenconstruct

By [L3], the set $S$ of nontrivial Schreier generators is a free basis of $H^{'}$ . Therefore the inclusion $S ↪ H^{'}$ extends to an isomorphism $ρ : F (S) \to H^{'}$ .

1.2L1L2L5given

By [L1], the ambient quotient is $G = F (X) / N$ with $N = ⟨ ⁣ ⟨ R ⟩ ⁣ ⟩_{F (X)}$ . The restriction of the quotient map to $H^{'}$ has image $H$ and kernel $H^{'} \cap N$ , so [L5] gives $H ≅ H^{'} / (H^{'} \cap N)$ . By [L2], every element of $H^{'} \cap N$ is a finite product of conjugates $u r^{\pm 1} u^{- 1}$ with $u \in F (X)$ and $r \in R$ . Writing $u = h t$ with $h \in H^{'}$ and $t \in T$ turns each such conjugate into $h (t r^{\pm 1} t^{- 1}) h^{- 1}$ , so $H^{'} \cap N$ is contained in the normal closure in $H^{'}$ of the elements $t r t^{- 1}$ . Conversely, each $t r t^{- 1}$ lies in $H^{'} \cap N$ , and $H^{'} \cap N$ is normal in $H^{'}$ , so that normal closure is exactly $H^{'} \cap N$ .

2.1L4L6step 1.1step 1.2construct

Let $q : H^{'} \to H^{'} / (H^{'} \cap N)$ be the quotient map, and put $\overset{ˉ}{ρ} = q \circ ρ : F (S) \to H^{'} / (H^{'} \cap N) ≅ H$ . Fix $t \in T$ and $r \in R$ , and write $t r t^{- 1} = a_{1} \dots a_{n}$ . Let $t_{j}$ and $σ_{j}$ be the successive representatives and rewriting factors from [L4]. If $a_{j} = x \in X$ , then [L6] gives $σ_{j} = s (t_{j - 1}, x) = t_{j - 1} x t_{j}^{- 1}$ , so $t_{j - 1} a_{j} = σ_{j} t_{j}$ . If $a_{j} = x^{- 1}$ , then $t_{j - 1}$ is the chosen representative of the coset $H^{'} t_{j} x$ , so [L6] gives $σ_{j} = s (t_{j}, x)^{- 1} = t_{j - 1} x^{- 1} t_{j}^{- 1}$ and again $t_{j - 1} a_{j} = σ_{j} t_{j}$ . Multiplying these identities yields $t r t^{- 1} = σ_{1} \dots σ_{n} t_{n} = ρ (τ (t r t^{- 1}))$ , because $t r t^{- 1} \in H^{'}$ forces $t_{n} = 1$ by [L4]. Since $t r t^{- 1} \in H^{'} \cap N$ , every rewritten relator $τ (t r t^{- 1})$ lies in $\ker \overset{ˉ}{ρ}$ .

3.1step 1.1step 1.2step 2.1

Conversely, if $w \in \ker \overset{ˉ}{ρ}$ , then $ρ (w) \in H^{'} \cap N$ . By step 1.2, $ρ (w)$ is a finite product of conjugates in $H^{'}$ of the elements $t r t^{- 1}$ and their inverses. Replacing each $t r t^{- 1}$ by the equal element $ρ (τ (t r t^{- 1}))$ from step 2.1 and applying the isomorphism $ρ^{- 1}$ shows that $w$ lies in the normal closure of the words $τ (t r t^{- 1})$ in $F (S)$ . Therefore $\ker \overset{ˉ}{ρ} = ⟨ ⁣ ⟨ τ (t r t^{- 1}) : t \in T, r \in R ⟩ ⁣ ⟩_{F (S)}$ .

4.1L5step 3.1∎

The map $\overset{ˉ}{ρ}$ is surjective onto $H^{'} / (H^{'} \cap N) ≅ H$ , so [L5] gives $F (S) / \ker \overset{ˉ}{ρ} ≅ H$ . Substituting the kernel description from step 3.1 yields $H ≅ ⟨ S ∣ τ (t r t^{- 1}) for t \in T, r \in R ⟩$ , which is the Reidemeister-Schreier presentation.

Depends on

Used by

Dependency tree · two levels

26 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

Roger C. Lyndon and Paul E. Schupp, Combinatorial Group Theory (standard reference, not scraped)