module Cat.Functor.Adjoint.Kan where

Adjoints preserve Kan extensions🔗

Let $L\rightleftarrows R$ be a pair of adjoint functors. It’s well-known that right adjoints preserve limits¹, and dually that left adjoints preserve colimits, but it turns out that this theorem can be made a bit more general: If $G$ is a left (resp. right) extension of $F$ along $p\text{,}$ then $LG$ is a left extension of $LF$ along $p\text{:}$ 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 $L⊣R$ adjunction provides a bunch of isomorphisms between natural transformations, e.g. $(LF\to Mp)\cong (F\to RMp)\text{,}$ 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 $L\eta \text{.}$ Unfortunately, proof assistants; Our existing definition of whiskering lands in $L(Gp)\text{,}$ but we need a natural transformation onto $(LG)p\text{.}$

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

Given a 2-cell $\alpha :LF\to Mp\text{,}$ how do we factor it through $\eta$ as a 2-cell $\sigma :LG\to M\text{?}$ Well, since the original diagram was an extension, if we can get our hands on a 2-cell $F\to M^{\prime }p\text{,}$ that’ll give us a cell $G\to M^{\prime }\text{.}$ Hm: choose $M^{\prime }=RM\text{,}$ let ${\alpha }^{\prime }:F\to (RM)p$ be the adjunct of $\alpha \text{,}$ factor it through the original $\eta$ into a cell ${\sigma }^{\prime }:G\to RM\text{,}$ and let $\sigma :LG\to M$ 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 $LG$ is the extension of $LF$ along $p\text{!}$

    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                                 ∎
      where
        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 (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.

  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