Context
2-category theory
2-category theory
Definitions
Transfors between 2-categories
Morphisms in 2-categories
Structures in 2-categories
Limits in 2-categories
Structures on 2-categories
Idea
A lax-idempotent 2-monad generalizes the notion of idempotent monad to 2-categories by replacing inverses with adjoints. A lax-idempotent 2-adjunction (or KZ 2-adjunction) similarly generalizes the notion of idempotent adjunction, and is related to lax-idempotent 2-monads in the same way that idempotent adjunctions are related to idempotent monads.
Definition
We will need to use all three kinds of composition in the 3-category . We write composition along 0-cells (2-functors, denoted with upper case Latin letters) with juxtaposition. We write composition along 1-cells (functors, denoted with lower case Greek letters) with a dot; this is of course composition along 0-cells in a 2-category. And we write composition along 2-cells (transformations, denoted with lower case Latin letters) with , which is composition along 1-cells in a 2-category.
Let be a 2-adjunction with unit and counit . (For simplicity, we will assume it is a strict 2-adjunction, but the same definitions and proofs work in the pseudo case with some equalities replaced by isomorphisms.) Write and and and .
The 2-adjunction is said to be lax-idempotent if one (hence all) of the following equivalent conditions hold (of which the latter 7 are dual to the former 7; the duality involves reversing 2-cells).
-
The triangle identity is the unit of an adjunction .
-
The induced equality is the unit of an adjunction .
In monad notation: the induced equality is the unit of an adjunction .
-
The induced equality is the unit of an adjunction .
In comonad notation: the induced equality is the unit of an adjunction .
-
The induced 2-monad is lax-idempotent, meaning that every strict Eilenberg-Moore algebra has the property that the identity is the unit of an adjunction .
-
There is a modification such that and .
In monad notation: there is a modification such that and .
-
There is a modification such that and .
-
There is a modification such that and .
And the duals (which we will refer to below using a prime, i.e. 1’-7’):
-
The triangle identity is the counit of an adjunction .
-
The induced equality is the counit of an adjunction .
In comonad notation: the induced equality is the counit of an adjunction .
-
The induced equality is the counit of an adjunction .
In monad notation: the induced equality is the counit of an adjunction .
-
The induced 2-comonad is colax-idempotent, meaning that every strict Eilenberg-Moore coalgebra has the property that the identity is the counit of an adjunction .
-
There is a modification such that and .
In comonad notation: there is a modification such that and .
-
There is a modification such that and .
-
There is a modification such that and .
Proof of equivalence
First of all, note that, by uniqueness of the left/right adjoint, most of the properties listed are (essentially) mere propositions. So we will content ourselves with proving logical equivalence.
We first prove , which by duality implies that 1, 2, 5, 6, 1’, 2’, 5’ and 6’ are equivalent.
-
() Trivial by whiskering.
-
() We have with unit and counit . Let . This satisfies the equations:
-
by an adjunction law.
-
.
-
() Trivial by whiskering.
-
() We take the unit of the desired adjunction to be
This satisfies the required triangle identities:
-
,
-
.
We now prove , adding and to the set of equivalent properties.
-
() Trivial by whiskering.
-
() We have with unit and counit . Let . This satisfies the equations:
-
.
-
.
We now prove , adding and to the set of equivalent properties.
-
() Trivial by whiskering.
-
() We take the counit of the desired adjunction to be
This satisfies the required triangle identities:
-
,
-
.
Finally, we prove that is equivalent to (hence dually, is equivalent to ).
-
() Let be an algebra. Then . We will carry over the structure of by conjugating with . For , we have
-
,
-
.
Define
- .
This satisfies the adjunction laws:
-
.
-
.
-
() This is immediate, since is always a strict Eilenberg-Moore algebra.
Note that when and are locally discrete, hence just 1-categories, this reduces to the usual characterization of idempotent adjunctions.
In contrast to that situation, however, the lax-idempotent situation is of interest even when the adjunction is monadic or comonadic. In the monadic case, the implication means that the induced 2-comonad on the 2-category of algebras for a lax-idempotent 2-monad is colax-idempotent. Its (pseudo) coalgebras are the continuous algebras for the original 2-monad.
References
As “KZ-adjunctions”:
- J. Meseguer, U. Montanari, and V. Sassone. ω-Inductive completion of monoidal categories and infinite petri net computations. (1993) (pdf)
As “KZ-adjointness” (defined by both (1) and (6)):
As “lax idempotent 2-adjunctions”: