open import Cat.Diagram.Colimit.Base
open import Cat.Prelude

import Cat.Reasoning as Cr

module Cat.Functor.Final where

Final functorsπŸ”—

A final functor expresses an equivalence of diagram schemata for the purposes of computing colimits: If F:Cβ†’DF : \mathcal{C} \to \mathcal{D} is final, then colimits for D:Dβ†’ED : \mathcal{D} \to \mathcal{E} are equivalents to colimits for D∘F:Cβ†’ED\circ F : \mathcal{C} \to \mathcal{E}. A terminological warning: In older literature (e.g. (Borceux 1994) and (Adamek and Rosicky 1994)), these functors are called cofinal, but we stick with terminology from the nLab here.

Finality has an elementary characterisation: We define a functor FF to be final if, for every dd, the comma category d↙Fd \swarrow F is pointed and connected. That is, unpacking, the following data: For every object d:Dd : \mathcal{D}, an object d0d_0 and a map d!:dβ†’F(d0)d_! : d \to F(d_0), and for every span

a map f:a→bf : a \to b, such that the triangle


  record is-final : Type (o βŠ” β„“ βŠ” oβ€² βŠ” β„“β€²) where
      point : π’Ÿ.Ob β†’ π’ž.Ob
      map   : βˆ€ d β†’ π’Ÿ.Hom d (F.β‚€ (point d))
        : βˆ€ {a b x} (f : π’Ÿ.Hom x (F.β‚€ a)) (g : π’Ÿ.Hom x (F.β‚€ b))
        β†’ π’ž.Hom a b
        : βˆ€ {a b x} (f : π’Ÿ.Hom x (F.β‚€ a)) (g : π’Ÿ.Hom x (F.β‚€ b))
        β†’ g ≑ F.₁ (extend f g) π’Ÿ.∘ f

The utility of this definition comes, as mentioned, from the ability to move (colimiting) cocones back and forth between a diagram DD and its restriction D∣FD_{|F} to the domain category C\mathcal{C}. If we have a cocone {DF(x)β†’K}\{DF(x) \to K\}, then precomposition with the map D(x!):D(x)β†’DF(x0)D(x_!) : D(x) \to DF(x_0) (where x!x_! comes from the finality of FF) defines a cocone {D(x)β†’K}\{D(x) \to K\}.

    extend-cocone : Cocone (D F∘ F) β†’ Cocone D
    extend-cocone cone = coneβ€² where
      open is-iso
      module cone = Cocone cone
      coneβ€² : Cocone D
      coneβ€² .coapex = cone.coapex
      coneβ€² .ψ x = cone.ψ _ β„°.∘ D.₁ ( x)
      coneβ€² .commutes f =
        (cone.ψ _ β„°.∘ D.₁ ( _)) β„°.∘ D.₁ f β‰‘βŸ¨ β„°.pullr (sym (D.F-∘ _ _)) βŸ©β‰‘
        cone.ψ _ β„°.∘ D.₁ ( _ π’Ÿ.∘ f)       β‰‘βŸ¨ β„°.pushl (sym (cone.commutes (fin.extend ( _ π’Ÿ.∘ f) ( _)))) βŸ©β‰‘
        cone.ψ _ β„°.∘ _                           β‰‘βŸ¨ β„°.refl⟩∘⟨ sym (D.F-∘ _ _) βˆ™ ap D.₁ (sym (fin.extend-commutes _ _)) βŸ©β‰‘
        cone.ψ _ β„°.∘ D.₁ ( _)             ∎

In the other direction, suppose that we have a cocone {D(x)β†’K}\{D(x) \to K\} β€” inserting FF in the appropriate places makes a cocone {DF(x)β†’K}\{DF(x) \to K\}.

    restrict-cocone : Cocone D β†’ Cocone (D F∘ F)
    restrict-cocone K = Kβ€² where
      module K = Cocone K
      Kβ€² : Cocone (D F∘ F)
      Kβ€² .coapex = K.coapex
      Kβ€² .ψ x = K.ψ (F.Fβ‚€ x)
      Kβ€² .commutes f = K.commutes (F.F₁ f)

A computation using connectedness of the comma categories shows that these formulae are mutually inverse:

    open is-iso
    extend-cocone-is-iso : is-iso extend-cocone
    extend-cocone-is-iso .inv = restrict-cocone
    extend-cocone-is-iso .rinv x = Cocone-path _ refl $ Ξ» o β†’
      x .commutes _
    extend-cocone-is-iso .linv x = Cocone-path _ refl $ Ξ» o β†’
      x .ψ _ β„°.∘ D.₁ ( (F.Fβ‚€ o))                           β‰‘Λ˜βŸ¨ x .commutes (fin.extend ( (F.Fβ‚€ o)) π’Ÿ.id) β„°.⟩∘⟨refl βŸ©β‰‘Λ˜
      (x .ψ o β„°.∘ D.₁ (F.₁ (fin.extend _ _))) β„°.∘ D.₁ ( _) β‰‘βŸ¨ β„°.pullr (sym (D.F-∘ _ _) Β·Β· ap D.₁ (fin.extend-commutes _ _) Β·Β· ap D.₁ (π’Ÿ.idr _)) βŸ©β‰‘
      x .ψ o β„°.∘ D.₁ (F.₁ (fin.extend _ _))                       β‰‘βŸ¨ x .commutes _ βŸ©β‰‘
      x .ψ o                                                      ∎

    restriction-eqv : Cocone (D F∘ F) ≃ Cocone D
    restriction-eqv = _ , is-iso→is-equiv extend-cocone-is-iso

The most important conclusion that we get is the following: If you can show that the restricted cocone is a colimit, then the original cocone was a colimit, too! We’ll do this in two steps: First, show that the extension of a colimiting cocone is a colimit. Then, using the fact that restrict-cocone is an equivalence, we’ll be able to fix up the polarity mismatch.

      : (K : Cocone (D F∘ F))
      β†’ is-colimit (D F∘ F) K β†’ is-colimit D (extend-cocone K)
The proof of the auxiliary lemma is a direct computation, so I’ll leave it in this <details> tag for the curious reader only.
    extend-is-colimit K colim x = contr xΒ‘ xΒ‘-unique where
      module K = Cocone K
      module x = Cocone x
      xβ€² : Cocone (D F∘ F)
      xβ€² = restrict-cocone x

      xβ€²Β‘ = colim xβ€²
      xΒ‘ : Cocone-hom D (extend-cocone K) x
      xΒ‘ .hom = xβ€²Β‘ .centre .hom
      xΒ‘ .commutes o =
        xβ€²Β‘ .centre .hom β„°.∘ K.ψ _ β„°.∘ D.₁ _    β‰‘βŸ¨ β„°.pulll (xβ€²Β‘ .centre .commutes _) βŸ©β‰‘
        xβ€² .ψ _ β„°.∘ D.₁ ( o)             β‰‘βŸ¨ x .commutes _ βŸ©β‰‘
        x.ψ o                                   ∎

      xΒ‘-unique : βˆ€ hβ€² β†’ xΒ‘ ≑ hβ€²
      xΒ‘-unique hβ€² = Cocone-hom-path D $ ap hom $ xβ€²Β‘ .paths go where
        go : Cocone-hom (D F∘ F) K xβ€²
        go .hom = hβ€² .hom
        go .commutes o =
          hβ€² .hom β„°.∘ K.ψ o                     β‰‘Λ˜βŸ¨ β„°.refl⟩∘⟨ K.commutes (fin.extend π’Ÿ.id ( _)) βŸ©β‰‘Λ˜
          hβ€² .hom β„°.∘ K.ψ _ β„°.∘ D.₁ (F.₁ _)     β‰‘βŸ¨ β„°.refl⟩∘⟨ β„°.refl⟩∘⟨ ap D.₁ (π’Ÿ.intror refl βˆ™ sym (fin.extend-commutes _ _)) βŸ©β‰‘
          hβ€² .hom β„°.∘ K.ψ _ β„°.∘ D.₁ ( _) β‰‘βŸ¨ hβ€² .commutes _ βŸ©β‰‘
          x.ψ (F.β‚€ o)                           ∎
      : (K : Cocone D)
      β†’ is-colimit (D F∘ F) (restrict-cocone K) β†’ is-colimit D K
    is-colimit-restrict K colim = subst (is-colimit D)
      (Equiv.Ξ΅ restriction-eqv _)
      (extend-is-colimit (restrict-cocone K) colim)

Another short computation shows us that final functors are closed under composition.

  F∘-is-final : is-final (G F∘ F)
  F∘-is-final .point e    = ff.point (gf.point e)
  F∘-is-final .map d      = G.₁ ( _) β„°.∘ _
  F∘-is-final .extend f g = ff.extend π’Ÿ.id (gf.extend f g)
  F∘-is-final .extend-commutes f g =
    g                                                β‰‘βŸ¨ gf.extend-commutes _ _ βŸ©β‰‘
    G.₁ ⌜ g-fin .extend f g ⌝ β„°.∘ f                  β‰‘βŸ¨ ap! (ff.extend-commutes _ _ βˆ™ π’Ÿ.elimr refl) βŸ©β‰‘
    G.₁ (F.₁ (ff.extend π’Ÿ.id (gf.extend f g))) β„°.∘ f ∎