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:
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 coconesEquiv) 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_hasColimit, hasColimit_of_comp, and colimitIso.
From 2. we can specialize to G = coyoneda.obj (op d) to obtain 3., as colimitCompCoyonedaIso.
From 3., we prove 1. directly in final_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.
In the end of the file, we characterize the finality of some important induced functors on the
(co)structured arrow category (StructuredArrow.pre and CostructuredArrow.pre) and on the
Grothendieck construction (Grothendieck.pre and Grothendieck.map).
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".
See also #
In CategoryTheory.Filtered.Final we give additional equivalent conditions in the case that
C is filtered.
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
CategoryTheory.Functor.Final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D is final if for every d : D, the comma category of morphisms d ⟶ F.obj c
is connected.
- out (d : D) : IsConnected (StructuredArrow d F)
Instances
class
CategoryTheory.Functor.Initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D is initial if for every d : D, the comma category of morphisms
F.obj c ⟶ d is connected.
- out (d : D) : IsConnected (CostructuredArrow F d)
Instances
instance
CategoryTheory.Functor.final_op_of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
:
instance
CategoryTheory.Functor.initial_op_of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
:
theorem
CategoryTheory.Functor.final_of_initial_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.op.Initial]
:
F.Final
theorem
CategoryTheory.Functor.initial_of_final_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.op.Final]
:
F.Initial
theorem
CategoryTheory.Functor.final_of_adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
:
R.Final
If a functor R : D ⥤ C is a right adjoint, it is final.
theorem
CategoryTheory.Functor.initial_of_adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{L : Functor C D}
{R : Functor D C}
(adj : L ⊣ R)
:
L.Initial
If a functor L : C ⥤ D is a left adjoint, it is initial.
@[instance 100]
instance
CategoryTheory.Functor.final_of_isRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsRightAdjoint]
:
F.Final
@[instance 100]
instance
CategoryTheory.Functor.initial_of_isLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsLeftAdjoint]
:
F.Initial
theorem
CategoryTheory.Functor.final_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F F' : Functor C D}
[F.Final]
(i : F ≅ F')
:
F'.Final
theorem
CategoryTheory.Functor.final_natIso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F F' : Functor C D}
(i : F ≅ F')
:
theorem
CategoryTheory.Functor.initial_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F F' : Functor C D}
[F.Initial]
(i : F ≅ F')
:
F'.Initial
theorem
CategoryTheory.Functor.initial_natIso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F F' : Functor C D}
(i : F ≅ F')
:
instance
CategoryTheory.Functor.Final.instNonemptyStructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
(d : D)
:
Nonempty (StructuredArrow d F)
def
CategoryTheory.Functor.Final.lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
(d : D)
:
C
When F : C ⥤ D is final, 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
Instances For
def
CategoryTheory.Functor.Final.homToLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
(d : D)
:
When F : C ⥤ D is final, we denote by homToLift an arbitrary choice of morphism
d ⟶ F.obj (lift F d).
Equations
Instances For
def
CategoryTheory.Functor.Final.induction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor 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₂) → CategoryStruct.comp 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₂) → CategoryStruct.comp 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 homToLift.
We want to perform some construction (usually just a proof) about
the particular choices lift F d and homToLift 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
- CategoryTheory.Functor.Final.induction F Z h₁ h₂ z = ⋯.some
Instances For
def
CategoryTheory.Functor.Final.extendCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
:
Functor (Limits.Cocone (F.comp G)) (Limits.Cocone G)
Given a cocone over F ⋙ G, we can construct a Cocone G with the same cocone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Final.extendCocone_obj_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cocone (F.comp G))
:
@[simp]
theorem
CategoryTheory.Functor.Final.extendCocone_obj_ι_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cocone (F.comp G))
(X : D)
:
@[simp]
theorem
CategoryTheory.Functor.Final.extendCocone_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{X✝ Y✝ : Limits.Cocone (F.comp G)}
(f : X✝ ⟶ Y✝)
:
theorem
CategoryTheory.Functor.Final.extendCocone_obj_ι_app'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cocone (F.comp G))
{X : D}
{Y : C}
(f : X ⟶ F.obj Y)
:
Alternative equational lemma for (extendCocone c).ι.app in case a lift of the object
is given explicitly.
@[simp]
theorem
CategoryTheory.Functor.Final.colimit_cocone_comp_aux
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(s : Limits.Cocone (F.comp G))
(j : C)
:
def
CategoryTheory.Functor.Final.coconesEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
If F is final,
the category of cocones on F ⋙ G is equivalent to the category of cocones on G,
for any G : D ⥤ E.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
(coconesEquiv F G).unitIso = NatIso.ofComponents
(fun (c : Limits.Cocone (F.comp G)) =>
Limits.Cocones.ext (Iso.refl ((Functor.id (Limits.Cocone (F.comp G))).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
(coconesEquiv F G).counitIso = NatIso.ofComponents
(fun (c : Limits.Cocone G) =>
Limits.Cocones.ext (Iso.refl (((Limits.Cocones.whiskering F).comp extendCocone).obj c).pt) ⋯)
⋯
def
CategoryTheory.Functor.Final.isColimitWhiskerEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.Cocone G)
:
When F : C ⥤ D is final, and t : Cocone G for some G : D ⥤ E,
t.whisker F is a colimit cocone exactly when t is.
Equations
Instances For
def
CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.Cocone (F.comp G))
:
When F is final, and t : Cocone (F ⋙ G),
extendCocone.obj t is a colimit cocone exactly when t is.
Equations
Instances For
def
CategoryTheory.Functor.Final.colimitCoconeComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone G)
:
Limits.ColimitCocone (F.comp G)
Given a colimit cocone over G : D ⥤ E we can construct a colimit cocone over F ⋙ G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeComp_cocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone G)
:
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeComp_isColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone G)
:
@[instance 100]
instance
CategoryTheory.Functor.Final.comp_hasColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasColimit G]
:
Limits.HasColimit (F.comp G)
@[instance 100]
instance
CategoryTheory.Functor.Final.comp_preservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.PreservesColimit G H]
:
Limits.PreservesColimit (F.comp G) H
@[instance 100]
instance
CategoryTheory.Functor.Final.comp_reflectsColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.ReflectsColimit G H]
:
Limits.ReflectsColimit (F.comp G) H
@[instance 100]
instance
CategoryTheory.Functor.Final.compCreatesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[CreatesColimit G H]
:
CreatesColimit (F.comp G) H
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Functor.Final.colimit_pre_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasColimit G]
:
IsIso (Limits.colimit.pre G F)
def
CategoryTheory.Functor.Final.colimitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
:
When F : C ⥤ D is final, and G : D ⥤ E has a colimit, then F ⋙ G has a colimit also and
colimit (F ⋙ G) ≅ colimit G.
Equations
Instances For
theorem
CategoryTheory.Functor.Final.colimitIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
:
theorem
CategoryTheory.Functor.Final.colimitIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
:
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
(X : C)
:
CategoryStruct.comp (Limits.colimit.ι (F.comp G) X) (colimitIso F G).hom = Limits.colimit.ι G (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
(X : C)
{Z : E}
(h : Limits.colimit G ⟶ Z)
:
CategoryStruct.comp (Limits.colimit.ι (F.comp G) X) (CategoryStruct.comp (colimitIso F G).hom h) = CategoryStruct.comp (Limits.colimit.ι G (F.obj X)) h
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
(X : C)
:
CategoryStruct.comp (Limits.colimit.ι G (F.obj X)) (colimitIso F G).inv = Limits.colimit.ι (F.comp G) X
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasColimit G]
(X : C)
{Z : E}
(h : Limits.colimit (F.comp G) ⟶ Z)
:
CategoryStruct.comp (Limits.colimit.ι G (F.obj X)) (CategoryStruct.comp (colimitIso F G).inv h) = CategoryStruct.comp (Limits.colimit.ι (F.comp G) X) h
def
CategoryTheory.Functor.Final.colimIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasColimitsOfShape D E]
[Limits.HasColimitsOfShape C E]
:
A pointfree version of colimitIso, stating that whiskering by F followed by taking the
colimit is isomorpic to taking the colimit on the codomain of F.
Equations
Instances For
def
CategoryTheory.Functor.Final.colimitCoconeOfComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone (F.comp G))
:
Given a colimit cocone over F ⋙ G we can construct a colimit cocone over G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeOfComp_isColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone (F.comp G))
:
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeOfComp_cocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.ColimitCocone (F.comp G))
:
theorem
CategoryTheory.Functor.Final.hasColimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasColimit (F.comp G)]
:
When F is final, 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_hasColimit.)
theorem
CategoryTheory.Functor.Final.preservesColimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.PreservesColimit (F.comp G) H]
:
theorem
CategoryTheory.Functor.Final.reflectsColimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.ReflectsColimit (F.comp G) H]
:
def
CategoryTheory.Functor.Final.createsColimitOfComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[CreatesColimit (F.comp G) H]
:
CreatesColimit G H
If F is final and F ⋙ G creates colimits of H, then so does G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.Final.hasColimitsOfShape_of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasColimitsOfShape C E]
:
theorem
CategoryTheory.Functor.Final.preservesColimitsOfShape_of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[Limits.PreservesColimitsOfShape C H]
:
theorem
CategoryTheory.Functor.Final.reflectsColimitsOfShape_of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[Limits.ReflectsColimitsOfShape C H]
:
def
CategoryTheory.Functor.Final.createsColimitsOfShapeOfFinal
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[CreatesColimitsOfShape C H]
:
If H creates colimits of shape C and F : C ⥤ D is final, then H creates colimits of
shape D.
Equations
- CategoryTheory.Functor.Final.createsColimitsOfShapeOfFinal F H = { CreatesColimit := fun {K : CategoryTheory.Functor D E} => CategoryTheory.Functor.Final.createsColimitOfComp F }
Instances For
theorem
CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel
{C : Type v}
[Category.{v, v} C]
{D : Type u₁}
[Category.{v, u₁} D]
{F : Functor C D}
{d : D}
{f₁ f₂ : (X : C) × (d ⟶ F.obj X)}
(t : Relation.EqvGen (F.comp (coyoneda.obj (Opposite.op d))).ColimitTypeRel f₁ f₂)
:
Zigzag (StructuredArrow.mk f₁.snd) (StructuredArrow.mk f₂.snd)
@[deprecated CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel (since := "2025-06-22")]
theorem
CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel
{C : Type v}
[Category.{v, v} C]
{D : Type u₁}
[Category.{v, u₁} D]
{F : Functor C D}
{d : D}
{f₁ f₂ : (X : C) × (d ⟶ F.obj X)}
(t : Relation.EqvGen (F.comp (coyoneda.obj (Opposite.op d))).ColimitTypeRel f₁ f₂)
:
Zigzag (StructuredArrow.mk f₁.snd) (StructuredArrow.mk f₂.snd)
Alias of CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel.
theorem
CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit
{C : Type v}
[Category.{v, v} C]
{D : Type u₁}
[Category.{v, u₁} D]
(F : Functor C D)
(I : (d : D) → Limits.colimit (F.comp (coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1})
:
F.Final
If colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit for all d : D, then F is final.
theorem
CategoryTheory.Functor.final_of_isTerminal_colimit_comp_yoneda
{C : Type v}
[Category.{v, v} C]
{D : Type u₁}
[Category.{v, u₁} D]
(F : Functor C D)
(h : Limits.IsTerminal (Limits.colimit (F.comp yoneda)))
:
F.Final
A variant of final_of_colimit_comp_coyoneda_iso_pUnit where we bind the various claims
about colimit (F ⋙ coyoneda.obj (Opposite.op d)) for each d : D into a single claim about
the presheaf colimit (F ⋙ yoneda).
def
CategoryTheory.Functor.Final.colimitCompCoyonedaIso
{C : Type v}
[Category.{v, v} C]
{D : Type u₁}
[Category.{v, u₁} D]
(F : Functor C D)
(d : D)
[IsIso (Limits.colimit.pre (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 final),
then colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit
(simply because colimit (coyoneda.obj (op d)) ≅ PUnit).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.final_iff_isIso_colimit_pre
{C : Type v}
[Category.{v, v} C]
{D : Type v}
[Category.{v, v} D]
(F : Functor C D)
:
instance
CategoryTheory.Functor.Initial.instNonemptyCostructuredArrow
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
(d : D)
:
Nonempty (CostructuredArrow F d)
def
CategoryTheory.Functor.Initial.lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor 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
Instances For
def
CategoryTheory.Functor.Initial.homToLift
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
(d : D)
:
When F : C ⥤ D is initial, we denote by homToLift an arbitrary choice of morphism
F.obj (lift F d) ⟶ d.
Equations
Instances For
def
CategoryTheory.Functor.Initial.induction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor 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₂) → CategoryStruct.comp (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₂) → CategoryStruct.comp (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 homToLift.
We want to perform some construction (usually just a proof) about
the particular choices lift F d and homToLift 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
- CategoryTheory.Functor.Initial.induction F Z h₁ h₂ z = ⋯.some
Instances For
def
CategoryTheory.Functor.Initial.extendCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
:
Functor (Limits.Cone (F.comp G)) (Limits.Cone G)
Given a cone over F ⋙ G, we can construct a Cone G with the same cocone point.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Initial.extendCone_obj_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cone (F.comp G))
:
@[simp]
theorem
CategoryTheory.Functor.Initial.extendCone_obj_π_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cone (F.comp G))
(d : D)
:
@[simp]
theorem
CategoryTheory.Functor.Initial.extendCone_map_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{X✝ Y✝ : Limits.Cone (F.comp G)}
(f : X✝ ⟶ Y✝)
:
theorem
CategoryTheory.Functor.Initial.extendCone_obj_π_app'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(c : Limits.Cone (F.comp G))
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
:
Alternative equational lemma for (extendCone c).π.app in case a lift of the object
is given explicitly.
@[simp]
theorem
CategoryTheory.Functor.Initial.limit_cone_comp_aux
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(s : Limits.Cone (F.comp G))
(j : C)
:
def
CategoryTheory.Functor.Initial.conesEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor 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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_counitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
(conesEquiv F G).counitIso = NatIso.ofComponents
(fun (c : Limits.Cone G) => Limits.Cones.ext (Iso.refl (((Limits.Cones.whiskering F).comp extendCone).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_functor
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_unitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
(conesEquiv F G).unitIso = NatIso.ofComponents
(fun (c : Limits.Cone (F.comp G)) => Limits.Cones.ext (Iso.refl ((Functor.id (Limits.Cone (F.comp G))).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_inverse
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
:
def
CategoryTheory.Functor.Initial.isLimitWhiskerEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : 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.
Equations
Instances For
def
CategoryTheory.Functor.Initial.isLimitExtendConeEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.Cone (F.comp G))
:
When F is initial, and t : Cone (F ⋙ G),
extendCone.obj t is a limit cone exactly when t is.
Equations
Instances For
def
CategoryTheory.Functor.Initial.limitConeComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone G)
:
Limits.LimitCone (F.comp G)
Given a limit cone over G : D ⥤ E we can construct a limit cone over F ⋙ G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeComp_isLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone G)
:
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeComp_cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone G)
:
@[instance 100]
instance
CategoryTheory.Functor.Initial.comp_hasLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasLimit G]
:
Limits.HasLimit (F.comp G)
@[instance 100]
instance
CategoryTheory.Functor.Initial.comp_preservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.PreservesLimit G H]
:
Limits.PreservesLimit (F.comp G) H
@[instance 100]
instance
CategoryTheory.Functor.Initial.comp_reflectsLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.ReflectsLimit G H]
:
Limits.ReflectsLimit (F.comp G) H
@[instance 100]
instance
CategoryTheory.Functor.Initial.compCreatesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[CreatesLimit G H]
:
CreatesLimit (F.comp G) H
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Functor.Initial.limit_pre_isIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasLimit G]
:
IsIso (Limits.limit.pre G F)
def
CategoryTheory.Functor.Initial.limitIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasLimit 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.
Equations
Instances For
theorem
CategoryTheory.Functor.Initial.limitIso_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasLimit G]
:
theorem
CategoryTheory.Functor.Initial.limitIso_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
(G : Functor D E)
[Limits.HasLimit G]
:
def
CategoryTheory.Functor.Initial.limIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasLimitsOfShape D E]
[Limits.HasLimitsOfShape C E]
:
A pointfree version of limitIso, stating that whiskering by F followed by taking the
limit is isomorpic to taking the limit on the codomain of F.
Equations
- CategoryTheory.Functor.Initial.limIso F = (CategoryTheory.NatIso.ofComponents (fun (G : CategoryTheory.Functor D E) => (CategoryTheory.Functor.Initial.limitIso F G).symm) ⋯).symm
Instances For
def
CategoryTheory.Functor.Initial.limitConeOfComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone (F.comp G))
:
Given a limit cone over F ⋙ G we can construct a limit cone over G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeOfComp_isLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone (F.comp G))
:
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeOfComp_cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
(t : Limits.LimitCone (F.comp G))
:
theorem
CategoryTheory.Functor.Initial.hasLimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
[Limits.HasLimit (F.comp 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_hasLimit.)
theorem
CategoryTheory.Functor.Initial.preservesLimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.PreservesLimit (F.comp G) H]
:
theorem
CategoryTheory.Functor.Initial.reflectsLimit_of_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[Limits.ReflectsLimit (F.comp G) H]
:
def
CategoryTheory.Functor.Initial.createsLimitOfComp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{G : Functor D E}
{B : Type u₄}
[Category.{v₄, u₄} B]
{H : Functor E B}
[CreatesLimit (F.comp G) H]
:
CreatesLimit G H
If F is initial and F ⋙ G creates limits of H, then so does G.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
[Limits.HasLimitsOfShape C E]
:
theorem
CategoryTheory.Functor.Initial.preservesLimitsOfShape_of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[Limits.PreservesLimitsOfShape C H]
:
theorem
CategoryTheory.Functor.Initial.reflectsLimitsOfShape_of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[Limits.ReflectsLimitsOfShape C H]
:
def
CategoryTheory.Functor.Initial.createsLimitsOfShapeOfInitial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
{E : Type u₃}
[Category.{v₃, u₃} E]
{B : Type u₄}
[Category.{v₄, u₄} B]
(H : Functor E B)
[CreatesLimitsOfShape C H]
:
If H creates limits of shape C and F : C ⥤ D is initial, then H creates limits of shape
D.
Equations
- CategoryTheory.Functor.Initial.createsLimitsOfShapeOfInitial F H = { CreatesLimit := fun {K : CategoryTheory.Functor D E} => CategoryTheory.Functor.Initial.createsLimitOfComp F }
Instances For
theorem
CategoryTheory.Functor.final_of_comp_full_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Full]
[G.Faithful]
[(F.comp G).Final]
:
F.Final
The hypotheses also imply that G is final, see final_of_comp_full_faithful'.
theorem
CategoryTheory.Functor.initial_of_comp_full_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Full]
[G.Faithful]
[(F.comp G).Initial]
:
F.Initial
The hypotheses also imply that G is initial, see initial_of_comp_full_faithful'.
theorem
CategoryTheory.Functor.final_comp_equivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Final]
[G.IsEquivalence]
:
See also the strictly more general final_comp below.
theorem
CategoryTheory.Functor.initial_comp_equivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Initial]
[G.IsEquivalence]
:
See also the strictly more general initial_comp below.
theorem
CategoryTheory.Functor.final_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
[G.Final]
:
See also the strictly more general final_comp below.
theorem
CategoryTheory.Functor.initial_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
[G.Initial]
:
See also the strictly more general initial_comp below.
theorem
CategoryTheory.Functor.final_of_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
[(F.comp G).Final]
:
G.Final
See also the strictly more general final_of_final_comp below.
theorem
CategoryTheory.Functor.initial_of_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
[(F.comp G).Initial]
:
G.Initial
See also the strictly more general initial_of_initial_comp below.
theorem
CategoryTheory.Functor.final_iff_comp_equivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.IsEquivalence]
:
See also the strictly more general final_iff_comp_final_full_faithful below.
theorem
CategoryTheory.Functor.final_iff_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
:
See also the strictly more general final_iff_final_comp below.
theorem
CategoryTheory.Functor.initial_iff_comp_equivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.IsEquivalence]
:
See also the strictly more general initial_iff_comp_initial_full_faithful below.
theorem
CategoryTheory.Functor.initial_iff_equivalence_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.IsEquivalence]
:
See also the strictly more general initial_iff_initial_comp below.
instance
CategoryTheory.Functor.final_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[hF : F.Final]
[hG : G.Final]
:
instance
CategoryTheory.Functor.initial_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Initial]
[G.Initial]
:
theorem
CategoryTheory.Functor.final_of_final_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[hF : F.Final]
[hFG : (F.comp G).Final]
:
G.Final
theorem
CategoryTheory.Functor.initial_of_initial_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Initial]
[(F.comp G).Initial]
:
G.Initial
theorem
CategoryTheory.Functor.final_of_comp_full_faithful'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Full]
[G.Faithful]
[(F.comp G).Final]
:
G.Final
The hypotheses also imply that F is final, see final_of_comp_full_faithful.
theorem
CategoryTheory.Functor.initial_of_comp_full_faithful'
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Full]
[G.Faithful]
[(F.comp G).Initial]
:
G.Initial
The hypotheses also imply that F is initial, see initial_of_comp_full_faithful.
theorem
CategoryTheory.Functor.final_iff_comp_final_full_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Final]
[G.Full]
[G.Faithful]
:
theorem
CategoryTheory.Functor.initial_iff_comp_initial_full_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.Initial]
[G.Full]
[G.Faithful]
:
theorem
CategoryTheory.Functor.final_iff_final_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Final]
:
theorem
CategoryTheory.Functor.initial_iff_initial_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.Initial]
:
theorem
CategoryTheory.Functor.final_fromPUnit_of_isTerminal
{C : Type u₁}
[Category.{v₁, u₁} C]
{c : C}
(hc : Limits.IsTerminal c)
:
theorem
CategoryTheory.Functor.initial_fromPUnit_of_isInitial
{C : Type u₁}
[Category.{v₁, u₁} C]
{c : C}
(hc : Limits.IsInitial c)
:
theorem
CategoryTheory.IsFilteredOrEmpty.of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
[IsFilteredOrEmpty C]
:
Final functors preserve filteredness.
This can be seen as a generalization of IsFiltered.of_right_adjoint (which states that right
adjoints preserve filteredness), as right adjoints are always final, see final_of_adjunction.
theorem
CategoryTheory.IsFiltered.of_final
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Final]
[IsFiltered C]
:
Final functors preserve filteredness.
This can be seen as a generalization of IsFiltered.of_right_adjoint (which states that right
adjoints preserve filteredness), as right adjoints are always final, see final_of_adjunction.
theorem
CategoryTheory.IsCofilteredOrEmpty.of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
[IsCofilteredOrEmpty C]
:
Initial functors preserve cofilteredness.
This can be seen as a generalization of IsCofiltered.of_left_adjoint (which states that left
adjoints preserve cofilteredness), as right adjoints are always initial,
see initial_of_adjunction.
theorem
CategoryTheory.IsCofiltered.of_initial
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Initial]
[IsCofiltered C]
:
Initial functors preserve cofilteredness.
This can be seen as a generalization of IsCofiltered.of_left_adjoint (which states that left
adjoints preserve cofilteredness), as right adjoints are always initial,
see initial_of_adjunction.
instance
CategoryTheory.StructuredArrow.final_pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(T : Functor C D)
[T.Final]
(S : Functor D E)
(X : E)
:
The functor StructuredArrow.pre X T S is final if T is final.
instance
CategoryTheory.CostructuredArrow.initial_pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(T : Functor C D)
[T.Initial]
(S : Functor D E)
(X : E)
:
The functor CostructuredArrow.pre X T S is initial if T is initial.
def
CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor D Cat)
(G : Functor C D)
(d : D)
(f : ↑(F.obj d))
:
A prefunctor mapping structured arrows on G to structured arrows on pre F G with their
action on fibers being the identity.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.Grothendieck.final_pre
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor D Cat)
(G : Functor C D)
[hG : G.Final]
:
def
CategoryTheory.Grothendieck.fiberwiseColimitMapCompEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{F G : Functor C Cat}
(α : F ⟶ G)
[∀ (X : C), Functor.Final (α.app X)]
(H : Functor (Grothendieck G) (Type u₂))
:
A natural transformation α : F ⟶ G between functors F G : C ⥤ Cat which is is final on each
fiber (α.app X) induces an equivalence of fiberwise colimits of map α ⋙ H and H for each
functor H : Grothendieck G ⥤ Type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Grothendieck.final_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{F G : Functor C Cat}
(α : F ⟶ G)
[hα : ∀ (X : C), Functor.Final (α.app X)]
:
The functor Grothendieck.map α for a natural transformation α : F ⟶ G, with
F G : C ⥤ Cat, is final if for each X : C, the functor α.app X is final.
instance
CategoryTheory.instFinalProdProd
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{C' : Type u₃}
[Category.{v₃, u₃} C']
{D' : Type u₄}
[Category.{v₄, u₄} D']
(F : Functor C D)
(G : Functor C' D')
[F.Final]
[G.Final]
:
theorem
CategoryTheory.ObjectProperty.initial_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
(P : ObjectProperty C)
(h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d))
:
For the full subcategory induced by an object property P on C, to show initiality of
the inclusion functor it is enough to consider arrows to objects outside of the subcategory.