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.

Actions of a group $G$ on sets are functors $BG\to\mathbf{Set}$

Example

A left action of $G$ on a set is exactly a set-valued functor on the one-object category $BG$ .

Facts & Assumptions

Given: A group $G$ and its one-object category $BG$ .

[L1]

A group is a one-object category whose arrows are all invertible (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible).

[L2]

Sets form $\mathbf{Set}$ , and a functor preserves identity and composition (Sets and functions form the large locally small category $\mathbf{Set}$ , Covariant functor, identity functor, composite functor, and contravariant functor).

[L3]

Group actions correspond to homomorphisms into permutation groups (Actions of $G$ on $X$ correspond exactly to homomorphisms $G\to\operatorname{Sym}(X)$ ).

Verification

technique · direct

1.1

A functor $F:BG\to\mathbf{Set}$ selects one set $X=F(*)$ and, for every $g\in G$ , a function $F(g):X\to X$ .

L1L2

1.2

Conversely, a left action defines $F(*)=X$ and $F(g)(x)=g\cdot x$ ; its action axioms are precisely the two functor equations.

L1L2L3

2.1

The functor equations say $F(e)=1_X$ and $F(gh)=F(g)F(h)$ . With $g\cdot x=F(g)(x)$ , these become $e\cdot x=x$ and $(gh)\cdot x=g\cdot(h\cdot x)$ , exactly the left-action axioms.

step 1.1L2L3

3.1

The two constructions recover the same functions $F(g)$ and the same action operation. Therefore left $G$ -actions on sets are exactly functors $BG\to\mathbf{Set}$ .

step 2.1step 1.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: 44 results over 15 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.3.5 (standard reference, not scraped)

Actions of a group GGG on sets are functors BG→SetBG\to\mathbf{Set}BG→Set