mathlib3 documentation

category_theory.limits.final

Final and initial functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.initial {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) :
Prop

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]
@[protected, instance]
theorem category_theory.functor.final_of_adjunction {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {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 u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {L : C D} {R : D C} (adj : L R) :

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

noncomputable def category_theory.functor.final.lift {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

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 u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

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

Equations

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

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

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

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

noncomputable def category_theory.functor.initial.lift {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

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 u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (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

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

Equations

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

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