TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 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.

The free-monoid monad has monoids as its Eilenberg–Moore algebras

Statement

The monad on $S e t$ induced by the free-monoid adjunction sends a set $X$ to the set $X^{*}$ of finite words, inserts letters as one-letter words, and flattens words of words by concatenation. Its Eilenberg–Moore category is isomorphic over $S e t$ to the category of monoids.

Facts & Assumptions

Given: The free-monoid adjunction between sets and monoids.

[L1]

The free-monoid functor sends $X$ to the monoid of finite words $X^{*}$ and is left adjoint to the underlying-set functor (The free-monoid functor is left adjoint to the underlying-set functor).

[L2]

Every adjunction induces a monad, whose unit is the adjunction unit and whose multiplication uses the counit (Every adjunction induces a monad on the domain of its left adjoint).

[L3]

A monoid has an associative binary operation and a two-sided identity (Semigroup and monoid).

Proof

technique · direct

1.1

By [L1]–[L2], the induced endofunctor is $X \mapsto X^{*}$ , its unit sends a letter to its one-letter word, and its multiplication concatenates a finite word of finite words. A monoid $M$ therefore gives an algebra $M^{*} \to M$ by evaluating each word.

L1L2

2.1

Conversely, for an algebra $a : X^{*} \to X$ , define $e = a ([])$ and $x \cdot y = a ([x, y])$ . The algebra unit law evaluates one-letter words to their letters, and the multiplication law says evaluation is unchanged by first evaluating subwords; applied to empty, two-letter, and three-letter decompositions, it gives the two unit laws and associativity.

L3step 1.1

3.1

An algebra homomorphism commutes with evaluation, hence preserves the empty word and two-letter words and is a monoid homomorphism. Conversely a monoid homomorphism preserves every finite word evaluation, so it is an algebra homomorphism. These identifications are inverse and unchanged on underlying sets.

L3step 1.1step 2.1∎

Depends on

Used by

A two-element idempotent monoid is an algebra for the free-monoid monad but is not free Counterexample
A Kleisli composite for the list monad computed by substitution and concatenation Example
The list monad on a two-element set Example
FALSE: Every algebra for a monad is free False statement
FALSE: The Kleisli and Eilenberg–Moore categories are equivalent for every monad False statement

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 28 results over 9 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

E. Riehl, Category Theory in Context, 2nd ed., Example 5.2.6(i) (standard reference, not scraped)