nLab monadic adjunction

Redirected from "structure-semantics adjunction".
Monadic adjunctions

Context

Higher algebra

2-Category theory

Monadic adjunctions

Idea

One can turn monads into adjunctions and adjunctions into monads (see there), but one doesn't always return where one started. Every monad comes from an adjunction, but only a monadic adjunction comes from a monad via a monadic functor. (To be fair, there are two ways to turn a monad into an adjunction, given by the Kleisli category and the Eilenberg–Moore category; we are talking about the latter here.)

Definition

We give the definitions in Cat and leave it to future readers and writers to generalise. See for instance (Riehl-Verity 13).

Let (C,D,,r,ι,ϵ)(C,D,\ell,r,\iota,\epsilon) be an adjunction in CatCat; that is, :CD\ell: C \to D and r:DCr: D \to C are adjoint functors with r\ell \dashv r, where ι\iota and ϵ\epsilon are the unit and counit. Let TT be rr \circ \ell; TT has the structure of a monad on CC, so consider the Eilenberg–Moore category C TC^T of modules (algebras) for TT. Then rϵ:Trrr \circ \epsilon: T \circ r \to r endows r:DCr: D \to C with a TT-algebra structure, hence defines a functor k:DC Tk: D \to C^T.

The adjunction r\ell \dashv r is monadic if this functor kk is an equivalence of categories.

Beck’s monadicity theorem

Beck’s Monadicity Theorem gives a necessary and sufficient condition for an adjunction to be monadic. Namely, the adjunction (C,D,,r,ι,ϵ)(C,D,\ell,r,\iota,\epsilon) is monadic iff:

  • rr reflects isomorphisms; and

  • DD has coequalizers of rr-split coequalizer pairs, and rr preserves those coequalizers.

See monadicity theorem for more details and variants.

Algebraic categories

The typical categories studied in algebra, such as Grp, Ring, etc, all come equipped with monadic adjunctions from Set. Specifically, the right adjoint is the forgetful functor from algebras to sets, and the left adjoint maps each set to the free algebra on that set. Their composite (a monad on SetSet) may be thought of as mapping a set AA to the set of words with alphabet taken from AA and the connections between letters taken from the appropriate algebraic operations, with two words identified if they can be proved equal by the appropriate algebraic axioms.

Abstractly, one may define an algebraic category to be a category equipped with a monadic adjunction from SetSet. However, there are now more examples than the ones from algebra; the best known of these is the category of compact Hausdorff spaces, which corresponds to the ultrafilter monad. (This result relies on the ultrafilter principle, regardless of whether one interprets ‘space’ here as referring to topological spaces or locales.)

Semantics-structure adjunction

The relationship between monads and adjunctions itself constitutes an adjunction called the semantics-structure adjunction. Explicitly, for a category CC there exist contravariant functors Str:Cat /C *Mon(C):SemStr:Cat_{/C}^*\to Mon(C):Sem with StrSemStr\dashv Sem where Cat /C *Cat_{/C}^* denotes the full subcategory of Cat /CCat_{/C} consisting of functors admitting a codensity monad; StrStr sends a functor to its corresponding codensity monad and SemSem sends a monad to the forgetful functor from its E-M category to CC. Intuitively speaking we may think of a monad on CC as a kind of structure with which the objects of CC can be equipped presented in a syntax-independent way, and we may think of the E-M category of a monad (viewed as a syntax-independent presentation of an equational theory) as the category of models of this theory, which is often referred to by logicians as the semantics of the theory. For more on this, see for instance section 5 of (Schäppi 2009).

Examples

  1. Eilenberg-Moore categories are obviously all examples, and up to equivalence, the only examples.
  2. If the categories are pre-orders, then a monadic adjunction is a Galois connection where the right adjoint reflects ordering and dually a comonadic adjunction is a Galois connection where the left adjoint reflects ordering.
  3. More generally an idempotent adjunction is monadic if and only if the right adjoint is fully faithful, i.e. essentially a reflective subcategory inclusion. Dually, a comonadic idempotent adjunction is essentially a coreflective subcategory inclusion.

References

Discussion for quasi-categories is around definition 6.1.15 and definition 7.1.6 in

Last revised on March 3, 2024 at 23:36:59. See the history of this page for a list of all contributions to it.