Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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 edge-group presentation is equivalent to the associated-subgroup presentation

Statement

Let

G=⟨A,t | t α(c) t−1=β(c) for c∈C⟩

be an HNN extension as in An HNN extension with its stable letter. Put

C−:=α(C),C+:=β(C)≤A,

and define

ϕ:=β∘α−1:C−→C+.

Then ϕ is an isomorphism, and the same group is presented by

G=⟨A,t | tct−1=ϕ(c) for every c∈C−⟩.

Facts & Assumptions

Given: The HNN extension in the statement.

[L1]

An HNN extension is defined by relations t α(c) t−1=β(c) with α,β injective group homomorphisms into the base group. (An HNN extension with its stable letter)

[L2]

A subgroup is a subset closed under the group operations and inverses. (Subgroup)

[L3]

A group isomorphism is a bijective group homomorphism. (Group isomorphisms, automorphisms and the set Aut⁡(G))

[L4]

A group homomorphism is injective if and only if its kernel is trivial. (A group homomorphism is injective if and only if its kernel is trivial)

Proof

technique · direct
1.1L1L2L3L4given

Because α and β are injective by [L1], [L4] shows that both maps identify C with their images C−,C+≤A from [L2]. Hence α−1:C−→C exists, and ϕ=β∘α−1 is a bijective group homomorphism C−→C+. So ϕ is an isomorphism by [L3].

2.1L1step 1.1algebra

For each c∈C, put x=α(c)∈C−. Then the defining relator tα(c)t−1=β(c) from [L1] becomes txt−1=ϕ(x). Conversely every x∈C− has the form x=α(c) for a unique c∈C, so every relator txt−1=ϕ(x) comes from exactly one original relator.

3.1step 2.1∎

The two presentations therefore have the same generators and the same set of defining relations after the change of notation x=α(c). Hence they present the same group.

Depends on

Used by

Dependency tree · two levels

18 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