ExampleConstruction: Literature-sourcedVerification: Literature-sourcedprecheck 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.1L1L5given

$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)))$ .

1.2L1given

$η$ 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))$ .

2.1L1givenstep 1.1step 1.2

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.

2.2L1givenstep 1.1step 1.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].

3.1L2L3step 2.1step 2.2

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$ .

4.1L2L3step 3.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$ .

5.1L2L4step 3.1step 4.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].

6.1L6step 4.1step 5.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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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

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