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 is final, then colimits for are equivalents to colimits for . 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 to be final if, for every , the comma category is pointed and connected. That is, unpacking, the following data: For every object , an object and a map , and for every span
a map , such that the triangle
commutes.
record is-final : Type (o β β β oβ² β ββ²) where field point : π.Ob β π.Ob map : β d β π.Hom d (F.β (point d)) extend : β {a b x} (f : π.Hom x (F.β a)) (g : π.Hom x (F.β b)) β π.Hom a b extend-commutes : β {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 and its restriction to the domain category . If we have a cocone , then precomposition with the map (where comes from the finality of ) defines a cocone .
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.β (fin.map x) coneβ² .commutes f = (cone.Ο _ β°.β D.β (fin.map _)) β°.β D.β f β‘β¨ β°.pullr (sym (D.F-β _ _)) β©β‘ cone.Ο _ β°.β D.β (fin.map _ π.β f) β‘β¨ β°.pushl (sym (cone.commutes (fin.extend (fin.map _ π.β f) (fin.map _)))) β©β‘ cone.Ο _ β°.β _ β‘β¨ β°.reflβ©ββ¨ sym (D.F-β _ _) β ap D.β (sym (fin.extend-commutes _ _)) β©β‘ cone.Ο _ β°.β D.β (fin.map _) β
In the other direction, suppose that we have a cocone β inserting in the appropriate places makes a cocone .
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.β (fin.map (F.Fβ o)) β‘Λβ¨ x .commutes (fin.extend (fin.map (F.Fβ o)) π.id) β°.β©ββ¨refl β©β‘Λ (x .Ο o β°.β D.β (F.β (fin.extend _ _))) β°.β D.β (fin.map _) β‘β¨ β°.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.
extend-is-colimit : (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.β (fin.map 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 (fin.map _)) β©β‘Λ hβ² .hom β°.β K.Ο _ β°.β D.β (F.β _) β‘β¨ β°.reflβ©ββ¨ β°.reflβ©ββ¨ ap D.β (π.intror refl β sym (fin.extend-commutes _ _)) β©β‘ hβ² .hom β°.β K.Ο _ β°.β D.β (fin.map _) β‘β¨ hβ² .commutes _ β©β‘ x.Ο (F.β o) β
is-colimit-restrict : (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.β (ff.map _) β°.β gf.map _ 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 β
References
- Adamek, J., and J. Rosicky. 1994. Locally Presentable and Accessible Categories. Lecture Note Series / London Mathematical Society. Cambridge University Press. https://books.google.com.br/books?id=iXh6rOd7of0C.
- Borceux, Francis. 1994. Handbook of Categorical Algebra. Vol. 1. Encyclopedia of Mathematics and Its Applications. Cambridge University Press. https://doi.org/10.1017/CBO9780511525858.