ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck 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 $B G \to S e t$

Example

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

Facts & Assumptions

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

[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 $S e t$ , and a functor preserves identity and composition (Sets and functions form the large locally small category $S e t$ , 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 Sym (X)$ ).

Verification

technique · direct

1.1

A functor $F : B G \to S e t$ 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 (g h) = F (g) F (h)$ . With $g \cdot x = F (g) (x)$ , these become $e \cdot x = x$ and $(g h) \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 $B G \to S e t$ .

step 2.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

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

Actions of a group GG on sets are functors BG→SetBG→Set