module Cat.Functor.Kan.Pointwise where

Pointwise Kan extensions🔗

One useful perspective on Kan extensions is that they are generalizations of (co)limits; in fact, we have defined (co)limits as a special case of Kan extensions! This means that many theorems involving (co)limits can be directly generalized to theorems of Kan extensions. A concrete example of this phenomena is the fact that right adjoints don’t just preserve limits, they preserve all right extensions!

However, this pattern of generalization fails in one critical way: corepresentable functors preserve limits, but corepresentable functors do not necessarily preserve Kan extensions! This seemingly slight issue has far-reaching consequences, to the point that some authors write off general Kan extensions entirely.

Instead of throwing the whole thing out, an alternative is to focus on only the Kan extensions that are preserved by arbitrary (co)representables; we call such extensions pointwise.

  is-pointwise-lan : ∀ {eta : G => E F∘ F} → is-lan F G E eta → Type _
  is-pointwise-lan lan =
    ∀ (x : D.Ob) → preserves-lan (Functor.op (Hom-into D x)) lan

  is-pointwise-ran : ∀ {eps : E F∘ F => G} → is-ran F G E eps → Type _
  is-pointwise-ran ran =
    ∀ (x : D.Ob) → preserves-ran (Hom-from D x) ran

Absolute Kan extensions are trivially pointwise, since they are preserved by all functors.

    : {eta : G => E F∘ F}
    → {lan : is-lan F G E eta}
    → is-absolute-lan lan
    → is-pointwise-lan lan
  absolute-lan→pointwise abs _ = abs _

    : {eps : E F∘ F => G}
    → {ran : is-ran F G E eps}
    → is-absolute-ran ran
    → is-pointwise-ran ran
  absolute-ran→pointwise abs _ = abs _

As noted earlier, limits and colimits are pointwise Kan extensions.

    : {eps : Const x => Dia}
    → (lim : is-limit Dia x eps)
    → is-pointwise-ran lim
  limit→pointwise lim x = Hom-from-preserves-limits x lim

    : {eta : Dia => Const x}
    → (colim : is-colimit Dia x eta)
    → is-pointwise-lan colim
  colimit→pointwise colim x = よ-reverses-colimits x colim

Computing pointwise extensions🔗

One useful fact about pointwise left Kan extensions (resp. right) is that they can be computed via colimits (resp. limits). We will focus on the left extensions for the moment. Given functors and if is a category, is locally and has colimits, then exists and is pointwise.

The big idea of our construction is to approximate by gluing together “all the ways that is able to see through ”. Concretely, this means looking at the comma category for a given Objects in this category are pairs of an object and morphisms If we apply the “domain” projection we obtain a diagram in encoding the hand-wavy intuition from before.

To finish the construction, we take our diagram in and post-compose with to obtain a diagram

Since is put together out of objects in and morphisms in it is also a category, so these diagrams all have colimits in

    ↓Dia : (c' : C'.Ob) → Functor (F ↘ c') D
    ↓Dia c' = G F∘ Dom F (Const c')

In fact, we can weaken the precondition from cocompleteness of to having colimits of these comma-category-shaped diagrams.

    : (∀ (c' : C'.Ob) → Colimit (↓Dia c'))
    → Lan F G
  comma-colimits→lan ↓colim = lan module comma-colimits→lan where
      module ↓colim c' = Colimit (↓colim c')

Taking the colimit at each gives an assignment of objects so we’re left with extending it to a proper functor Coming up with morphisms in the image of isn’t too complicated, and universality of colimits guarantees the functoriality constraints are satisfied.

      F' : Functor C' D
      F' .F₀ c' = ↓colim.coapex c'
      F' .F₁ f = ↓colim.universal _
        (λ j → ↓colim.ψ _ (↓obj (f C'.∘ j .map)))
        (λ f → ↓colim.commutes _ (↓hom {ÎČ = f .ÎČ} (C'.pullr (f .sq)
            ·· C'.elim-inner refl
            ·· sym (C'.idl _))))

Next, we need to show that the functor we constructed actually is a left extension. The first step will be to construct a “unit” natural transformation which, in components, means we’re looking for maps Since each is a colimit, we can use the coprojections!

      eta : G => F' F∘ F
      eta .η c = ↓colim.ψ (F .F₀ c) (↓obj C'.id)

This “type checks” because the colimit coprojections for our essentially, convert maps into maps If we take the identity we get what we wanted: a map

      eta .is-natural x y f =
        ↓colim.commutes (F .F₀ y) (↓hom (ap (C'.id C'.∘_) (sym (C'.idr _))))
        ∙ sym (↓colim.factors _ _ _)

For the other obligation, suppose we’re given some and natural transformation How do we extend it to a transformation By “matching” on the colimit, with a slight adjustment to

      has-lan : is-lan F G F' eta
      has-lan .σ {M = M} α .η c' = ↓colim.universal c'
        (λ j → M .F₁ (j .map) D.∘ α .η (j .x))
        (λ f → D.pullr (α .is-natural _ _ _)
            ∙ pulll M ((f .sq) ∙ C'.idl _))
      has-lan .σ {M = M} α .is-natural x y f = ↓colim.unique₂ _ _
        (λ f → D.pullr (α .is-natural _ _ _)
             ∙ pulll M (C'.pullr (f .sq) ∙ C'.elim-inner refl))
        (λ j → D.pullr (↓colim.factors _ _ _)
             ∙ ↓colim.factors _ _ _)
        (λ j → D.pullr (↓colim.factors _ _ _)
             ∙ D.pulll (sym (M .F-∘ _ _)))

Finally, commutativity and uniqueness follow from the corresponding properties of colimits.

      has-lan .σ-comm {M = M} = ext λ c →
        ↓colim.factors _ _ _ ∙ D.eliml (M .F-id)
      has-lan .σ-uniq {M = M} {α = α} {σ' = σ'} p = ext λ c' → sym $
        ↓colim.unique _ _ _ _ λ j →
        σ' .η c' D.∘ ↓colim.ψ c' j                                ≡⟹ ap (λ ϕ → σ' .η c' D.∘ ↓colim.ψ c' ϕ) (↓Obj-path _ _ refl refl (sym (C'.idr _))) âŸ©â‰Ą
        (σ' .η c' D.∘ ↓colim.ψ c' (↓obj (j .map C'.∘ C'.id)))     ≡⟹ D.pushr (sym $ ↓colim.factors _ _ _) âŸ©â‰Ą
        (σ' .η c' D.∘ ↓colim.universal _ _ _) D.∘ ↓colim.ψ _ _    ≡⟹ D.pushl (σ' .is-natural _ _ _) âŸ©â‰Ą
        M .F₁ (j .map) D.∘ (σ' .η _ D.∘ ↓colim.ψ _ (↓obj C'.id))  ≡˘⟹ (D.refl⟩∘⟚ (p ηₚ j .x)) âŸ©â‰ĄË˜
        M .F₁ (j .map) D.∘ α .η (j .x)                            ∎

All that remains is to bundle up the data!

      lan : Lan F G
      lan .Lan.Ext = F'
      lan .Lan.eta = eta
      lan .Lan.has-lan = has-lan

And, if is then it certainly has the required colimits: we can “un-weaken” our result.

  cocomplete→lan : is-cocomplete ℓ ℓ D → Lan F G
  cocomplete→lan colimits = comma-colimits→lan (λ c' → colimits (↓Dia c'))

Next, we shall show that the left extension we just constructed is pointwise. To do this, we will show a more general fact: if is then it also preserves extensions “built from” colimits.

The mathematical content of the proof is quite straightforward: preserves the colimits used to construct the extension, so we can perform the exact same process in to obtain a left extension. However, the mechanical content of this proof is less pleasant: we end up being off by a bunch of natural isomorphisms.

    : ∀ {o'' ℓ''} {E : Precategory o'' ℓ''}
    → (colimits : is-cocomplete ℓ ℓ D)
    → (H : Functor D E)
    → is-cocontinuous ℓ ℓ H
    → preserves-lan H (Lan.has-lan (cocomplete→lan F G colimits))
  preserves-colimits→preserves-pointwise-lan {E = E} colimits H cocont =
    natural-isos→is-lan idni idni HF'-cohere fixup $
      comma-colimits→lan.has-lan F (H F∘ G) H-↓colim
      module E = Cat.Reasoning E
      open make-natural-iso
      open Func

      ↓colim : (c' : C'.Ob) → Colimit (G F∘ Dom F (Const c'))
      ↓colim c' = colimits (G F∘ Dom F (Const c'))

      module ↓colim c' = Colimit (↓colim c')

      H-↓colim : (c' : C'.Ob) → Colimit ((H F∘ G) F∘ Dom F (Const c'))
      H-↓colim c' =
        natural-iso→colimit ni-assoc $
        preserves-colimit.colimit cocont (↓colim c')

      module H-↓colim c' = Colimit (H-↓colim c')
Unfortunately, proof assistants. By “a bunch”, we really do mean a bunch. This fold contains all the required coherence data, which ends up not being very interesting.
      F' : Functor C' D
      F' = comma-colimits→lan.F' F G λ c' → colimits (G F∘ Dom F (Const c'))

      HF' : Functor C' E
      HF' = comma-colimits→lan.F' F (H F∘ G) H-↓colim

      HF'-cohere : HF' ≅ⁿ H F∘ F'
      HF'-cohere = to-natural-iso mi where
        mi : make-natural-iso HF' (H F∘ F')
        mi .eta c' =
        mi .inv c' =
        mi .eta∘inv _ = E.idl _
        mi .inv∘eta _ = E.idl _
        mi .natural _ _ _ =
          E.idr _
          ∙ H-↓colim.unique _ _ _ _ (λ j → pulll H (↓colim.factors _ _ _))
          ∙ sym (E.idl _)

      module HF'-cohere = Isoⁿ HF'-cohere

        fixup : (HF' ◆ idnt) ∘nt comma-colimits→lan.eta F (H F∘ G) _ ∘nt idnt ≡ nat-assoc-to (H ▾ comma-colimits→lan.eta F G _)
        fixup = ext λ j →
          (H .F₁ (↓colim.universal _ _ _) E.∘ E.∘ (H-↓colim.ψ _ _ E.∘ ≡⟹ ap₂ E._∘_ (E.idr _) (E.idr _) âŸ©â‰Ą
          H .F₁ (↓colim.universal _ _ _) E.∘ H-↓colim.ψ _ _                       ≡⟹ pulll H (↓colim.factors _ _ _) âŸ©â‰Ą
          H .F₁ (↓colim.ψ _ _) E.∘                                           ≡⟹ E.idr _ âŸ©â‰Ą
          H .F₁ (↓colim.ψ _ (↓obj ⌜ C'.id C'.∘ C'.id ⌝))                          ≡⟹ ap! (C'.idl _) âŸ©â‰Ą
          H .F₁ (↓colim.ψ _ (↓obj (C'.id)))                                       ∎

Hom functors take colimits in to colimits in so by the previous lemma, they must preserve the left extension. In other words, the extension we constructed is pointwise.

    : (colim : is-cocomplete ℓ ℓ D)
    → is-pointwise-lan (Lan.has-lan (cocomplete→lan F G colim))
  cocomplete→pointwise-lan colim d =
      colim (Functor.op (Hom-into D d))
      (よ-reverses-colimits d)

All pointwise extensions are computed via (co)limits🔗

As we’ve seen earlier, we can compute the extension of along when has enough colimits, and that this extension is pointwise. It turns out that this is an exact characterization of the pointwise extensions: if is a pointwise extension of along then must have colimits of all diagrams of the form and must be computed via these colimits. This is where the name “pointwise extension” comes from — they really are computed pointwise!

We begin by constructing a cocone for every object

  ↓cocone : ∀ (c' : C'.Ob) → F F∘ Dom p (const! c') => Const (L .F₀ c')
  ↓cocone c' .η j = L .F₁ (j .map) D.∘ eta .η _
  ↓cocone c' .is-natural _ _ f =
    D.pullr (eta .is-natural _ _ _ )
    ∙ pulll L (f .sq ∙ C'.idl _)
    ∙ sym (D.idl _)

To show that the extension is computed pointwise by these extensions, we shall appeal to the fact that colimits are representable.

    : ∀ (c' : C'.Ob)
    → is-colimit (F F∘ Dom p (const! c')) (L .F₀ c') (↓cocone c')
  pointwise-lan→has-comma-colimits c' =
    represents→is-colimit $
    [D,Sets].make-invertible inv invl invr

As is pointwise, we can represent every cocone as a natural transformation though we do need to pass through some abstract representability nonsense to get there.

        : ∀ (d : D.Ob)
        → F F∘ Dom p (const! c') => Const d
        → Functor.op (よ₀ D d) F∘ F => Functor.op (よ₀ C' c') F∘ p
      represent-↓cocone d α .η c f = α .η (↓obj f)
      represent-↓cocone d α .is-natural _ _ f = funext λ g →
        α .is-natural (↓obj (g C'.∘ p .F₁ f)) (↓obj g) (↓hom (sym (C'.idl _)))
        ∙ D.idl _

        : ∀ (d : D.Ob)
        → (α : F F∘ Dom p (const! c') => Const d)
        → Functor.op (Hom-into D d) F∘ L => Functor.op (Hom-into C' c')
      pointwise-↓cocone d α = pointwise.σ d (represent-↓cocone d α)

We can use this representation to construct the required inverse, via the usual Yoneda-like argument.

      inv : Lim[C[F-,=]] => Hom-from D (L .F₀ c')
      inv .η d α =
        pointwise-↓cocone d α .η c' C'.id
      inv .is-natural x y f = funext λ α →
        pointwise.σ-uniq y {σ' = pointwise-↓cocone x α ∘nt (_=>_.op (よ₁ D f) ◂ L)}
          (ext λ c g → D.pushr (sym (pointwise.σ-comm x ηₚ _ $ₚ _))) ηₚ c' $ₚ C'.id
To show that we’ve constructed an isomorphism, we’ll forget the pointwise, and remember that we’re working with a Kan extension.
      invl : Hom-into-inj (↓cocone c') ∘nt inv ≡ idnt
      invl = ext λ d α p↓c' →
        pointwise-↓cocone d α .η _ C'.id D.∘ L .Functor.F₁ (p↓c' .map) D.∘ eta .η _ ≡⟹ D.pulll (pointwise.σ d (represent-↓cocone d α) .is-natural _ _ _ $ₚ _) âŸ©â‰Ą
        pointwise-↓cocone d α .η _ ⌜ C'.id C'.∘ p↓c' .map ⌝ D.∘ eta .η _            ≡⟹ ap! (C'.idl _) âŸ©â‰Ą
        pointwise-↓cocone d α .η _ (p↓c' .map) D.∘ eta .η (x p↓c')                  ≡⟹ pointwise.σ-comm d ηₚ _ $ₚ p↓c' .map âŸ©â‰Ą
        α .η (↓obj (p↓c' .map))                                                     ≡⟹ ap (α .η) (↓Obj-path _ _ refl refl refl) âŸ©â‰Ą
        α .η p↓c'                                                                   ∎

        : ∀ {d : D.Ob} (α : D.Hom (L .F₀ c') d)
        → Functor.op (Hom-into D d) F∘ L => Functor.op (Hom-into C' c')
      vaguely-yoneda α .η c'' f = α D.∘ L .F₁ f
      vaguely-yoneda α .is-natural x y f =
        funext λ g → D.pullr (sym (L .F-∘ _ _))

      invr : inv ∘nt Hom-into-inj (↓cocone c') ≡ idnt
      invr = ext λ d α →
        unext (pointwise.σ-uniq d {σ' = vaguely-yoneda α}
          (ext λ c f → D.assoc _ _ _)) c' C'.id
        ∙ D.elimr (L .F-id)

A corollary is that if is a pointwise left extension along a fully faithful functor, then is a natural isomorphism.

  ff→pointwise-lan-ext : is-fully-faithful p → is-invertibleⁿ eta

The idea is to use the fact that is computed via colimits to construct an inverse to In particular, we use the universal map out of each colimit, relying on the full faithfulness of to construct the requisite cocone.

  ff→pointwise-lan-ext p-ff =
     invertible→invertibleⁿ eta λ c →
       D.make-invertible (inv c)
         (pointwise-colim.unique₂ _ _
           (λ f → D.pullr (eta .is-natural _ _ _)
                ∙ pulll L (sym (p .F-∘ _ _) ∙ path f))
           (λ j → D.pullr (pointwise-colim.factors _ {j = j} _ _)
                ∙ eta .is-natural _ _ _)
           (λ j → D.idl _
                ∙ ap₂ D._∘_ (ap (L .F₁) (sym (equiv→counit p-ff (j .map)))) refl))
         (pointwise.σ-comm _ ηₚ c $ₚ C'.id
          ∙ elimr F (ap (equiv→inverse p-ff) (sym (p .F-id)) ∙ equiv→unit p-ff _))
      module pointwise-colim c' = is-colimit (pointwise-lan→has-comma-colimits c')

        : {c : C.Ob} {x y : ↓Obj p (const! (p .F₀ c))} (f : ↓Hom p (const! (p .F₀ c)) x y)
        → p .F₁ (equiv→inverse p-ff (y .map) C.∘ f .α) ≡ p .F₁ (equiv→inverse p-ff (x .map))
      path {c} {x} {y} f =
        p .F₁ (equiv→inverse p-ff (y .map) C.∘ f .α)          ≡⟹ p .F-∘ _ _ âŸ©â‰Ą
        p .F₁ (equiv→inverse p-ff (y .map)) C'.∘ p .F₁ (f .α) ≡⟹ equiv→counit p-ff _ C'.⟩∘⟚refl âŸ©â‰Ą
        y .map C'.∘ p .F₁ (f .α)                              ≡⟹ f .sq âŸ©â‰Ą
        C'.id C'.∘ x .map                                     ≡⟹ C'.idl _ âŸ©â‰Ą
        x .map                                                ≡˘⟹ equiv→counit p-ff _ âŸ©â‰ĄË˜
        p .F₁ (equiv→inverse p-ff (x .map)) ∎

      inv : ∀ c → D.Hom (L .F₀ (p .F₀ c)) (F .F₀ c)
      inv c =
        pointwise-colim.universal (p .F₀ c)
          (λ j → F .F₁ (equiv→inverse p-ff (j .map)))
          (λ {x} {y} f → collapse F (fully-faithful→faithful {F = p} p-ff (path f)))

module _
  {o o' ℓ ℓ'}
  {C : Precategory ℓ ℓ} {C' : Precategory o ℓ} {D : Precategory o' ℓ'}
  (F : Functor C C') (G : Functor C D)

    module C = Cat.Reasoning C
    module C' = Cat.Reasoning C'
    module D = Cat.Reasoning D
    open Func
    open ↓Obj
    open ↓Hom
    open _=>_
    open Lan

  -- We don't use 'ff→pointwise-lan-ext' here, as it has a more restrictive
  -- universe bound.
    : (cocompl : is-cocomplete ℓ ℓ D)
    → is-fully-faithful F
    → cocomplete→lan F G cocompl .Ext F∘ F ≅ⁿ G
  ff→cocomplete-lan-ext cocompl ff = (to-natural-iso ni) ni⁻Âč where
    open comma-colimits→lan F G (λ c' → cocompl (G F∘ Dom F (Const c')))
    open make-natural-iso renaming (eta to to)
    module ff {x} {y} = Equiv (_ , ff {x} {y})

    ni : make-natural-iso G (F' F∘ F)
    ni .to x = ↓colim.ψ _ (↓obj C'.id)
    ni .inv x = ↓colim.universal _
      (λ j → G .F₁ (ff.from (j .map)))
      (λ f → collapse G $ fully-faithful→faithful {F = F} ff $
           F .F-∘ _ _
        ·· ap₂ C'._∘_ (ff.Δ _) refl
        ·· f .sq
        ·· C'.idl _
        ·· sym (ff.Δ _))
    ni .eta∘inv x = ↓colim.unique₂ _ _
      (λ f → ↓colim.commutes _ f)
      (λ j → D.pullr (↓colim.factors _ _ _)
           ∙ ↓colim.commutes _ (↓hom (ap₂ C'._∘_ refl (ff.Δ _))))
      (λ j → D.idl _)
    ni .inv∘eta x =
        ↓colim.factors _ _ _
      ∙ elim G (ap ff.from (sym (F .F-id)) ∙ ff.η _)
    ni .natural x y f =
        ↓colim.factors _ _ _
      ∙ sym (↓colim.commutes _ (↓hom (ap₂ C'._∘_ refl (sym (C'.idr _)))))