# mathlibdocumentation

category_theory.limits.cofinal

# 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 the following three statements are equivalent:

1. F : C ⥤ D is cofinal.
2. Every functor G : D ⥤ E has a colimit if and only if F ⋙ G does, and these colimits are isomorphic via colimit.pre G F.
3. colimit (F ⋙ coyoneda.obj (op d)) ≅ punit.

Starting at 1. we show (in cocones_equiv) that 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.) This readily implies 2., as comp_has_colimit, has_colimit_of_comp, and colimit_iso.

From 2. we can specialize to G = coyoneda.obj (op d) to obtain 3., as colimit_comp_coyoneda_iso.

From 3., we prove 1. directly in cofinal_of_colimit_comp_coyoneda_iso_punit.

We also show these conditions imply: 4. Every functor H : Dᵒᵖ ⥤ E has a limit if and only if F.op ⋙ H does, and these limits are isomorphic via limit.pre H F.op.

## 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 #

@[class]
structure category_theory.cofinal {C : Type v} {D : Type v} (F : C D) :
Prop
• out : ∀ (d : D),

A functor F : C ⥤ D is cofinal if for every d : D, the comma category of morphisms d ⟶ F.obj c is connected.

Instances
@[instance]
def category_theory.cofinal.category_theory.structured_arrow.nonempty {C : Type v} {D : Type v} (F : C D) (d : D) :
def category_theory.cofinal.lift {C : Type v} {D : Type v} (F : C D) (d : D) :
C

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
def category_theory.cofinal.hom_to_lift {C : Type v} {D : Type v} (F : C D) (d : D) :
d F.obj

When F : C ⥤ D is cofinal, we denote by hom_to_lift an arbitrary choice of morphism d ⟶ F.obj (lift F d).

Equations
theorem category_theory.cofinal.induction {C : Type v} {D : Type v} (F : C D) {d : D} (Z : Π (X : C), (d F.obj X) → Prop) (h₁ : ∀ (X₁ X₂ : C) (k₁ : d F.obj X₁) (k₂ : d F.obj X₂) (f : X₁ X₂), k₁ F.map f = k₂Z X₁ k₁Z X₂ k₂) (h₂ : ∀ (X₁ X₂ : C) (k₁ : d F.obj X₁) (k₂ : d F.obj X₂) (f : X₁ X₂), k₁ F.map f = k₂Z X₂ k₂Z X₁ k₁) {X₀ : C} {k₀ : d F.obj X₀} (z : Z X₀ k₀) :

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.

@[simp]
theorem category_theory.cofinal.extend_cocone_obj_ι_app {C : Type v} {D : Type v} {F : C D} {E : Type u} {G : D E} (c : category_theory.limits.cocone (F G)) (X : D) :
= c.ι.app
@[simp]
theorem category_theory.cofinal.extend_cocone_map_hom {C : Type v} {D : Type v} {F : C D} {E : Type u} {G : D E} (X Y : category_theory.limits.cocone (F G)) (f : X Y) :
@[simp]
theorem category_theory.cofinal.extend_cocone_obj_X {C : Type v} {D : Type v} {F : C D} {E : Type u} {G : D E} (c : category_theory.limits.cocone (F G)) :
def category_theory.cofinal.extend_cocone {C : Type v} {D : Type v} {F : C D} {E : Type u} {G : D E} :

Given a cocone over F ⋙ G, we can construct a cocone G with the same cocone point.

Equations
@[simp]
theorem category_theory.cofinal.colimit_cocone_comp_aux {C : Type v} {D : Type v} {F : C D} {E : Type u} {G : D E} (s : category_theory.limits.cocone (F G)) (j : C) :
G.map (F.obj j)) s.ι.app (F.obj j)) = s.ι.app j
def category_theory.cofinal.extend_cone_cone_to_cocone {C : Type v} {D : Type v} {E : Type u} {F : C D} {H : Dᵒᵖ E} (c : category_theory.limits.cone (F.op H)) :

An auxiliary construction for extend_cone, moving op around.

Equations
@[simp]
theorem category_theory.cofinal.extend_cone_cone_to_cocone_X {C : Type v} {D : Type v} {E : Type u} {F : C D} {H : Dᵒᵖ E} (c : category_theory.limits.cone (F.op H)) :
@[simp]
theorem category_theory.cofinal.extend_cone_cone_to_cocone_ι_app {C : Type v} {D : Type v} {E : Type u} {F : C D} {H : Dᵒᵖ E} (c : category_theory.limits.cone (F.op H)) (j : C) :
= (c.π.app (opposite.op j)).op
def category_theory.cofinal.extend_cone_cocone_to_cone {D : Type v} {E : Type u} {H : Dᵒᵖ E}  :

An auxiliary construction for extend_cone, moving op around.

Equations
@[simp]
theorem category_theory.cofinal.extend_cone_cocone_to_cone_π_app {D : Type v} {E : Type u} {H : Dᵒᵖ E} (j : Dᵒᵖ) :
@[simp]
theorem category_theory.cofinal.extend_cone_cocone_to_cone_X {D : Type v} {E : Type u} {H : Dᵒᵖ E}  :
def category_theory.cofinal.extend_cone {C : Type v} {D : Type v} {F : C D} {E : Type u} {H : Dᵒᵖ E} :

Given a cone over F.op ⋙ H, we can construct a cone H with the same cone point.

Equations
@[simp]
theorem category_theory.cofinal.extend_cone_obj {C : Type v} {D : Type v} {F : C D} {E : Type u} {H : Dᵒᵖ E} (c : category_theory.limits.cone (F.op H)) :
@[simp]
theorem category_theory.cofinal.extend_cone_map_hom {C : Type v} {D : Type v} {F : C D} {E : Type u} {H : Dᵒᵖ E} (X Y : category_theory.limits.cone (F.op H)) (f : X Y) :
@[simp]
theorem category_theory.cofinal.limit_cone_comp_aux {C : Type v} {D : Type v} {F : C D} {E : Type u} {H : Dᵒᵖ E} (s : category_theory.limits.cone (F.op H)) (j : Cᵒᵖ) :
@[simp]
theorem category_theory.cofinal.cocones_equiv_unit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E) :
@[simp]
theorem category_theory.cofinal.cocones_equiv_functor {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E) :
@[simp]
theorem category_theory.cofinal.cocones_equiv_inverse {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E) :
def category_theory.cofinal.cocones_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E) :

If F is cofinal, the category of cocones on F ⋙ G is equivalent to the category of cocones on G, for any G : D ⥤ E.

Equations
@[simp]
theorem category_theory.cofinal.cocones_equiv_counit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E) :
@[simp]
theorem category_theory.cofinal.cones_equiv_functor {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E) :
@[simp]
theorem category_theory.cofinal.cones_equiv_unit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E) :
def category_theory.cofinal.cones_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E) :

If F is cofinal, the category of cones on F.op ⋙ H is equivalent to the category of cones on H, for any H : Dᵒᵖ ⥤ E.

Equations
@[simp]
theorem category_theory.cofinal.cones_equiv_counit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E) :
@[simp]
theorem category_theory.cofinal.cones_equiv_inverse {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E) :
def category_theory.cofinal.is_colimit_whisker_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :

When F : C ⥤ D is cofinal, and t : cocone G for some G : D ⥤ E, t.whisker F is a colimit cocone exactly when t is.

Equations
def category_theory.cofinal.is_limit_whisker_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :

When F : C ⥤ D is cofinal, and t : cone H for some H : Dᵒᵖ ⥤ E, t.whisker F.op is a limit cone exactly when t is.

Equations
def category_theory.cofinal.is_colimit_extend_cocone_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E} (t : category_theory.limits.cocone (F G)) :

When F is cofinal, and t : cocone (F ⋙ G), extend_cocone.obj t is a colimit coconne exactly when t is.

Equations
def category_theory.cofinal.is_limit_extend_cone_equiv {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} (t : category_theory.limits.cone (F.op H)) :

When F is cofinal, and t : cone (F.op ⋙ H), extend_cone.obj t is a limit conne exactly when t is.

Equations
@[simp]
theorem category_theory.cofinal.colimit_cocone_comp_is_colimit {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :
@[simp]
theorem category_theory.cofinal.colimit_cocone_comp_cocone {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :
def category_theory.cofinal.colimit_cocone_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :

Given a colimit cocone over G : D ⥤ E we can construct a colimit cocone over F ⋙ G.

Equations
def category_theory.cofinal.limit_cone_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :

Given a limit cone over H : Dᵒᵖ ⥤ E we can construct a limit cone over F.op ⋙ H.

Equations
@[simp]
theorem category_theory.cofinal.limit_cone_comp_cone {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :
@[simp]
theorem category_theory.cofinal.limit_cone_comp_is_limit {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :
@[instance]
def category_theory.cofinal.comp_has_colimit {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :
@[instance]
def category_theory.cofinal.comp_has_limit {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :
theorem category_theory.cofinal.colimit_pre_is_iso_aux {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :
@[instance]
def category_theory.cofinal.colimit_pre_is_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :
theorem category_theory.cofinal.limit_pre_is_iso_aux {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :
= 𝟙 t.X
@[instance]
def category_theory.cofinal.limit_pre_is_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E}  :
def category_theory.cofinal.colimit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (G : D E)  :

When F : C ⥤ D is cofinal, and G : D ⥤ E has a colimit, then F ⋙ G has a colimit also and colimit (F ⋙ G) ≅ colimit G

https://stacks.math.columbia.edu/tag/04E7

Equations
def category_theory.cofinal.limit_iso {C : Type v} {D : Type v} (F : C D) {E : Type u} (H : Dᵒᵖ E)  :

When F : C ⥤ D is cofinal, and H : Dᵒᵖ ⥤ E has a limit, then F.op ⋙ H has a limit also and limit (F.op ⋙ H) ≅ limit H

https://stacks.math.columbia.edu/tag/04E7

Equations
def category_theory.cofinal.colimit_cocone_of_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E} (t : category_theory.limits.colimit_cocone (F G)) :

Given a colimit cocone over F ⋙ G we can construct a colimit cocone over G.

Equations
@[simp]
theorem category_theory.cofinal.colimit_cocone_of_comp_cocone {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E} (t : category_theory.limits.colimit_cocone (F G)) :
@[simp]
theorem category_theory.cofinal.colimit_cocone_of_comp_is_colimit {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E} (t : category_theory.limits.colimit_cocone (F G)) :
@[simp]
theorem category_theory.cofinal.limit_cone_of_comp_cone {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} (t : category_theory.limits.limit_cone (F.op H)) :
@[simp]
theorem category_theory.cofinal.limit_cone_of_comp_is_limit {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} (t : category_theory.limits.limit_cone (F.op H)) :
def category_theory.cofinal.limit_cone_of_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} (t : category_theory.limits.limit_cone (F.op H)) :

Given a limit cone over F.op ⋙ H we can construct a limit cone over H.

Equations
theorem category_theory.cofinal.has_colimit_of_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :

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.)

theorem category_theory.cofinal.has_limit_of_comp {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} [category_theory.limits.has_limit (F.op H)] :

When F is cofinal, and F.op ⋙ H has a limit, then H has a limit 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_limit.)

def category_theory.cofinal.colimit_iso' {C : Type v} {D : Type v} (F : C D) {E : Type u} {G : D E}  :

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

Equations
def category_theory.cofinal.limit_iso' {C : Type v} {D : Type v} (F : C D) {E : Type u} {H : Dᵒᵖ E} [category_theory.limits.has_limit (F.op H)] :

When F is cofinal, and F.op ⋙ H has a limit, then H has a limit also and limit (F.op ⋙ H) ≅ limit H

https://stacks.math.columbia.edu/tag/04E7

Equations
def category_theory.cofinal.colimit_comp_coyoneda_iso {C : Type v} {D : Type v} (F : C D) (d : D)  :

If the universal morphism colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d)) is an isomorphism (as it always is when F is cofinal), then colimit (F ⋙ coyoneda.obj (op d)) ≅ punit (simply because colimit (coyoneda.obj (op d)) ≅ punit).

Equations
theorem category_theory.cofinal.zigzag_of_eqv_gen_quot_rel {C : Type v} {D : Type v} {F : C D} {d : D} {f₁ f₂ : Σ (X : C), d F.obj X} (t : f₂) :
theorem category_theory.cofinal.cofinal_of_colimit_comp_coyoneda_iso_punit {C : Type v} {D : Type v} (F : C D) (I : Π (d : D), ) :

If colimit (F ⋙ coyoneda.obj (op d)) ≅ punit for all d : D, then F is cofinal.