module Cat.Functor.Adjoint.Continuous where

Continuity of adjoints🔗

We prove that every functor $R : D \to C$ admitting a left adjoint $L ⊣ R$ preserves every limit which exists in $D .$ We then instantiate this theorem to the “canonical” shapes of limit: terminal objects, products, pullback and equalisers.

This follows directly from the fact that adjoints preserve Kan extensions.

  right-adjoint-is-continuous
    : ∀ {os ℓs} → is-continuous os ℓs R
  right-adjoint-is-continuous lim =
    right-adjoint→right-extension lim L⊣R

  left-adjoint-is-cocontinuous
    : ∀ {os ℓs} → is-cocontinuous os ℓs L
  left-adjoint-is-cocontinuous colim =
    left-adjoint→left-extension colim L⊣R

  module _ {od ℓd} {J : Precategory od ℓd} where
    right-adjoint-limit : ∀ {F : Functor J D} → Limit F → Limit (R F∘ F)
    right-adjoint-limit lim =
      to-limit (right-adjoint-is-continuous (Limit.has-limit lim))

    left-adjoint-colimit : ∀ {F : Functor J C} → Colimit F → Colimit (L F∘ F)
    left-adjoint-colimit colim =
      to-colimit (left-adjoint-is-cocontinuous (Colimit.has-colimit colim))

Concrete limits🔗

We now show that adjoint functors preserve “concrete limits”. We could show this using general abstract nonsense, but we can avoid transports if we do it by hand.

  right-adjoint→is-product
    : ∀ {x a b} {p1 : D.Hom x a} {p2 : D.Hom x b}
    → is-product D p1 p2
    → is-product C (R.₁ p1) (R.₁ p2)
  right-adjoint→is-product {x = x} {a} {b} {p1} {p2} d-prod = c-prod where
    open is-product

    c-prod : is-product C (R.₁ p1) (R.₁ p2)
    c-prod .⟨_,_⟩ f g =
      L-adjunct L⊣R (d-prod .⟨_,_⟩ (R-adjunct L⊣R f) (R-adjunct L⊣R g))
    c-prod .π₁∘factor =
      R.pulll (d-prod .π₁∘factor) ∙ L-R-adjunct L⊣R _
    c-prod .π₂∘factor =
      R.pulll (d-prod .π₂∘factor) ∙ L-R-adjunct L⊣R _
    c-prod .unique other p q =
      sym (L-R-adjunct L⊣R other)
      ∙ ap (L-adjunct L⊣R)
           (d-prod .unique _ (R-adjunct-ap L⊣R p) (R-adjunct-ap L⊣R q))

  right-adjoint→is-pullback
    : ∀ {p x y z}
    → {p1 : D.Hom p x} {f : D.Hom x z} {p2 : D.Hom p y} {g : D.Hom y z}
    → is-pullback D p1 f p2 g
    → is-pullback C (R.₁ p1) (R.₁ f) (R.₁ p2) (R.₁ g)
  right-adjoint→is-pullback {p1 = p1} {f} {p2} {g} d-pb = c-pb where
    open is-pullback

    c-pb : is-pullback C (R.₁ p1) (R.₁ f) (R.₁ p2) (R.₁ g)
    c-pb .square = R.weave (d-pb .square)
    c-pb .universal sq =
      L-adjunct L⊣R (d-pb .universal (R-adjunct-square L⊣R sq))
    c-pb .p₁∘universal =
      R.pulll (d-pb .p₁∘universal) ∙ L-R-adjunct L⊣R _
    c-pb .p₂∘universal =
      R.pulll (d-pb .p₂∘universal) ∙ L-R-adjunct L⊣R _
    c-pb .unique {_} {p₁'} {p₂'} {sq} {other} p q =
      sym (L-R-adjunct L⊣R other)
      ∙ ap (L-adjunct L⊣R)
           (d-pb .unique (R-adjunct-ap L⊣R p) (R-adjunct-ap L⊣R q))

  right-adjoint→is-equaliser
    : ∀ {e a b} {f g : D.Hom a b} {equ : D.Hom e a}
    → is-equaliser D f g equ
    → is-equaliser C (R.₁ f) (R.₁ g) (R.₁ equ)
  right-adjoint→is-equaliser {f = f} {g} {equ} d-equal = c-equal where
    open is-equaliser

    c-equal : is-equaliser C (R.₁ f) (R.₁ g) (R.₁ equ)
    c-equal .equal = R.weave (d-equal .equal)
    c-equal .universal sq =
      L-adjunct L⊣R (d-equal .universal (R-adjunct-square L⊣R sq))
    c-equal .factors =
      R.pulll (d-equal .factors) ∙ L-R-adjunct L⊣R _
    c-equal .unique p =
      sym (L-R-adjunct L⊣R _)
      ∙ ap (L-adjunct L⊣R)
           (d-equal .unique (R-adjunct-ap L⊣R p))

  right-adjoint→terminal
    : ∀ {x} → is-terminal D x → is-terminal C (R.₀ x)
  right-adjoint→terminal term x = contr fin uniq where
    fin = L-adjunct L⊣R (term (L.₀ x) .centre)
    uniq : ∀ x → fin ≡ x
    uniq x = ap fst $ is-contr→is-prop (R-adjunct-is-equiv L⊣R .is-eqv _)
      (_ , equiv→counit (R-adjunct-is-equiv L⊣R) _)
      (x , is-contr→is-prop (term _) _ _)

  right-adjoint→lex : is-lex R
  right-adjoint→lex .is-lex.pres-⊤ =
    right-adjoint→terminal
  right-adjoint→lex .is-lex.pres-pullback {f = f} {g = g} pb =
    right-adjoint→is-pullback pb