# mathlibdocumentation

category_theory.limits.final

# Final and initial functors #

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

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

We show that right adjoints are examples of final functors, while left adjoints are examples of initial functors.

For final functors, we prove that the following three statements are equivalent:

1. F : C ⥤ D is final.
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.

Dually, we prove that if a functor F : C ⥤ D is initial, then any functor G : D ⥤ E has a limit if and only if F ⋙ G does, and these limits are isomorphic via limit.pre G F.

## Naming #

There is some discrepancy in the literature about naming; some say 'cofinal' instead of 'final'. 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".

## Future work #

Dualise condition 3 above and the implications 2 ⇒ 3 and 3 ⇒ 1 to initial functors.

## References #

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

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

Instances of this typeclass
@[class]
structure category_theory.functor.initial {C : Type v} {D : Type v} (F : C D) :
Prop
• out : ∀ (d : D),

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

Instances of this typeclass
@[protected, instance]
def category_theory.functor.final_op_of_initial {C : Type v} {D : Type v} (F : C D) [F.initial] :
@[protected, instance]
def category_theory.functor.initial_op_of_final {C : Type v} {D : Type v} (F : C D) [F.final] :
theorem category_theory.functor.final_of_initial_op {C : Type v} {D : Type v} (F : C D) [F.op.initial] :
theorem category_theory.functor.initial_of_final_op {C : Type v} {D : Type v} (F : C D) [F.op.final] :
theorem category_theory.functor.final_of_adjunction {C : Type v} {D : Type v} {L : C D} {R : D C} (adj : L R) :

If a functor R : D ⥤ C is a right adjoint, it is final.

theorem category_theory.functor.initial_of_adjunction {C : Type v} {D : Type v} {L : C D} {R : D C} (adj : L R) :

If a functor L : C ⥤ D is a left adjoint, it is initial.

@[protected, instance]
def category_theory.functor.final_of_is_right_adjoint {C : Type v} {D : Type v} (F : C D)  :
@[protected, instance]
def category_theory.functor.initial_of_is_left_adjoint {C : Type v} {D : Type v} (F : C D)  :
@[protected, instance]
def category_theory.functor.final.category_theory.structured_arrow.nonempty {C : Type v} {D : Type v} (F : C D) [F.final] (d : D) :
noncomputable def category_theory.functor.final.lift {C : Type v} {D : Type v} (F : C D) [F.final] (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
noncomputable def category_theory.functor.final.hom_to_lift {C : Type v} {D : Type v} (F : C D) [F.final] (d : D) :
d

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

Equations
noncomputable def category_theory.functor.final.induction {C : Type v} {D : Type v} (F : C D) [F.final] {d : D} (Z : Π (X : C), (d F.obj X)Sort u_1) (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 how to transport such a construction both directions along a morphism between such choices.

Equations
@[simp]
theorem category_theory.functor.final.extend_cocone_obj_X {C : Type v} {D : Type v} {F : C D} [F.final] {E : Type u} {G : D E} (c : category_theory.limits.cocone (F G)) :
@[simp]
theorem category_theory.functor.final.extend_cocone_obj_ι_app {C : Type v} {D : Type v} {F : C D} [F.final] {E : Type u} {G : D E} (c : category_theory.limits.cocone (F G)) (X : D) :
noncomputable def category_theory.functor.final.extend_cocone {C : Type v} {D : Type v} {F : C D} [F.final] {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.functor.final.extend_cocone_map_hom {C : Type v} {D : Type v} {F : C D} [F.final] {E : Type u} {G : D E} (X Y : category_theory.limits.cocone (F G)) (f : X Y) :
@[simp]
theorem category_theory.functor.final.colimit_cocone_comp_aux {C : Type v} {D : Type v} {F : C D} [F.final] {E : Type u} {G : D E} (s : category_theory.limits.cocone (F G)) (j : C) :
G.map s.ι.app (F.obj j)) = s.ι.app j
@[simp]
theorem category_theory.functor.final.cocones_equiv_inverse {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} (G : D E) :
noncomputable def category_theory.functor.final.cocones_equiv {C : Type v} {D : Type v} (F : C D) [F.final] {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.functor.final.cocones_equiv_functor {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} (G : D E) :
@[simp]
theorem category_theory.functor.final.cocones_equiv_counit_iso {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} (G : D E) :
@[simp]
theorem category_theory.functor.final.cocones_equiv_unit_iso {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} (G : D E) :
noncomputable def category_theory.functor.final.is_colimit_whisker_equiv {C : Type v} {D : Type v} (F : C D) [F.final] {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
noncomputable def category_theory.functor.final.is_colimit_extend_cocone_equiv {C : Type v} {D : Type v} (F : C D) [F.final] {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
@[simp]
theorem category_theory.functor.final.colimit_cocone_comp_is_colimit {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :
noncomputable def category_theory.functor.final.colimit_cocone_comp {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :

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

Equations
@[simp]
theorem category_theory.functor.final.colimit_cocone_comp_cocone {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :
@[protected, instance]
def category_theory.functor.final.comp_has_colimit {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :
theorem category_theory.functor.final.colimit_pre_is_iso_aux {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :
@[protected, instance]
def category_theory.functor.final.colimit_pre_is_iso {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E}  :
noncomputable def category_theory.functor.final.colimit_iso {C : Type v} {D : Type v} (F : C D) [F.final] {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
@[simp]
theorem category_theory.functor.final.colimit_cocone_of_comp_is_colimit {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E} (t : category_theory.limits.colimit_cocone (F G)) :
@[simp]
theorem category_theory.functor.final.colimit_cocone_of_comp_cocone {C : Type v} {D : Type v} (F : C D) [F.final] {E : Type u} {G : D E} (t : category_theory.limits.colimit_cocone (F G)) :
noncomputable def category_theory.functor.final.colimit_cocone_of_comp {C : Type v} {D : Type v} (F : C D) [F.final] {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
theorem category_theory.functor.final.has_colimit_of_comp {C : Type v} {D : Type v} (F : C D) [F.final] {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.)

noncomputable def category_theory.functor.final.colimit_iso' {C : Type v} {D : Type v} (F : C D) [F.final] {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
noncomputable def category_theory.functor.final.colimit_comp_coyoneda_iso {C : Type v} {D : Type v} (F : C D) [F.final] (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.functor.final.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.functor.final.cofinal_of_colimit_comp_coyoneda_iso_punit {C : Type v} {D : Type v} (F : C D) [F.final] (I : Π (d : D), ) :

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

@[protected, instance]
def category_theory.functor.initial.category_theory.costructured_arrow.nonempty {C : Type v} {D : Type v} (F : C D) [F.initial] (d : D) :
noncomputable def category_theory.functor.initial.lift {C : Type v} {D : Type v} (F : C D) [F.initial] (d : D) :
C

When F : C ⥤ D is initial, we denote by lift F d an arbitrary choice of object in C such that there exists a morphism F.obj (lift F d) ⟶ d.

Equations
noncomputable def category_theory.functor.initial.hom_to_lift {C : Type v} {D : Type v} (F : C D) [F.initial] (d : D) :
d

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

Equations
noncomputable def category_theory.functor.initial.induction {C : Type v} {D : Type v} (F : C D) [F.initial] {d : D} (Z : Π (X : C), (F.obj X d)Sort u_1) (h₁ : Π (X₁ X₂ : C) (k₁ : F.obj X₁ d) (k₂ : F.obj X₂ d) (f : X₁ X₂), F.map f k₂ = k₁Z X₁ k₁Z X₂ k₂) (h₂ : Π (X₁ X₂ : C) (k₁ : F.obj X₁ d) (k₂ : F.obj X₂ d) (f : X₁ X₂), F.map f k₂ = k₁Z X₂ k₂Z X₁ k₁) {X₀ : C} {k₀ : F.obj X₀ d} (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₀ : F.obj X₀ ⟶ d below), and to show how to transport such a construction both directions along a morphism between such choices.

Equations
@[simp]
theorem category_theory.functor.initial.extend_cone_map_hom {C : Type v} {D : Type v} {F : C D} [F.initial] {E : Type u} {G : D E} (X Y : category_theory.limits.cone (F G)) (f : X Y) :
noncomputable def category_theory.functor.initial.extend_cone {C : Type v} {D : Type v} {F : C D} [F.initial] {E : Type u} {G : D E} :

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

Equations
@[simp]
theorem category_theory.functor.initial.extend_cone_obj_π_app {C : Type v} {D : Type v} {F : C D} [F.initial] {E : Type u} {G : D E} (c : category_theory.limits.cone (F G)) (d : D) :
@[simp]
theorem category_theory.functor.initial.extend_cone_obj_X {C : Type v} {D : Type v} {F : C D} [F.initial] {E : Type u} {G : D E} (c : category_theory.limits.cone (F G)) :
@[simp]
theorem category_theory.functor.initial.limit_cone_comp_aux {C : Type v} {D : Type v} {F : C D} [F.initial] {E : Type u} {G : D E} (s : category_theory.limits.cone (F G)) (j : C) :
s.π.app (F.obj j)) G.map = s.π.app j
@[simp]
theorem category_theory.functor.initial.cones_equiv_counit_iso {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E) :
noncomputable def category_theory.functor.initial.cones_equiv {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E) :

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

Equations
@[simp]
theorem category_theory.functor.initial.cones_equiv_unit_iso {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E) :
@[simp]
theorem category_theory.functor.initial.cones_equiv_inverse {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E) :
@[simp]
theorem category_theory.functor.initial.cones_equiv_functor {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E) :
noncomputable def category_theory.functor.initial.is_limit_whisker_equiv {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :

When F : C ⥤ D is initial, and t : cone G for some G : D ⥤ E, t.whisker F is a limit cone exactly when t is.

Equations
noncomputable def category_theory.functor.initial.is_limit_extend_cone_equiv {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E} (t : category_theory.limits.cone (F G)) :

When F is initial, and t : cone (F ⋙ G), extend_cone.obj t is a limit cone exactly when t is.

Equations
@[simp]
theorem category_theory.functor.initial.limit_cone_comp_cone {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :
noncomputable def category_theory.functor.initial.limit_cone_comp {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :

Given a limit cone over G : D ⥤ E we can construct a limit cone over F ⋙ G.

Equations
@[simp]
theorem category_theory.functor.initial.limit_cone_comp_is_limit {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :
@[protected, instance]
def category_theory.functor.initial.comp_has_limit {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :
theorem category_theory.functor.initial.limit_pre_is_iso_aux {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :
@[protected, instance]
def category_theory.functor.initial.limit_pre_is_iso {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :
noncomputable def category_theory.functor.initial.limit_iso {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} (G : D E)  :

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

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

Equations
@[simp]
theorem category_theory.functor.initial.limit_cone_of_comp_cone {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E} (t : category_theory.limits.limit_cone (F G)) :
@[simp]
theorem category_theory.functor.initial.limit_cone_of_comp_is_limit {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E} (t : category_theory.limits.limit_cone (F G)) :
noncomputable def category_theory.functor.initial.limit_cone_of_comp {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E} (t : category_theory.limits.limit_cone (F G)) :

Given a limit cone over F ⋙ G we can construct a limit cone over G.

Equations
theorem category_theory.functor.initial.has_limit_of_comp {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :

When F is initial, and F ⋙ G has a limit, then G 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.)

noncomputable def category_theory.functor.initial.limit_iso' {C : Type v} {D : Type v} (F : C D) [F.initial] {E : Type u} {G : D E}  :

When F is initial, and F ⋙ G has a limit, then G has a limit also and limit (F ⋙ G) ≅ limit G

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

Equations