module Cat.Functor.Adjoint.Continuous where

Continuity of adjointsπŸ”—

We prove that every functor admitting a left adjoint preserves every limit which exists in 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.

    : βˆ€ {os β„“s} β†’ is-continuous os β„“s R
  right-adjoint-is-continuous lim =
    right-adjointβ†’right-extension lim L⊣R

    : βˆ€ {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.

    : βˆ€ {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))

    : βˆ€ {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))

    : βˆ€ {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))

    : βˆ€ {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→lex .is-lex.pres-pullback {f = f} {g = g} pb =
    right-adjoint→is-pullback pb