Alphabeta MathHow 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 induced by the free-monoid adjunction sends a set to the set of finite words, inserts letters as one-letter words, and flattens words of words by concatenation. Its Eilenberg–Moore category is isomorphic over to the category of monoids.
Facts & Assumptions
Given: The free-monoid adjunction between sets and monoids.
The free-monoid functor sends to the monoid of finite words and is left adjoint to the underlying-set functor (The free-monoid functor is left adjoint to the underlying-set functor).
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).
A monoid has an associative binary operation and a two-sided identity (Semigroup and monoid).
Proof
By [L1]–[L2], the induced endofunctor is , its unit sends a letter to its one-letter word, and its multiplication concatenates a finite word of finite words. A monoid therefore gives an algebra by evaluating each word.
Conversely, for an algebra , define and . 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.
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.
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 canonical free-algebra presentation of a two-element idempotent monoid Example
- The free-monoid monad as a monoid object in the endofunctor category 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
- Monoids and unital rings are strictly monadic over sets Theorem
- The canonical algebra presentation is split in the base, but its canonical splittings need not be algebra homomorphisms Theorem
Dependency tree · two levels
12 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.2.6(i) (standard reference, not scraped)