nLab
lax-idempotent 2-adjunction

Lax-idempotent 2-adjunctions

Lax-idempotent 2-adjunctions

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 2Cat2 Cat. We write composition along 0-cells (2-categories) with juxtaposition. We write composition along 1-cells (2-functors) with a dot; this is of course composition along 0-cells in a 2-category. And we write composition along 2-cells (transformations) with \circ, which is composition along 1-cells in a 2-category.

Let F:CD:GF : C \rightleftarrows D : G be a 2-adjunction with unit η:1 CGF\eta: 1_C \to G F and counit ϵ:FG1 D\epsilon: F G \to 1_D. (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.) This 2-adjunction is said to be lax-idempotent if one (hence all) of the following equivalent conditions hold.

  1. The triangle identity 1 F=ϵF.Fη1_F = \epsilon F . F\eta is the unit of an adjunction FηϵFF\eta \dashv \epsilon F.

  2. The induced equality 1 GF=GϵF.GFη1_{G F} = G \epsilon F . G F\eta is the unit of an adjunction GFηGϵFG F\eta \dashv G \epsilon F.

  3. The induced 2-monad GFG F is lax-idempotent.

  4. There is a modification δ:GFηηGF\delta : G F \eta \to \eta G F such that δη=1\delta \circ \eta = 1 and (GϵF)δ=1(G\epsilon F) \circ \delta = 1.

  5. There is a modification δ:GFηGηGFG\delta' : G F \eta G \to \eta G F G such that δ(ηG)=1\delta' \circ (\eta G) = 1 and (GϵFG)δ=1(G\epsilon F G) \circ \delta' = 1.

  6. The triangle identity Gϵ.ηGG \epsilon . \eta G is the counit of an adjunction GϵηGG \epsilon \dashv \eta G.

  7. The induced equality FGϵ.FηGF G \epsilon . F \eta G is the counit of an adjunction FGϵFηGF G \epsilon \dashv F \eta G.

  8. The induced 2-comonad FGF G is lax-idempotent.

  9. There is a modification δ:ϵFGFGϵ\delta : \epsilon F G \to F G \epsilon such that ϵδ=1\epsilon \circ \delta = 1 and δ(FηG)=1\delta \circ (F\eta G) = 1.

  10. There is a modification δ:GϵFGGFGϵ\delta' : G \epsilon F G \to G F G \epsilon such that (Gϵ)δ=1(G \epsilon) \circ \delta = 1 and δ(GFηG)=1\delta \circ (G F\eta G) = 1.

Proof of equivalence

By duality, it suffices to prove that 1234561\Rightarrow 2 \Rightarrow 3 \Rightarrow 4 \Rightarrow 5 \Rightarrow 6. Of these, 121\Rightarrow 2 and 454 \Rightarrow 5 are obvious by whiskering. And since GϵFG\epsilon F is the multiplication of the 2-monad GFG F, a standard fact about lax-idempotent 2-monads gives 2342\Leftrightarrow 3 \Leftrightarrow 4.

Thus, it remains to show 565 \Rightarrow 6. We take the unit of the desired adjunction to be

1 =triangleGFGϵ.GFηG δGFGϵ.ηGFG =naturalityηG.Gϵ \begin{aligned} 1 &\overset{triangle}{=} G F G \epsilon . G F \eta G\\ &\xrightarrow{\delta'} G F G \epsilon . \eta G F G\\ &\overset{naturality}{=} \eta G . G \epsilon \end{aligned}

The two triangle identities for this putative adjunction follow from the two axioms assumed for δ\delta'.

Note that when CC and DD 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 383\Rightarrow 8 means that the induced 2-comonad on the 2-category of algebras for a lax-idempotent 2-monad is again lax-idempotent. Its (pseudo) coalgebras are the continuous algebras for the original 2-monad.

References

  • Marta Bunge and Jonathon Funk, Singular Coverings of Toposes. In this book the notion is called a “KZ adjointness” and defined by both (1) and (6).

Last revised on November 22, 2013 at 06:16:15. See the history of this page for a list of all contributions to it.