ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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 orbit-set and fixed-point constructions as Kan extensions

Example

Let $G$ be a group, view it as a one-object category, and let $! : G \to 1$ be the unique functor to the terminal category. A $G$ -action on a set $X$ is the same thing as a functor $X : G \to S e t$ (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible, Left group actions, transitive actions, and faithful actions).

Then the left Kan extension of $X$ along $!$ is the orbit set $X / G$ , while the right Kan extension is the fixed-point set $X^{G}$ .

Facts & Assumptions

Given: A group $G$ , a $G$ -set $X$ , and the unique functor $! : G \to 1$ .

[F1]

Groups are one-object categories and $G$ -actions are functors to $S e t$ (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible, Left group actions, transitive actions, and faithful actions, Sets and functions form the large locally small category $S e t$ ).

[L1]

The comma-category formulae compute left and right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).

[F2]

The one-object category of a group is connected, hence equivalent to the automorphism groupoid of its sole object (Under the Axiom of Choice, a connected small groupoid is equivalent to the automorphism group of any one of its objects).

Verification

technique · direct

1.1F1F2L1

For the unique object of $1$ , the comma category $(! ↓ *)$ is just the one-object category $G$ again, by [F1] and [F2]. A cocone from the $G$ -action diagram $X : G \to S e t$ to a set $Y$ is exactly a function $q : X \to Y$ constant on $G$ -orbits, so its universal example is the quotient map $X \to X / G$ . Therefore [L1] identifies the orbit set with the left Kan extension of $X$ along $!$ .

2.1F1L1∎

Dually, a cone from a set $Y$ to the action diagram is exactly a function $Y \to X$ landing in the equalizer of all action maps, that is, in the fixed-point set $X^{G}$ . Hence [L1] identifies $X^{G}$ with the right Kan extension of $X$ along $!$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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

E. Riehl, Category Theory in Context, 2nd ed., Example 6.2.14 (standard reference, not scraped)