LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Vertex and edge stabilizers determine the quotient incidences

Statement

Let a group $G$ act without inversions on an oriented graph $X$ , and let $e$ be an oriented edge with origin $v$ and terminus $w$ . Then the edge stabilizer

$G_{e} : = {g \in G : g \cdot e = e}$

is a subgroup of both vertex stabilizers $G_{v}$ and $G_{w}$ . Moreover, replacing $e, v, w$ by another representative of the same quotient edge conjugates all three stabilizers by the same element of $G$ , so the inclusions

$G_{e} ↪ G_{v}, G_{e} ↪ G_{w}$

are the representative-independent incidence maps attached to the quotient edge.

Facts & Assumptions

Given: An action without inversions on an oriented graph and an oriented edge $e$ from $v$ to $w$ .

[L1]

The quotient graph records vertex and edge orbits, with origin and terminus descending from representatives. (The quotient graph of an action without inversions)

[L2]

A subgroup is a subset closed under products and inverses. (Subgroup)

Proof

technique · direct

1.1

If $g \in G_{e}$ , then $g \cdot e = e$ , so applying origin and terminus to this equality gives $g \cdot v = v$ and $g \cdot w = w$ . Thus $G_{e} \subseteq G_{v} \cap G_{w}$ . Since each stabilizer is an intersection of solution sets to $g \cdot x = x$ , it is closed under products and inverses, hence is a subgroup by [L2].

L1L2given

2.1

If $e^{'} = h \cdot e$ , then $G_{e^{'}} = h G_{e} h^{- 1}$ and similarly $G_{h \cdot v} = h G_{v} h^{- 1}$ and $G_{h \cdot w} = h G_{w} h^{- 1}$ . Therefore passing to another representative of the quotient edge conjugates the two inclusion maps by the same $h$ , so the quotient incidence data from [L1] is well defined up to that canonical conjugacy.

L1step 1.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

8 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)
Yuriy Tumarkin, Groups Acting on Trees (standard reference, not scraped)