ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11

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.

An action groupoid has the acted-on set as objects, orbits as connected components, and stabilizers as automorphism groups

Example

Every group action determines a groupoid whose categorical connectedness and automorphisms recover the action's orbits and stabilizers.

Facts & Assumptions

Given: A left action of a group $G$ on a set $X$ .

[L1]

The identity and multiplication in $G$ may be read as categorical identity and composition (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible).

[L2]

The action axioms, orbits, and stabilizers have their standard meanings (Left group actions, transitive actions, and faithful actions, The orbit $G \cdot x$ and stabilizer $G_{x}$ of a point in a group action).

[L3]

A groupoid has only invertible arrows, and connectedness means that every two objects are joined by an arrow (Isomorphism, groupoid, and connected category).

Verification

technique · direct

1.1

Define $X // G$ to have objects $x \in X$ and one arrow $(g, x) : x \to g \cdot x$ for each $g \in G$ . Put $(h, g \cdot x) \circ (g, x) = (h g, x)$ and $1_{x} = (e, x)$ .

L1L2

2.1

Associativity and the identity laws follow from the corresponding group laws and the action law. The inverse of $(g, x)$ is $(g^{- 1}, g \cdot x)$ , so this category is a groupoid.

step 1.1L1L2L3

2.2

Objects $x, y$ are joined by an arrow exactly when $y = g \cdot x$ for some $g$ , which is exactly membership in the same orbit. An automorphism of $x$ is an element $g$ with $g \cdot x = x$ , exactly an element of ${Stab}_{G} (x)$ .

step 1.1L2L3

3.1

Consequently the connected components of $X // G$ are the $G$ -orbits, and $Aut (x) = {Stab}_{G} (x)$ with the same multiplication.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 14 results over 10 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, Example 1.1.7 (standard reference, not scraped)