mathlib documentation

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:

  1. 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]
def category_theory.cofinal {C : Type v} [category_theory.small_category C] {D : Type v} [category_theory.small_category D] (F : C D) :
Prop

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
Instances

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
theorem category_theory.cofinal.induction {C : Type v} [category_theory.small_category C] {D : Type v} [category_theory.small_category D] (F : C D) [category_theory.cofinal F] {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.

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

Equations

An auxilliary construction for extend_cone, moving op around.

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

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

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

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

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.