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:
F : C ⥤ Dis cofinal.- Every functor
G : D ⥤ Ehas a colimit if and only ifF ⋙ Gdoes, and these colimits are isomorphic viacolimit.pre G F. 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 #
- 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!)
@[class]
structure
category_theory.cofinal
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D) :
Prop
- out : ∀ (d : D), category_theory.is_connected (category_theory.structured_arrow d F)
A functor F : C ⥤ D is cofinal if for every d : D, the comma category of morphisms d ⟶ F.obj c
is connected.
@[protected, instance]
def
category_theory.cofinal.category_theory.structured_arrow.nonempty
{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) :
def
category_theory.cofinal.lift
{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) :
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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
(d : D) :
d ⟶ F.obj (category_theory.cofinal.lift F 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
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.
@[simp]
theorem
category_theory.cofinal.extend_cocone_obj_ι_app
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cocone (F ⋙ G))
(X : D) :
(category_theory.cofinal.extend_cocone.obj c).ι.app X = G.map (category_theory.cofinal.hom_to_lift F X) ≫ c.ι.app (category_theory.cofinal.lift F X)
@[simp]
theorem
category_theory.cofinal.extend_cocone_map_hom
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cocone (F ⋙ G)) :
def
category_theory.cofinal.extend_cocone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E} :
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' := _}
@[simp]
theorem
category_theory.cofinal.colimit_cocone_comp_aux
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(s : category_theory.limits.cocone (F ⋙ G))
(j : C) :
def
category_theory.cofinal.extend_cone_cone_to_cocone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{F : C ⥤ D}
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cone (F.op ⋙ H)) :
An auxilliary construction for extend_cone, moving op around.
Equations
- category_theory.cofinal.extend_cone_cone_to_cocone c = {X := opposite.op c.X, ι := {app := λ (j : C), (c.π.app (opposite.op j)).op, naturality' := _}}
@[simp]
theorem
category_theory.cofinal.extend_cone_cone_to_cocone_X
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{F : C ⥤ D}
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cone (F.op ⋙ H))
(j : C) :
(category_theory.cofinal.extend_cone_cone_to_cocone c).ι.app j = (c.π.app (opposite.op j)).op
def
category_theory.cofinal.extend_cone_cocone_to_cone
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cocone H.right_op) :
An auxilliary construction for extend_cone, moving op around.
Equations
- category_theory.cofinal.extend_cone_cocone_to_cone c = {X := opposite.unop c.X, π := {app := λ (j : Dᵒᵖ), (c.ι.app (opposite.unop j)).unop, naturality' := _}}
@[simp]
theorem
category_theory.cofinal.extend_cone_cocone_to_cone_π_app
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cocone H.right_op)
(j : Dᵒᵖ) :
(category_theory.cofinal.extend_cone_cocone_to_cone c).π.app j = (c.ι.app (opposite.unop j)).unop
@[simp]
theorem
category_theory.cofinal.extend_cone_cocone_to_cone_X
{D : Type v}
[category_theory.small_category D]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cocone H.right_op) :
def
category_theory.cofinal.extend_cone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E} :
Given a cone over F.op ⋙ H, we can construct a cone H with the same cone point.
Equations
- category_theory.cofinal.extend_cone = {obj := λ (c : category_theory.limits.cone (F.op ⋙ H)), category_theory.cofinal.extend_cone_cocone_to_cone (category_theory.cofinal.extend_cocone.obj (category_theory.cofinal.extend_cone_cone_to_cocone c)), map := λ (X Y : category_theory.limits.cone (F.op ⋙ H)) (f : X ⟶ Y), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.cofinal.extend_cone_obj
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(c : category_theory.limits.cone (F.op ⋙ H)) :
@[simp]
theorem
category_theory.cofinal.extend_cone_map_hom
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(s : category_theory.limits.cone (F.op ⋙ H))
(j : Cᵒᵖ) :
s.π.app (opposite.op (category_theory.cofinal.lift F (F.obj (opposite.unop j)))) ≫ H.map (category_theory.cofinal.hom_to_lift F (F.obj (opposite.unop j))).op = s.π.app j
@[simp]
theorem
category_theory.cofinal.cocones_equiv_unit_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(G : D ⥤ E) :
(category_theory.cofinal.cocones_equiv F G).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) _) _
@[simp]
theorem
category_theory.cofinal.cocones_equiv_functor
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(G : D ⥤ E) :
@[simp]
theorem
category_theory.cofinal.cocones_equiv_inverse
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(G : D ⥤ E) :
def
category_theory.cofinal.cocones_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(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
- category_theory.cofinal.cocones_equiv F G = {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' := _}
@[simp]
theorem
category_theory.cofinal.cocones_equiv_counit_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(G : D ⥤ E) :
@[simp]
theorem
category_theory.cofinal.cones_equiv_functor
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(H : Dᵒᵖ ⥤ E) :
@[simp]
theorem
category_theory.cofinal.cones_equiv_unit_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(H : Dᵒᵖ ⥤ E) :
(category_theory.cofinal.cones_equiv F H).unit_iso = category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (F.op ⋙ H)), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone (F.op ⋙ H))).obj c).X) _) _
def
category_theory.cofinal.cones_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(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
- category_theory.cofinal.cones_equiv F H = {functor := category_theory.cofinal.extend_cone H, inverse := category_theory.limits.cones.whiskering F.op, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (F.op ⋙ H)), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone (F.op ⋙ H))).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone H), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.whiskering F.op ⋙ category_theory.cofinal.extend_cone).obj c).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.cofinal.cones_equiv_counit_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(H : Dᵒᵖ ⥤ E) :
@[simp]
theorem
category_theory.cofinal.cones_equiv_inverse
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(H : Dᵒᵖ ⥤ E) :
def
category_theory.cofinal.is_colimit_whisker_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.cocone G) :
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.
def
category_theory.cofinal.is_limit_whisker_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(t : category_theory.limits.cone H) :
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.
def
category_theory.cofinal.is_colimit_extend_cocone_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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.
def
category_theory.cofinal.is_limit_extend_cone_equiv
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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.
@[simp]
theorem
category_theory.cofinal.colimit_cocone_comp_is_colimit
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone G) :
@[simp]
theorem
category_theory.cofinal.colimit_cocone_comp_cocone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone G) :
def
category_theory.cofinal.colimit_cocone_comp
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone G) :
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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(t : category_theory.limits.limit_cone H) :
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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(t : category_theory.limits.limit_cone H) :
@[simp]
theorem
category_theory.cofinal.limit_cone_comp_is_limit
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(t : category_theory.limits.limit_cone H) :
@[protected, instance]
def
category_theory.cofinal.comp_has_colimit
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit G] :
@[protected, instance]
def
category_theory.cofinal.comp_has_limit
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
[category_theory.limits.has_limit H] :
theorem
category_theory.cofinal.colimit_pre_is_iso_aux
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
{t : category_theory.limits.cocone G}
(P : category_theory.limits.is_colimit t) :
(⇑((category_theory.cofinal.is_colimit_whisker_equiv F t).symm) P).desc (category_theory.limits.cocone.whisker F t) = 𝟙 t.X
@[protected, instance]
def
category_theory.cofinal.colimit_pre_is_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit G] :
theorem
category_theory.cofinal.limit_pre_is_iso_aux
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
{t : category_theory.limits.cone H}
(P : category_theory.limits.is_limit t) :
(⇑((category_theory.cofinal.is_limit_whisker_equiv F t).symm) P).lift (category_theory.limits.cone.whisker F.op t) = 𝟙 t.X
@[protected, instance]
def
category_theory.cofinal.limit_pre_is_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
[category_theory.limits.has_limit H] :
def
category_theory.cofinal.colimit_iso
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(G : D ⥤ E)
[category_theory.limits.has_colimit G] :
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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
(H : Dᵒᵖ ⥤ E)
[category_theory.limits.has_limit H] :
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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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.
@[simp]
theorem
category_theory.cofinal.colimit_cocone_of_comp_cocone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone (F ⋙ G)) :
@[simp]
theorem
category_theory.cofinal.limit_cone_of_comp_cone
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{H : Dᵒᵖ ⥤ E}
(t : category_theory.limits.limit_cone (F.op ⋙ H)) :
def
category_theory.cofinal.limit_cone_of_comp
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit (F ⋙ 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.)
theorem
category_theory.cofinal.has_limit_of_comp
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit (F ⋙ G)] :
When F is cofinal, and F ⋙ G has a colimit, then G has a colimit also and
colimit (F ⋙ G) ≅ colimit G
def
category_theory.cofinal.limit_iso'
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
{E : Type u}
[category_theory.category E]
{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}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
(d : D)
[category_theory.is_iso (category_theory.limits.colimit.pre (category_theory.coyoneda.obj (opposite.op d)) F)] :
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).
theorem
category_theory.cofinal.zigzag_of_eqv_gen_quot_rel
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
{F : C ⥤ D}
{d : D}
{f₁ f₂ : Σ (X : C), d ⟶ F.obj X}
(t : eqv_gen (category_theory.limits.types.quot.rel (F ⋙ category_theory.coyoneda.obj (opposite.op d))) f₁ f₂) :
theorem
category_theory.cofinal.cofinal_of_colimit_comp_coyoneda_iso_punit
{C : Type v}
[category_theory.small_category C]
{D : Type v}
[category_theory.small_category D]
(F : C ⥤ D)
[category_theory.cofinal F]
(I : Π (d : D), category_theory.limits.colimit (F ⋙ category_theory.coyoneda.obj (opposite.op d)) ≅ punit) :
If colimit (F ⋙ coyoneda.obj (op d)) ≅ punit for all d : D, then F is cofinal.