TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-29

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.

Different maximal trees give isomorphic graph-of-groups fundamental groups

Statement

Let $G$ be a graph of groups on a connected graph $X$ . If $T$ and $T^{'}$ are maximal subtrees of $X$ , then $π_{1} (G, T)$ and $π_{1} (G, T^{'})$ are isomorphic.

Facts & Assumptions

Given: A graph of groups $G$ on a connected graph $X$ , and maximal subtrees $T, T^{'} \subseteq X$ .

[L1]

The graph-of-groups fundamental group acts on its Bass-Serre tree, with quotient equal to the original graph and with stabilizers of the base cosets equal to the chosen vertex and edge groups. (The fundamental group acts without inversions on its Bass-Serre tree)

[L2]

The Bass-Serre tree has vertices and edges given by cosets of the chosen vertex and edge groups. (The Bass-Serre tree of a graph of groups)

[L3]

A tree action produces a quotient graph of groups from chosen vertex and edge lifts. (The quotient graph of groups attached to a tree action)

[L4]

Bass-Serre structure reconstructs the acting group from that quotient graph of groups and any chosen maximal subtree. (Bass-Serre structure theorem)

Proof

technique · direct

1.1

Let $Γ : = π_{1} (G, T)$ , and let $\tilde{X}$ be its Bass-Serre tree. By [L1], $Γ$ acts on $\tilde{X}$ without inversions, the quotient graph is $X$ , and for the standard lifts $G_{v}$ and $G_{e}$ from [L2] the stabilizers are exactly the chosen groups of $G$ . Thus the quotient graph of groups recovered from this action is the original graph of groups $G$ .

L1L2L3given

2.1

Apply [L4] to the action of $Γ$ on $\tilde{X}$ , but choose the maximal subtree $T^{'}$ of the quotient graph. Step 1.1 identifies that quotient graph of groups with $G$ , so [L4] gives $Γ ≅ π_{1} (G, T^{'}) .$ Since $Γ = π_{1} (G, T)$ , the two relative fundamental groups are isomorphic.

L4step 1.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Jean-Pierre Serre, Trees (standard reference, not scraped)