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 : βˆ€ {coapex} β†’ D F∘ F => Const coapex β†’ D => Const coapex
    extend-cocone cone .Ξ· x = cone .Ξ· _ β„°.∘ D.₁ ( x)
    extend-cocone cone .is-natural x y f =
      β„°.pullr (sym (D.F-∘ _ _))
      Β·Β· β„°.pushl (sym (cone .is-natural _ _ _ βˆ™ β„°.idl _))
      Β·Β· (β„°.refl⟩∘⟨ D.collapse (sym (fin.extend-commutes _ _)))
      βˆ™ sym (β„°.idl _)

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 : βˆ€ {coapex} β†’ D => Const coapex β†’ D F∘ F => Const coapex
    restrict-cocone K .Ξ· x = K .Ξ· (F.Fβ‚€ x)
    restrict-cocone K .is-natural x y f = K .is-natural (F.Fβ‚€ x) (F.Fβ‚€ y) (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 : βˆ€ {coapex} β†’ is-iso (extend-cocone {coapex})
    extend-cocone-is-iso .inv = restrict-cocone
    extend-cocone-is-iso .rinv x =
      Nat-path Ξ» o β†’
        x .is-natural _ _ _ βˆ™ β„°.idl _
    extend-cocone-is-iso .linv x =
      Nat-path Ξ» o β†’
        (sym (β„°.idl _) βˆ™ sym (x .is-natural _ _ (fin.extend ( (F.Fβ‚€ o)) π’Ÿ.id)) β„°.⟩∘⟨refl)
        Β·Β· β„°.pullr (D.collapse (fin.extend-commutes _ _ βˆ™ π’Ÿ.idr _))
        Β·Β· x .is-natural _ _ _
        βˆ™ β„°.idl _

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.

      : βˆ€ {coapex} (K : D F∘ F => Const coapex)
      β†’ is-colimit (D F∘ F) coapex K
      β†’ is-colimit D coapex (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 {coapex} K colim =
      to-is-colimitp mc refl
      module extend-is-colimit where
        module colim = is-colimit colim
        open make-is-colimit

        mc : make-is-colimit D coapex
        mc .ψ x = extend-cocone K .η x
        mc .commutes f = extend-cocone K .is-natural _ _ _ βˆ™ β„°.idl _
        mc .universal eps p =
          colim.universal (Ξ» j β†’ eps (F.Fβ‚€ j)) Ξ» f β†’ p (F.F₁ f)
        mc .factors eps p =
          β„°.pulll (colim.factors _ _)
          βˆ™ p ( _)
        mc .unique eps p other q =
          colim.unique _ _ _ Ξ» j β†’
            other β„°.∘ K .Ξ· j                                  β‰‘βŸ¨ β„°.refl⟩∘⟨ (sym (β„°.idl _) βˆ™ sym (K .is-natural _ _ _)) ⟩
            other β„°.∘ K .Ξ· _ β„°.∘ D.F₁ (F.F₁ (fin.extend _ _)) β‰‘βŸ¨ β„°.refl⟩∘⟨ β„°.refl⟩∘⟨ ap D.₁ (sym (π’Ÿ.idr _) βˆ™ sym (fin.extend-commutes _ _)) ⟩
            other β„°.∘ K .Ξ· _ β„°.∘ D.F₁ ( _)             β‰‘βŸ¨ q (F.Fβ‚€ j) ⟩
            eps (F.Fβ‚€ j)                                      ∎
      : βˆ€ {coapex}
      β†’ (K : D => Const coapex)
      β†’ is-colimit (D F∘ F) coapex (restrict-cocone K)
      β†’ is-colimit D coapex K
    is-colimit-restrict {coapex} K colim =
        ( (restrict-cocone K) colim)
        (extend-cocone-is-iso .rinv K Ξ·β‚š _)
        where open is-iso

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 ∎