nLab lax-idempotent 2-adjunction

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-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 \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.) Write M=GFM = GF and μ=GϵF:M 2F\mu = G \epsilon F : M^2 \to F and C=FGC = FG and δ=FηG:CC 2\delta = F \eta G : C \to C^2.

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).

  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.

    In monad notation: the induced equality 1 M=μ.Mη1_M = \mu . M \eta is the unit of an adjunction MημM \eta \dashv \mu.

  3. The induced equality 1 FG=ϵFG.FηG1_{F G} = \epsilon F G . F \eta G is the unit of an adjunction FηGϵFGF \eta G \dashv \epsilon F G.

    In comonad notation: the induced equality 1 C=ϵC.δ1_C = \epsilon C . \delta is the unit of an adjunction δϵC\delta \dashv \epsilon C.

  4. The induced 2-monad M=GFM = G F is lax-idempotent, meaning that every strict Eilenberg-Moore algebra (A,α)(A, \alpha) has the property that the identity 1 A=α.η A1_A = \alpha . \eta_A is the unit of an adjunction αη A\alpha \dashv \eta_A.

  5. There is a modification w:GFηηGFw : G F \eta \to \eta G F such that w.η=1w . \eta = 1 and (GϵF).w=1(G\epsilon F) . w = 1.

    In monad notation: there is a modification w:MηηMw : M \eta \to \eta M such that w.η=1w . \eta = 1 and μ.w=1\mu . w = 1.

  6. There is a modification w:GFηGηGFGw' : G F \eta G \to \eta G F G such that w.(ηG)=1w' . (\eta G) = 1 and (GϵFG).w=1(G\epsilon F G) . w' = 1.

  7. There is a modification w:FGFηFηGFw'' : F G F \eta \to F \eta G F such that w.(Fη)=1w'' . (F \eta) = 1 and (FGϵF).w=1(F G \epsilon F) . w'' = 1.

And the duals (which we will refer to below using a prime, i.e. 1’-7’):

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

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

    In comonad notation: the induced equality Cϵ.δ=1 CC \epsilon . \delta = 1_C is the counit of an adjunction CϵδC \epsilon \dashv \delta.

  3. The induced equality GϵF.ηGF=1 GFG \epsilon F . \eta G F = 1_{G F} is the counit of an adjunction GϵFηGFG \epsilon F \dashv \eta G F.

    In monad notation: the induced equality μ.ηM=1 M\mu . \eta M = 1_M is the counit of an adjunction μηM\mu \dashv \eta M.

  4. The induced 2-comonad FGF G is colax-idempotent, meaning that every strict Eilenberg-Moore coalgebra (Z,ζ)(Z, \zeta) has the property that the identity ϵ Z.ζ=1 Z\epsilon_Z . \zeta = 1_Z is the counit of an adjunction ζϵ Z\zeta \dashv \epsilon_Z.

  5. There is a modification v:ϵFGFGϵv : \epsilon F G \to F G \epsilon such that ϵ.v=1\epsilon . v = 1 and v.(FηG)=1v . (F\eta G) = 1.

    In comonad notation: there is a modification v:ϵCCϵv : \epsilon C \to C \epsilon such that ϵ.v=1\epsilon . v = 1 and v.δ=1v . \delta = 1.

  6. There is a modification v:ϵFGFFGϵFv' : \epsilon F G F \to F G \epsilon F such that (ϵG).v=1(\epsilon G) . v' = 1 and v.(FηGF)=1v' . (F \eta G F) = 1.

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

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 125611 \Rightarrow 2 \Rightarrow 5 \Rightarrow 6 \Rightarrow 1', which by duality implies that 1, 2, 5, 6, 1’, 2’, 5’ and 6’ are equivalent.

  • (121 \Rightarrow 2) Trivial by whiskering.

  • (252 \Rightarrow 5) We have MημM \eta \dashv \mu with unit h=1:1 Mμ.Mηh = 1 : 1_M \to \mu . M \eta and counit e:Mη.μ1 M 2e : M \eta . \mu \to 1_{M^2}. Let w=e.ηM:MηηMw = e . \eta M : M \eta \to \eta M. This satisfies the equations:

    • w.η=e.ηM.η=e.Mη.η=(Mη.h) 1.η=1 Mη.ηw . \eta = e . \eta M . \eta = e . M \eta . \eta = (M \eta . h)^{-1} . \eta = 1_{M \eta . \eta} by an adjunction law.

    • μ.w=μ.e.ηM=(h.μ) 1.ηM=1 μ.ηM=1 1 M\mu . w = \mu . e . \eta M = (h . \mu)^{-1} . \eta M = 1_{\mu . \eta M} = 1_{1_M}.

  • (565 \Rightarrow 6) Trivial by whiskering.

  • (616 \Rightarrow 1') We take the unit h:1 GFGηG.Gϵh : 1_{G F G} \to \eta G . G \epsilon of the desired adjunction to be

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

    This satisfies the required triangle identities:

    • Gϵ.h=Gϵ.GFGϵ.w=Gϵ.GϵFG.w=Gϵ.1=1G \epsilon . h = G \epsilon . G F G \epsilon . w' = G \epsilon . G \epsilon F G . w' = G \epsilon . 1 = 1,

    • h.ηG=GFGϵ.w.ηG=GFGϵ.1=1h . \eta G = G F G \epsilon . w' . \eta G = G F G \epsilon . 1 = 1.

We now prove 1351 \Rightarrow 3 \Rightarrow 5', adding 33 and 33' to the set of equivalent properties.

  • (131 \Rightarrow 3) Trivial by whiskering.

  • (353 \Rightarrow 5') We have δϵC\delta \dashv \epsilon C with unit h=1:1 CϵC.δh = 1 : 1_C \to \epsilon C . \delta and counit e:δ.ϵC1 C 2e : \delta . \epsilon C \to 1_{C^2}. Let v=Cϵ.ev = C \epsilon . e. This satisfies the equations:

    • ϵ.v=ϵ.Cϵ.e=ϵ.ϵC.e=ϵ.(h.ϵC) 1=1 ϵ.ϵC\epsilon . v = \epsilon . C \epsilon . e = \epsilon . \epsilon C . e = \epsilon . (h . \epsilon C)^{-1} = 1_{\epsilon . \epsilon C}.

    • v.δ=Cϵ.e.δ=Cϵ.(δ.h) 1=1 1 Cv . \delta = C \epsilon . e . \delta = C \epsilon . (\delta . h)^{-1} = 1_{1_C}.

We now prove 5715 \Rightarrow 7 \Rightarrow 1, adding 77 and 77' to the set of equivalent properties.

  • (575 \Rightarrow 7) Trivial by whiskering.

  • (717 \Rightarrow 1) We take the counit e:Fη.ϵF1 FGFe : F \eta . \epsilon F \to 1_{F G F} of the desired adjunction to be

    Fη.ϵF =naturalityϵFGF.FGFη ϵFGF.wϵFGF.FηGF =triangle1 \begin{aligned} F \eta . \epsilon F &\overset{naturality}{=} \epsilon F G F . F G F \eta \\ &\xrightarrow{\epsilon F G F . w''} \epsilon F G F . F \eta G F \\ &\overset{triangle}{=} 1 \end{aligned}

    This satisfies the required triangle identities:

    • ϵF.e=ϵF.ϵFGF.w=ϵF.FGϵF.w=ϵF.1=1\epsilon F . e = \epsilon F . \epsilon F G F . w'' = \epsilon F . F G \epsilon F . w'' = \epsilon F . 1 = 1,

    • e.Fη=ϵFGF.w.Fη=ϵFGF.1=1e . F \eta = \epsilon F G F . w'' . F \eta = \epsilon F G F . 1 = 1.

Finally, we prove that 33' is equivalent to 44 (hence dually, 33 is equivalent to 44').

  • (343' \Rightarrow 4) Let (A,α)(A, \alpha) be an algebra. Then α.η A=1 A\alpha . \eta_A = 1_A. We will carry over the structure of (MA,μ A)(MA, \mu_A) by conjugating with α..η A\alpha . {-} . \eta_A. For MAMA, we have

    • e A=1 A:μ A.η MA1 MAe_A = 1_A : \mu_A . \eta_{MA} \to 1_{MA},

    • h A:1 M 2Aη MA.μ Ah_A : 1_{M^2 A} \to \eta_{MA} . \mu_A.

    Define

    • h=Mα.h A.Mη A:1 MA=Mα.Mη AMα.η MA.μ A.Mη A=Mα.η MA=η A.αh' = M \alpha . h_A . M\eta_A : 1_{MA} = M \alpha . M\eta_A \to M \alpha . \eta_{MA} . \mu_A . M\eta_A = M \alpha . \eta_{MA} = \eta_A . \alpha.

    This satisfies the adjunction laws:

    • α.h=α.Mα.h A.Mη A=α.μ A.h A.Mη A=α.(e A.μ A) 1.Mη A=α.1.Mη A=1\alpha . h' = \alpha . M \alpha . h_A . M\eta_A = \alpha . \mu_A . h_A . M\eta_A = \alpha . (e_A . \mu_A)^{-1} . M\eta_A = \alpha . 1 . M\eta_A = 1.

    • h.η A=Mα.h A.Mη A.η A=Mα.h A.η MA.η A=Mα.(η MA.e A) 1.η A=Mα.1.η A=1h' . \eta_A = M \alpha . h_A . M\eta_A . \eta_A = M \alpha . h_A . \eta_{MA} . \eta_A = M \alpha . (\eta_{MA} . e_A)^{-1} . \eta_A = M \alpha . 1 . \eta_A = 1.

  • (434 \Rightarrow 3') This is immediate, since (MX,μ X)(MX, \mu_X) is always a strict Eilenberg-Moore algebra.

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 444 \Rightarrow 4' 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”:

Last revised on August 7, 2023 at 19:21:01. See the history of this page for a list of all contributions to it.