TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

A distributive law makes the composite endofunctor a monad

Statement

If $λ : S T \Rightarrow T S$ is a distributive law of the monad $S$ over the monad $T$ , then $T S$ is a monad. Its unit is $η^{T} S \circ η^{S}$ and its multiplication is

$T S T S \overset{T λ S}{\to} T T S S \overset{μ^{T} S S}{\to} T S S \overset{T μ^{S}}{\to} T S .$

Facts & Assumptions

Given: Monads $S, T$ on $C$ and a distributive law $λ : S T \Rightarrow T S$ .

[L1]

A distributive law of $S$ over $T$ is a natural transformation $λ : S T \Rightarrow T S$ satisfying $λ \circ η^{S} T = T η^{S}$ and $λ \circ S η^{T} = η^{T} S$ , together with $λ \circ μ^{S} T = T μ^{S} \circ λ S \circ S λ$ and $λ \circ S μ^{T} = μ^{T} S \circ T λ \circ λ T$ (Distributive law between two monads).

[L2]

A monad consists of an endofunctor with a unit and multiplication satisfying the unit and associativity equations (Monad on a category).

[L3]

An $S$ -algebra map $a : S A \to A$ satisfies $a η_{A}^{S} = 1_{A}$ and $a S (a) = a μ_{A}^{S}$ , and an algebra homomorphism $f : (A, a) \to (B, b)$ satisfies $f a = b S (f)$ (Algebra and algebra homomorphism for a monad).

[L4]

The Eilenberg--Moore forgetful functor is the identity on underlying morphisms, hence is faithful (Eilenberg–Moore category of a monad).

[L5]

The Eilenberg--Moore adjunction of any monad induces that monad on the nose (The free–forgetful Eilenberg–Moore adjunction induces the given monad).

[L6]

If $F ⊣ G$ has unit $η$ and counit $ε$ and $F^{'} ⊣ G^{'}$ has unit $η^{'}$ and counit $ε^{'}$ , then $F^{'} F ⊣ G G^{'}$ with unit $\overset{ˉ}{η} = (G η^{'} F) \circ η$ and counit $\overset{ˉ}{ε} = ε^{'} \circ (F^{'} ε G^{'})$ (Adjunctions compose with the composite unit and counit formulas).

[L7]

For an adjunction $F ⊣ G$ with unit $η$ and counit $ε$ , the data $T : = G F$ , $η : 1 \Rightarrow T$ and $μ : = G ε F : T^{2} \Rightarrow T$ define a monad on the domain of $F$ (Every adjunction induces a monad on the domain of its left adjoint).

Proof

technique · lift $T$ to $S$-algebras and compose Eilenberg--Moore adjunctions

1.1L1L3

For an $S$ -algebra $(A, a)$ define the following lifted object and arrow assignment.

$\tilde{T} (A, a) = (T A, b_{A}), b_{A} : = T (a) \circ λ_{A} : S T A \to T A,$

Put $\tilde{T} (f) = T (f)$ on an $S$ -algebra homomorphism $f$ .

2.1L1L2L3step 1.1

The first distributive unit law gives the first identity below, and the first distributive multiplication law, naturality of $λ$ , and the $S$ -algebra laws give the second.

$b_{A} η_{T A}^{S} = T (a) T (η_{A}^{S}) = 1_{T A},$

and

$\begin{aligned} b_{A} μ_{T A}^{S} & = T (a) T (μ_{A}^{S}) λ_{S A} S (λ_{A}) \\ = T (a S (a)) λ_{S A} S (λ_{A}) \\ = T (a) λ_{A} S (T (a)) S (λ_{A}) = b_{A} S (b_{A}) . \end{aligned}$

Thus $(T A, b_{A})$ is an $S$ -algebra. If $f : (A, a) \to (B, b)$ is an $S$ -algebra homomorphism, then naturality of $λ$ gives

$T (f) b_{A} = T (b) T S (f) λ_{A} = T (b) λ_{B} S (T (f)) = b_{B} S (T (f)),$

so the assignment in step 1.1 is an endofunctor $\tilde{T} : C^{S} \to C^{S}$ .

3.1L1L3step 2.1

The second distributive unit law and naturality of $η^{T}$ give the following identity.

$b_{A} S (η_{A}^{T}) = T (a) λ_{A} S (η_{A}^{T}) = T (a) η_{S A}^{T} = η_{A}^{T} a,$

Thus each $η_{A}^{T} : (A, a) \to \tilde{T} (A, a)$ is an $S$ -algebra homomorphism.

3.2L1L3step 2.1

The second distributive multiplication law and naturality of $μ^{T}$ give the following identity.

$\begin{aligned} b_{A} S (μ_{A}^{T}) & = T (a) μ_{S A}^{T} T (λ_{A}) λ_{T A} \\ = μ_{A}^{T} T (T (a)) T (λ_{A}) λ_{T A} = μ_{A}^{T} T (b_{A}) λ_{T A} . \end{aligned}$

Hence each $μ_{A}^{T} : {\tilde{T}}^{2} (A, a) \to \tilde{T} (A, a)$ is also an $S$ -algebra homomorphism.

4.1L2L4step 3.1step 3.2

The underlying components of these two natural transformations are $η^{T}$ and $μ^{T}$ . Their monad equations hold in $C$ by [L2], and [L4] reflects those equalities. Therefore $(\tilde{T}, η^{T}, μ^{T})$ is a monad on $C^{S}$ .

5.1L5L6step 4.1

Take the Eilenberg--Moore adjunction $F^{S} ⊣ U^{S}$ and the Eilenberg--Moore adjunction $F^{\tilde{T}} ⊣ U^{\tilde{T}}$ . By [L5] they induce $S$ and $\tilde{T}$ , respectively, and by [L6] they compose to the following adjunction.

$F^{\tilde{T}} F^{S} ⊣ U^{S} U^{\tilde{T}} .$

6.1L5L6step 1.1step 5.1

The induced endofunctor is $T S$ . The composite-unit formula in [L6] gives $η^{T} S \circ η^{S}$ . Expanding the two Eilenberg--Moore counits in the composite-counit formula gives the following multiplication.

$T S T S \overset{T λ S}{\to} T T S S \overset{T T μ^{S}}{\to} T T S \overset{μ^{T} S}{\to} T S .$

Naturality of $μ^{T}$ at $μ^{S}$ identifies its last two arrows with

$T T S S \overset{μ^{T} S S}{\to} T S S \overset{T μ^{S}}{\to} T S,$

This is the multiplication in the Statement.

7.1L7step 6.1∎

By [L7], the endofunctor, unit, and multiplication computed in step 6.1 satisfy both unit laws and associativity, so they define the asserted monad on $T S$ .

Depends on

Used by

Adjoining one of two fixed points defines commuting closure-operator monads whose distributive law yields their composite Example

Dependency tree · two levels

14 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. Cheng, Distributive laws for Lawvere theories, Theorem 2.2 (standard reference, not scraped)