ExampleConstruction: Literature-sourcedVerification: Literature-sourcedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

For a group $G$ the monad $G \times (-)$ on sets has the $G$ -sets as its algebras

Example

Let $G$ be a group with identity $u$ . On $S e t$ put

$T (X) = G \times X, T (f) = 1_{G} \times f, η_{X} (x) = (u, x), μ_{X} (g_{1}, (g_{2}, x)) = (g_{1} g_{2}, x) .$

Then $(T, η, μ)$ is a monad, and its $T$ -algebras are exactly the $G$ -sets: a structure map $h : G \times X \to X$ is the same thing as a left action of $G$ on $X$ , and a $T$ -algebra homomorphism is the same thing as a $G$ -equivariant map.

Facts & Assumptions

Given: A group $G$ with identity $u$ .

[L1]

A monad on $C$ is an endofunctor $T$ with natural transformations $η : 1_{C} \Rightarrow T$ and $μ : T^{2} \Rightarrow T$ such that componentwise $μ_{A} \circ T (μ_{A}) = μ_{A} \circ μ_{T A}$ and $μ_{A} \circ T (η_{A}) = 1_{T A} = μ_{A} \circ η_{T A}$ (Monad on a category).

[L2]

A $T$ -algebra is an object $A$ with a morphism $a : T A \to A$ satisfying $a \circ η_{A} = 1_{A}$ and $a \circ T (a) = a \circ μ_{A}$ ; a $T$ -algebra homomorphism $f : (A, a) \to (B, b)$ is a morphism $f : A \to B$ with $f \circ a = b \circ T (f)$ (Algebra and algebra homomorphism for a monad).

[L3]

A left action of $G$ on a set $X$ is a function $G \times X \to X$ , written $(g, x) \mapsto g \cdot x$ , such that $u \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ for all $g, h \in G$ and $x \in X$ ; then $X$ is a $G$ -set (Left group actions, transitive actions, and faithful actions).

[L4]

A function $f : X \to Y$ between $G$ -sets is $G$ -equivariant when $f (g \cdot x) = g \cdot f (x)$ for every $g \in G$ and $x \in X$ (Equivariant maps and isomorphisms of group actions).

[L5]

Sets and functions form the category $S e t$ , with composition of functions and identity functions (Sets and functions form the large locally small category $S e t$ ).

[L6]

The Eilenberg–Moore category $C^{T}$ has the $T$ -algebras as objects and the $T$ -algebra homomorphisms as morphisms (Eilenberg–Moore category of a monad).

Verification

technique · direct

1.1

$T$ is an endofunctor of $S e t$ : $T (1_{X}) = 1_{G} \times 1_{X} = 1_{G \times X}$ , and $T (f^{'} \circ f) = 1_{G} \times (f^{'} \circ f) = (1_{G} \times f^{'}) \circ (1_{G} \times f) = T (f^{'}) \circ T (f)$ , since both sides send $(g, x)$ to $(g, f^{'} (f (x)))$ .

L1L5given

1.2

$η$ is natural: for $f : X \to Y$ , both $T (f) \circ η_{X}$ and $η_{Y} \circ f$ send $x$ to $(u, f (x))$ . And $μ$ is natural: for $f : X \to Y$ , both $T (f) \circ μ_{X}$ and $μ_{Y} \circ T (T (f))$ send $(g_{1}, (g_{2}, x))$ to $(g_{1} g_{2}, f (x))$ .

L1given

2.1

Associativity holds componentwise: on $(g_{1}, (g_{2}, (g_{3}, x)))$ the composite $μ_{X} \circ T (μ_{X})$ gives $(g_{1} (g_{2} g_{3}), x)$ and $μ_{X} \circ μ_{T X}$ gives $((g_{1} g_{2}) g_{3}, x)$ , and these agree because multiplication in $G$ is associative.

L1givenstep 1.1step 1.2

2.2

The unit laws hold componentwise: on $(g, x)$ the composite $μ_{X} \circ T (η_{X})$ gives $(g u, x)$ and $μ_{X} \circ η_{T X}$ gives $(u g, x)$ , and both equal $(g, x)$ because $u$ is a two-sided identity of $G$ . Hence $(T, η, μ)$ is a monad by [L1].

L1givenstep 1.1step 1.2

3.1

Let $h : G \times X \to X$ be a structure map. By [L2] the unit law $h \circ η_{X} = 1_{X}$ says $h (u, x) = x$ for every $x$ , and the associativity law $h \circ T (h) = h \circ μ_{X}$ evaluated at $(g_{1}, (g_{2}, x))$ says $h (g_{1}, h (g_{2}, x)) = h (g_{1} g_{2}, x)$ . Writing $g \cdot x : = h (g, x)$ , these are exactly the two clauses of [L3], so $h$ is a left action of $G$ on $X$ .

L2L3step 2.1step 2.2

4.1

Conversely, a left action of $G$ on $X$ is a function $h : G \times X \to X$ with $h (u, x) = x$ and $h (g_{1} g_{2}, x) = h (g_{1}, h (g_{2}, x))$ by [L3], which are the two $T$ -algebra laws of [L2] read backwards. So the $T$ -algebras with underlying set $X$ are precisely the left actions of $G$ on $X$ .

L2L3step 3.1

5.1

For algebras $(X, h)$ and $(Y, k)$ and a function $f : X \to Y$ , the homomorphism condition $f \circ h = k \circ T (f)$ of [L2] evaluated at $(g, x)$ reads $f (h (g, x)) = k (g, f (x))$ , that is $f (g \cdot x) = g \cdot f (x)$ , which is $G$ -equivariance in the sense of [L4].

L2L4step 3.1step 4.1

6.1

By [L6] the Eilenberg–Moore category of this monad therefore has the $G$ -sets as objects and the $G$ -equivariant maps as morphisms. This proves the stated claim.

L6step 4.1step 5.1∎

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: 35 results over 14 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

S. Mac Lane, Categories for the Working Mathematician, 2nd ed., §VI.2, Group actions (standard reference, not scraped)

For a group GG the monad G×(−)G×(−) on sets has the GG-sets as its algebras