module Cat.Functor.Adjoint.Kan where

Adjoints preserve Kan extensionsπŸ”—

Let be a pair of adjoint functors. It’s well-known that right adjoints preserve limits1, and dually that left adjoints preserve colimits, but it turns out that this theorem can be made a bit more general: If is a left (resp. right) extension of along then is a left extension of along left adjoints preserve left extensions. This dualises to right adjoints preserving right extensions.

The proof could be given in bicategorical generality: If the triangle below is a left extension diagram, then the overall pasted diagram is also a left extension. This is essentially because the adjunction provides a bunch of isomorphisms between natural transformations, e.g.Β  which we can use to β€œgrow” the original extension diagram.

  left-adjoint→left-extension : preserves-lan L lan
  left-adjoint→left-extension = pres where

It wouldn’t fit in the diagram above, but the 2-cell of the larger diagram is simply the whiskering Unfortunately, proof assistants; Our existing definition of whiskering lands in but we need a natural transformation onto

    pres : is-lan p (L F∘ F) (L F∘ G) (nat-assoc-to (L β–Έ eta))

Given a 2-cell how do we factor it through as a 2-cell Well, since the original diagram was an extension, if we can get our hands on a 2-cell that’ll give us a cell Hm: choose let be the adjunct of factor it through the original into a cell and let be its adjunct.

    pres .Οƒ Ξ± .Ξ· x = R-adjunct adj (l.Οƒ (fixup Ξ±) .Ξ· x)
    pres .Οƒ {M = M} Ξ± .is-natural x y f =
      (Ξ΅ _ A.∘ L.₁ (l.Οƒ (fixup Ξ±) .Ξ· y)) A.∘ LG.₁ f        β‰‘βŸ¨ A.pullr (L.weave (l.Οƒ (fixup Ξ±) .is-natural x y f)) βŸ©β‰‘
      Ξ΅ _ A.∘ (L.₁ (RM.₁ f) A.∘ L.₁ (l.Οƒ (fixup Ξ±) .Ξ· x))  β‰‘βŸ¨ A.extendl ( _ _ _) βŸ©β‰‘
      M.₁ f A.∘ pres .Οƒ Ξ± .Ξ· x                             ∎
      where module M = Functor M
            module RM = Functor (R F∘ M)

And since every part of the process in the preceeding paragraph is an isomorphism, this is indeed a factorisation, and it’s unique to boot: we’ve shown that is the extension of along

The details of the calculation is just some more calculation with natural transformations. We’ll leave them here for the intrepid reader but they will not be elaborated on.
    pres .Οƒ-comm {Ξ± = Ξ±} = ext Ξ» x β†’
      (R-adjunct adj (l.Οƒ (fixup Ξ±) .Ξ· _)) A.∘ L.₁ (eta .Ξ· _) β‰‘βŸ¨ L.pullr (l.Οƒ-comm {Ξ± = fixup Ξ±} Ξ·β‚š _) βŸ©β‰‘
      R-adjunct adj (L-adjunct adj (Ξ± .Ξ· x))                  β‰‘βŸ¨ equivβ†’unit (L-adjunct-is-equiv adj) (Ξ± .Ξ· x) βŸ©β‰‘
      α .η x                                                  ∎

    pres .Οƒ-uniq {M = M} {Ξ± = Ξ±} {Οƒ' = Οƒ'} wit = ext Ξ» x β†’
      R-adjunct adj (l.Οƒ (fixup Ξ±) .Ξ· x)      β‰‘βŸ¨ A.refl⟩∘⟨ ap L.₁ (l.Οƒ-uniq lemma Ξ·β‚š x) βŸ©β‰‘
      R-adjunct adj (L-adjunct adj (Οƒ' .Ξ· x)) β‰‘βŸ¨ equivβ†’unit (L-adjunct-is-equiv adj) (Οƒ' .Ξ· x) βŸ©β‰‘
      Οƒ' .Ξ· x                                 ∎
        module M = Functor M

        Οƒ'' : G => R F∘ M
        Οƒ'' .Ξ· x = L-adjunct adj (Οƒ' .Ξ· x)
        Οƒ'' .is-natural x y f =
          (R.₁ (Οƒ' .Ξ· _) D.∘ unit.Ξ· _) D.∘ G.₁ f          β‰‘βŸ¨ D.pullr ( _ _ _) βŸ©β‰‘
          (R.₁ (Οƒ' .Ξ· _) D.∘ (RL.₁ (G.₁ f)) D.∘ unit.Ξ· _) β‰‘βŸ¨ D.extendl (R.weave (Οƒ' .is-natural _ _ _)) βŸ©β‰‘
          R.₁ (M.₁ f) D.∘ R.₁ (Οƒ' .Ξ· x) D.∘ unit.Ξ· _      ∎

        lemma : fixup Ξ± ≑ ((Οƒ'' β—‚ p) ∘nt eta)
        lemma = ext Ξ» x β†’
          R.₁ (Ξ± .Ξ· x) D.∘ unit.Ξ· _                     β‰‘βŸ¨ ap R.₁ (wit Ξ·β‚š _) D.⟩∘⟨refl βŸ©β‰‘
          R.₁ (Οƒ' .Ξ· _ A.∘ L.₁ (eta .Ξ· _)) D.∘ unit.Ξ· _ β‰‘βŸ¨ ap (D._∘ unit.Ξ· _) (R.F-∘ _ _) βˆ™ D.extendr (sym ( _ _ _)) βŸ©β‰‘
          (R.₁ (Οƒ' .Ξ· _) D.∘ unit.Ξ· _) D.∘ eta .Ξ· x     ∎


By duality, right adjoints preserve right extensions.

  right-adjoint→right-extension : preserves-ran R ran
  right-adjoint→right-extension = fixed where
    pres-lan = left-adjoint→left-extension
      (is-ran→is-co-lan _ _ ran)
      (opposite-adjunction adj)

    module p = is-lan pres-lan
    open is-ran
    open _=>_

    fixed : is-ran p (R F∘ F) (R F∘ G) (nat-assoc-from (R β–Έ eps))
    fixed .is-ran.Οƒ {M = M} Ξ± = Οƒ' where
      unquoteDecl Ξ±' = dualise-into Ξ±'
        (Functor.op R F∘ Functor.op F => Functor.op M F∘ Functor.op p)
      unquoteDecl Οƒ' = dualise-into Οƒ' (M => R F∘ G) (p.Οƒ Ξ±')

    fixed .is-ran.Οƒ-comm = ext Ξ» x β†’ p.Οƒ-comm Ξ·β‚š _
    fixed .is-ran.Οƒ-uniq {M = M} {Οƒ' = Οƒ'} p =
      ext Ξ» x β†’ p.Οƒ-uniq {Οƒ' = dualise! Οƒ'} (reext! p) Ξ·β‚š x

  1. Here on the 1Lab, we derive the proof that right (resp. left) adjoints preserve limits (resp. colimits) from this proof that adjoints preserve Kan extensions. For a more concrete approach to that proof, we recommend the nLab’sβ†©οΈŽ