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.
Ascending HNN extensions admit the one-sided normal form
Statement
Let
be an ascending HNN extension. Then every element of has a unique expression
with , , and
Facts & Assumptions
Given: The ascending HNN extension in the statement.
In an ascending HNN extension, the negative associated subgroup is all of and the positive associated subgroup is . (Ascending HNN extensions of injective endomorphisms)
An HNN extension has a unique transversal normal form once transversals are fixed. (Normal forms in an HNN extension are unique relative to chosen transversals)
Proof
Choose a right-coset transversal for containing , and apply [L2] with the transversal for the negative associated subgroup equal to . Every coefficient following a letter is then , so a sign pattern cannot occur: it would create a pin. Thus every transversal normal form has all negative stable letters before all positive stable letters.
Such a normal form has the shape , where and the positive-letter coefficients are identities. Repeatedly use to move and then the intervening coefficients to the right. This gives one expression . If , normality gives ; the resulting middle coefficient has the form , so it lies outside .
Conversely, start with and recursively decompose the coefficient immediately following the last into its unique form with and , moving left by . This recovers a unique transversal normal form. When , the condition makes the last representative nonidentity, so no cancellation occurs at the sign change. This reverse construction and the construction of step 2.1 are inverse, and uniqueness in [L2] therefore gives uniqueness of .
Depends on
Used by
Dependency tree · two levels
9 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)
- C. Loh, Geometric Group Theory: An Introduction (2015 course version) (standard reference, not scraped)