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:
F : C ⥤ Dis final.- 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.
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 #
- 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.functor.final
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.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 final if for every d : D, the comma category of morphisms d ⟶ F.obj c
is connected.
@[class]
structure
category_theory.functor.initial
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- out : ∀ (d : D), category_theory.is_connected (category_theory.costructured_arrow F d)
A functor F : C ⥤ D is initial if for every d : D, the comma category of morphisms
F.obj c ⟶ d is connected.
@[protected, instance]
def
category_theory.functor.final_op_of_initial
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial] :
@[protected, instance]
def
category_theory.functor.initial_op_of_final
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final] :
theorem
category_theory.functor.final_of_initial_op
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.op.initial] :
F.final
theorem
category_theory.functor.initial_of_final_op
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.op.final] :
F.initial
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) :
R.final
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) :
L.initial
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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[h : category_theory.is_right_adjoint F] :
F.final
@[protected, instance]
def
category_theory.functor.initial_of_is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[h : category_theory.is_left_adjoint F] :
F.initial
@[protected, instance]
def
category_theory.functor.final.category_theory.structured_arrow.nonempty
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
(d : D) :
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
noncomputable
def
category_theory.functor.final.hom_to_lift
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
(d : D) :
d ⟶ F.obj (category_theory.functor.final.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
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
- category_theory.functor.final.induction F Z h₁ h₂ z = _.some
@[simp]
theorem
category_theory.functor.final.extend_cocone_obj_X
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cocone (F ⋙ G)) :
@[simp]
theorem
category_theory.functor.final.extend_cocone_obj_ι_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cocone (F ⋙ G))
(X : D) :
noncomputable
def
category_theory.functor.final.extend_cocone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.final]
{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.functor.final.extend_cocone = {obj := λ (c : category_theory.limits.cocone (F ⋙ G)), {X := c.X, ι := {app := λ (X : D), G.map (category_theory.functor.final.hom_to_lift F X) ≫ c.ι.app (category_theory.functor.final.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.functor.final.extend_cocone_map_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.final]
{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.functor.final.colimit_cocone_comp_aux
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(s : category_theory.limits.cocone (F ⋙ G))
(j : C) :
@[simp]
theorem
category_theory.functor.final.cocones_equiv_inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
noncomputable
def
category_theory.functor.final.cocones_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.functor.final.cocones_equiv F G = {functor := category_theory.functor.final.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.functor.final.extend_cocone).obj c).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.functor.final.cocones_equiv_functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
@[simp]
theorem
category_theory.functor.final.cocones_equiv_counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
(category_theory.functor.final.cocones_equiv F G).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.functor.final.extend_cocone).obj c).X) _) _
@[simp]
theorem
category_theory.functor.final.cocones_equiv_unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
(category_theory.functor.final.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) _) _
noncomputable
def
category_theory.functor.final.is_colimit_whisker_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.
noncomputable
def
category_theory.functor.final.is_colimit_extend_cocone_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.
@[simp]
theorem
category_theory.functor.final.colimit_cocone_comp_is_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone G) :
noncomputable
def
category_theory.functor.final.colimit_cocone_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.
@[simp]
theorem
category_theory.functor.final.colimit_cocone_comp_cocone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone G) :
@[protected, instance]
def
category_theory.functor.final.comp_has_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit G] :
theorem
category_theory.functor.final.colimit_pre_is_iso_aux
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.functor.final.is_colimit_whisker_equiv F t).symm) P).desc (category_theory.limits.cocone.whisker F t) = 𝟙 t.X
@[protected, instance]
def
category_theory.functor.final.colimit_pre_is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_colimit G] :
noncomputable
def
category_theory.functor.final.colimit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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
@[simp]
theorem
category_theory.functor.final.colimit_cocone_of_comp_is_colimit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone (F ⋙ G)) :
@[simp]
theorem
category_theory.functor.final.colimit_cocone_of_comp_cocone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.colimit_cocone (F ⋙ G)) :
noncomputable
def
category_theory.functor.final.colimit_cocone_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.
theorem
category_theory.functor.final.has_colimit_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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.)
noncomputable
def
category_theory.functor.final.colimit_iso'
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
{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
noncomputable
def
category_theory.functor.final.colimit_comp_coyoneda_iso
{C : Type v}
[category_theory.category C]
{D : Type v}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
(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.functor.final.zigzag_of_eqv_gen_quot_rel
{C : Type v}
[category_theory.category C]
{D : Type v}
[category_theory.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.functor.final.cofinal_of_colimit_comp_coyoneda_iso_punit
{C : Type v}
[category_theory.category C]
{D : Type v}
[category_theory.category D]
(F : C ⥤ D)
[F.final]
(I : Π (d : D), category_theory.limits.colimit (F ⋙ category_theory.coyoneda.obj (opposite.op d)) ≅ punit) :
F.final
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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
(d : D) :
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
noncomputable
def
category_theory.functor.initial.hom_to_lift
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
(d : D) :
F.obj (category_theory.functor.initial.lift F 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 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
- category_theory.functor.initial.induction F Z h₁ h₂ z = _.some
@[simp]
theorem
category_theory.functor.initial.extend_cone_map_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(X Y : category_theory.limits.cone (F ⋙ G))
(f : X ⟶ Y) :
noncomputable
def
category_theory.functor.initial.extend_cone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E} :
Given a cone over F ⋙ G, we can construct a cone G with the same cocone point.
Equations
- category_theory.functor.initial.extend_cone = {obj := λ (c : category_theory.limits.cone (F ⋙ G)), {X := c.X, π := {app := λ (d : D), c.π.app (category_theory.functor.initial.lift F d) ≫ G.map (category_theory.functor.initial.hom_to_lift F d), naturality' := _}}, map := λ (X Y : category_theory.limits.cone (F ⋙ G)) (f : X ⟶ Y), {hom := f.hom, w' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.functor.initial.extend_cone_obj_π_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cone (F ⋙ G))
(d : D) :
@[simp]
theorem
category_theory.functor.initial.extend_cone_obj_X
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(c : category_theory.limits.cone (F ⋙ G)) :
@[simp]
theorem
category_theory.functor.initial.limit_cone_comp_aux
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(s : category_theory.limits.cone (F ⋙ G))
(j : C) :
@[simp]
theorem
category_theory.functor.initial.cones_equiv_counit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
(category_theory.functor.initial.cones_equiv F G).counit_iso = category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone G), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.whiskering F ⋙ category_theory.functor.initial.extend_cone).obj c).X) _) _
noncomputable
def
category_theory.functor.initial.cones_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(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
- category_theory.functor.initial.cones_equiv F G = {functor := category_theory.functor.initial.extend_cone G, inverse := category_theory.limits.cones.whiskering F, unit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (F ⋙ G)), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone (F ⋙ G))).obj c).X) _) _, counit_iso := category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone G), category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.whiskering F ⋙ category_theory.functor.initial.extend_cone).obj c).X) _) _, functor_unit_iso_comp' := _}
@[simp]
theorem
category_theory.functor.initial.cones_equiv_unit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
(category_theory.functor.initial.cones_equiv F G).unit_iso = category_theory.nat_iso.of_components (λ (c : category_theory.limits.cone (F ⋙ G)), category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 (category_theory.limits.cone (F ⋙ G))).obj c).X) _) _
@[simp]
theorem
category_theory.functor.initial.cones_equiv_inverse
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
@[simp]
theorem
category_theory.functor.initial.cones_equiv_functor
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E) :
noncomputable
def
category_theory.functor.initial.is_limit_whisker_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.cone G) :
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.
noncomputable
def
category_theory.functor.initial.is_limit_extend_cone_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{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.
@[simp]
theorem
category_theory.functor.initial.limit_cone_comp_cone
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.limit_cone G) :
noncomputable
def
category_theory.functor.initial.limit_cone_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.limit_cone G) :
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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.limit_cone G) :
@[protected, instance]
def
category_theory.functor.initial.comp_has_limit
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_limit G] :
theorem
category_theory.functor.initial.limit_pre_is_iso_aux
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
{t : category_theory.limits.cone G}
(P : category_theory.limits.is_limit t) :
(⇑((category_theory.functor.initial.is_limit_whisker_equiv F t).symm) P).lift (category_theory.limits.cone.whisker F t) = 𝟙 t.X
@[protected, instance]
def
category_theory.functor.initial.limit_pre_is_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_limit G] :
noncomputable
def
category_theory.functor.initial.limit_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
(G : D ⥤ E)
[category_theory.limits.has_limit G] :
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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
(t : category_theory.limits.limit_cone (F ⋙ G)) :
noncomputable
def
category_theory.functor.initial.limit_cone_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{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.
theorem
category_theory.functor.initial.has_limit_of_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_limit (F ⋙ G)] :
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 u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.initial]
{E : Type u₃}
[category_theory.category E]
{G : D ⥤ E}
[category_theory.limits.has_limit (F ⋙ G)] :
When F is initial, and F ⋙ G has a limit, then G has a limit also and
limit (F ⋙ G) ≅ limit G