open import Cat.Functor.Kan.Duality
open import Cat.Functor.Coherence
open import Cat.Instances.Functor
open import Cat.Functor.Kan.Base
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module Cat.Functor.Adjoint.Kan where


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.

module
_ {oc βc oc' βc' od βd oa βa}
{C : Precategory oc βc} {C' : Precategory oc' βc'} {D : Precategory od βd}
{A : Precategory oa βa}
{p : Functor C C'}
{F : Functor C D}
{G : Functor C' D}
{eta : F => G Fβ p}
(lan : is-lan p F G eta)
{L : Functor D A} {R : Functor A D}
where
private
module l = is-lan lan
open is-lan
open _=>_
module A = Cr A
module D = Cr D
module L = Fr L
module R = Fr R
module F = Functor F
module G = Functor G
module p = Functor p

LF = L Fβ F
LG = L Fβ G
RL = R Fβ L
module RL = Functor RL
module LF = Functor LF
module LG = Functor LG

  left-adjointβleft-extension : preserves-lan L lan

    fixup : β {M : Functor C' A} β (LF => M Fβ p) β F => (R Fβ M) Fβ p
fixup {M = M} Ξ± .is-natural x y f =
(R.β (Ξ± .Ξ· y) D.β unit.Ξ· _) D.β F.β f            β‘β¨ D.pullr (unit.is-natural _ _ _) β©β‘
(R.β (Ξ± .Ξ· y) D.β (RL.β (F.β f)) D.β unit.Ξ· _)   β‘β¨ D.extendl (R.weave (Ξ± .is-natural _ _ _)) β©β‘
R.β (M.β (p.β f)) D.β R.β (Ξ± .Ξ· x) D.β unit.Ξ· _  β
where module M = Functor M


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 (counit.is-natural _ _ _) β©β‘
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 Ξ±} Ξ·β _) β©β‘
Ξ± .Ξ· x                                                  β

pres .Ο-uniq {M = M} {Ξ± = Ξ±} {Ο' = Ο'} wit = ext Ξ» x β
Ο' .Ξ· x                                 β
where
module M = Functor M

Ο'' : G => R Fβ M
Ο'' .is-natural x y f =
(R.β (Ο' .Ξ· _) D.β unit.Ξ· _) D.β G.β f          β‘β¨ D.pullr (unit.is-natural _ _ _) β©β‘
(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 (unit.is-natural _ _ _)) β©β‘
(R.β (Ο' .Ξ· _) D.β unit.Ξ· _) D.β eta .Ξ· x     β


## Duallyπ

By duality, right adjoints preserve right extensions.

module
_ {oc βc oc' βc' od βd oa βa}
{C : Precategory oc βc} {C' : Precategory oc' βc'} {D : Precategory od βd}
{A : Precategory oa βa} {p : Functor C C'} {F : Functor C D} {G : Functor C' D}
{eps : G Fβ p => F} (ran : is-ran p F G eps) {L : Functor A D} {R : Functor D A}
where

  right-adjointβright-extension : preserves-ran R ran
(is-ranβis-co-lan _ _ ran)

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β©οΈ