The Eilenberg–Moore category as a displayed category

Fix a monad $(𝑇, 𝜂, 𝜇)$ on $𝒞︀$ . Its Eilenberg–Moore category arises in two displayed layers. The first layer is the displayed category of algebras $AlgStr (𝑇)$ of the underlying endofunctor.

The second layer, $EMStr (𝑇)$ , is displayed over the total category $Alg (𝑇)$ . Over an algebra $(𝑥, 𝛼)$ the displayed objects are the propositions that $𝛼$ satisfies the monad algebra laws:

𝜂_{𝑥} ⋆ 𝛼 = {𝗂𝖽}_{𝑥} 𝜇_{𝑥} ⋆ 𝛼 = 𝑇 𝛼 ⋆ 𝛼 .

The Eilenberg–Moore category is the total category of the tower:

EM (𝑇) = \int EMStr (𝑇) .

Backlinks

The co-Eilenberg–Moore category as a displayed category
The comparison functor of an adjunction
Monadicity and comonadicity
Presheaves are monadic and comonadic over families
Total category

Definitions

EMStr value

typst · 1 line

#let EMStr = [$"EMStr"$]

EM value

typst · 1 line

#let EM = [$"EM"$]