Cofinal functors
A functor F : C ⥤ D is cofinal if for every d : D,
the comma category of morphisms d ⟶ F.obj c is connected.
We prove that when F : C ⥤ D is cofinal,
the categories of cocones over G : D ⥤ E and over F ⋙ G are equivalent.
(In fact, via an equivalence which does not change the cocone point.)
As a consequence, the functor G : D ⥤ E has a colimit if and only if F ⋙ F does
(and in either case, the colimits are isomorphic).
There is a converse which we don't prove here.
I think the correct statement is that if colimit.pre G F : colimit (F ⋙ G) ⟶ colimit G
is an isomorphism for all functors G : D ⥤ Type v, then F is cofinal.
(Unfortunately I don't know a reference that gives the proof.)
Naming
There is some discrepancy in the literature about naming; some say 'final' instead of 'cofinal'. The explanation for this is that the 'co' prefix here is not the usual category-theoretic one indicating duality, but rather indicating the sense of "along with".
While the trend seems to be towards using 'final', for now we go with the bulk of the literature and use 'cofinal'.
References
- https://stacks.math.columbia.edu/tag/09WN
- https://ncatlab.org/nlab/show/final+functor
- Borceux, Handbook of Categorical Algebra I, Section 2.11. (Note he reverses the roles of definition and main result relative to here!)
A functor F : C ⥤ D is cofinal if for every d : D, the comma category of morphisms d ⟶ F.obj c
is connected.
See https://stacks.math.columbia.edu/tag/04E6
Equations
When F : C ⥤ D is cofinal, we denote by lift F d an arbitrary choice of object in C such that
there exists a morphism d ⟶ F.obj (lift F d).
Equations
When F : C ⥤ D is cofinal, we denote by hom_to_lift an arbitrary choice of morphism
d ⟶ F.obj (lift F d).
Equations
We provide an induction principle for reasoning about lift and hom_to_lift.
We want to perform some construction (usually just a proof) about
the particular choices lift F d and hom_to_lift F d,
it suffices to perform that construction for some other pair of choices
(denoted X₀ : C and k₀ : d ⟶ F.obj X₀ below),
and to show that how to transport such a construction
both directions along a morphism between such choices.
Given a cocone over F ⋙ G, we can construct a cocone G with the same cocone point.
Equations
- category_theory.cofinal.extend_cocone = {obj := λ (c : category_theory.limits.cocone (F ⋙ G)), {X := c.X, ι := {app := λ (X : D), G.map (category_theory.cofinal.hom_to_lift F X) ≫ c.ι.app (category_theory.cofinal.lift F X), naturality' := _}}, map := λ (X Y : category_theory.limits.cocone (F ⋙ G)) (f : X ⟶ Y), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
If F is cofinal,
the category of cocones on F ⋙ G is equivalent to the category of cocones on G.
Equations
- category_theory.cofinal.cocones_equiv F = {functor := category_theory.cofinal.extend_cocone G, inverse := category_theory.limits.cocones.whiskering F, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cocone (F ⋙ G)), category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cocone (F ⋙ G))).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cocone G), category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.whiskering F ⋙ category_theory.cofinal.extend_cocone).obj c).X) _) _, functor_unit_iso_comp' := _}
When F is cofinal, and t : cocone G,
t.whisker F is a colimit coconne exactly when t is.
When F is cofinal, and t : cocone (F ⋙ G),
extend_cocone.obj t is a colimit coconne exactly when t is.
Given a colimit cocone over G we can construct a colimit cocone over F ⋙ G.
Equations
Equations
When F is cofinal, and G has a colimit, then F ⋙ G has a colimit also and
colimit (F ⋙ G) ≅ colimit G
https://stacks.math.columbia.edu/tag/04E7
Given a colimit cocone over F ⋙ G we can construct a colimit cocone over G.
When F is cofinal, and F ⋙ G has a colimit, then G has a colimit also.
We can't make this an instance, because F is not determined by the goal.
(Even if this weren't a problem, it would cause a loop with comp_has_colimit.)
When F is cofinal, and F ⋙ G has a colimit, then G has a colimit also and
colimit (F ⋙ G) ≅ colimit G
https://stacks.math.columbia.edu/tag/04E7