TheoremStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Groups are strictly monadic over sets

Statement

The underlying-set functor $U : G r p \to S e t$ is strictly monadic, and hence monadic.

Facts & Assumptions

Given: The free-group adjunction and its comparison functor.

[L1]

The Eilenberg–Moore category of the free-group monad is isomorphic over $S e t$ to the category of groups (The free-group monad has groups as its Eilenberg–Moore algebras).

[L2]

A functor is strictly monadic when its comparison functor is an isomorphism of categories (Monadic and strictly monadic functors).

[L3]

The comparison functor is $K (d) = (U d, U ε_{d})$ and acts on morphisms by $K (h) = U (h)$ (The comparison functor to the Eilenberg–Moore category exists and is unique).

[L4]

Choosing a free group $(F (X), i_{X})$ on every set $X$ makes $F$ left adjoint to the underlying-set functor $U$ , the adjunction bijection sending $φ : F (X) \to G$ to $U (φ) i_{X}$ (The free-group functor is left adjoint to the underlying-set functor).

[L5]

An algebra $(A, a)$ for a monad $(T, η, μ)$ satisfies $a η_{A} = 1_{A}$ and $a T (a) = a μ_{A}$ , and an algebra homomorphism is a map commuting with the two structure maps (Algebra and algebra homomorphism for a monad).

Proof

technique · direct

1.1

By [L3], $K (G) = (U G, U ε_{G})$ and $K (h) = U (h)$ . Under [L4] the counit $ε_{G}$ corresponds to the identity of $U G$ , so it is the unique group homomorphism $F (U G) \to G$ carrying each basis element $g$ to $g$ ; a homomorphism out of a free group is determined by its values on the basis, so $ε_{G}$ evaluates a reduced word in the elements of $G$ to its product in $G$ . Hence $K (G)$ is the underlying set of $G$ with word evaluation.

L3L4construct

2.1

A function $f : U G \to U H$ commutes with word evaluation exactly when it is a group homomorphism: evaluating the words $[x, y]$ , the empty word and $[x^{- 1}]$ turns commutation into preservation of product, identity and inverse, and conversely a homomorphism preserves the value of every word. With [L5] and $K (h) = U (h)$ this makes $K$ bijective on the morphisms between any two groups.

step 1.1L5algebra

2.2

$K$ is injective on objects, since step 1.1 recovers the product of $G$ from $U ε_{G}$ as its value on two-letter words.

step 1.1

2.3

$K$ is surjective on objects. Let $(A, a)$ be an algebra for the free-group monad. Put $x \cdot y : = a ([x, y])$ , $1 : = a ([])$ and $x^{- 1} : = a ([x^{- 1}])$ . Writing a word as the concatenation of its first letter with its tail and applying the multiplication law $a T (a) = a μ_{A}$ of [L5] to the corresponding word of words gives $a (w) = a ([x_{1}]) \cdot a (tail)$ , while the unit law $a η_{A} = 1_{A}$ gives $a ([x]) = x$ ; induction on length therefore identifies $a$ with evaluation of words in the operations just defined. Substituting the group-word identities into the same multiplication law turns them into associativity, the unit laws and the inverse laws, so those operations make $A$ a group $G_{A}$ with $a = U ε_{G_{A}}$ , that is $(A, a) = K (G_{A})$ .

step 1.1L5construct

3.1

By steps 2.1, 2.2 and 2.3 the comparison is bijective on objects and on morphisms, hence an isomorphism of categories over $S e t$ ; the isomorphism over $S e t$ asserted by [L1] may therefore be taken to be $K$ . So $U$ is strictly monadic by [L2], and strict monadicity implies monadicity.

step 2.1step 2.2step 2.3L1L2∎

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

E. Riehl, Category Theory in Context, 2nd ed., Example 5.1.4(iv) and Corollary 5.5.3(i) (standard reference, not scraped)