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.
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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.
See https://stacks.math.columbia.edu/tag/04E6
- out : ∀ (d : D), CategoryTheory.IsConnected (CategoryTheory.StructuredArrow d F)
Instances
class
CategoryTheory.Functor.Initial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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), CategoryTheory.IsConnected (CategoryTheory.CostructuredArrow F d)
Instances
instance
CategoryTheory.Functor.final_op_of_initial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
:
F.op.Final
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.initial_op_of_final
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
:
F.op.Initial
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.final_of_initial_op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.op.Initial]
:
F.Final
theorem
CategoryTheory.Functor.initial_of_final_op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.op.Final]
:
F.Initial
theorem
CategoryTheory.Functor.final_of_adjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{L : CategoryTheory.Functor C D}
{R : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.IsRightAdjoint]
:
F.Final
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Functor.initial_of_isLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.IsLeftAdjoint]
:
F.Initial
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.final_of_natIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F F' : CategoryTheory.Functor C D}
[F.Final]
(i : F ≅ F')
:
F'.Final
theorem
CategoryTheory.Functor.final_natIso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F F' : CategoryTheory.Functor C D}
(i : F ≅ F')
:
F.Final ↔ F'.Final
theorem
CategoryTheory.Functor.initial_of_natIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F F' : CategoryTheory.Functor C D}
[F.Initial]
(i : F ≅ F')
:
F'.Initial
theorem
CategoryTheory.Functor.initial_natIso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F F' : CategoryTheory.Functor C D}
(i : F ≅ F')
:
F.Initial ↔ F'.Initial
instance
CategoryTheory.Functor.Final.instNonemptyStructuredArrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
(d : D)
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Functor.Final.lift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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
- CategoryTheory.Functor.Final.lift F d = (Classical.arbitrary (CategoryTheory.StructuredArrow d F)).right
Instances For
def
CategoryTheory.Functor.Final.homToLift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
(d : D)
:
d ⟶ F.obj (CategoryTheory.Functor.Final.lift F 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₂) → CategoryTheory.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₂) → CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cocone (F.comp G))
:
(CategoryTheory.Functor.Final.extendCocone.obj c).pt = c.pt
@[simp]
theorem
CategoryTheory.Functor.Final.extendCocone_obj_ι_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cocone (F.comp G))
(X : D)
:
(CategoryTheory.Functor.Final.extendCocone.obj c).ι.app X = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F X))
(c.ι.app (CategoryTheory.Functor.Final.lift F X))
@[simp]
theorem
CategoryTheory.Functor.Final.extendCocone_map_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
{X✝ Y✝ : CategoryTheory.Limits.Cocone (F.comp G)}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Functor.Final.extendCocone.map f).hom = f.hom
theorem
CategoryTheory.Functor.Final.extendCocone_obj_ι_app'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cocone (F.comp G))
{X : D}
{Y : C}
(f : X ⟶ F.obj Y)
:
(CategoryTheory.Functor.Final.extendCocone.obj c).ι.app X = CategoryTheory.CategoryStruct.comp (G.map f) (c.ι.app 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(s : CategoryTheory.Limits.Cocone (F.comp G))
(j : C)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.Final.homToLift F (F.obj j)))
(s.ι.app (CategoryTheory.Functor.Final.lift F (F.obj j))) = s.ι.app j
def
CategoryTheory.Functor.Final.coconesEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.Limits.Cocone (F.comp G) ≌ CategoryTheory.Limits.Cocone G
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_functor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Final.coconesEquiv F G).functor = CategoryTheory.Functor.Final.extendCocone
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_unitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Final.coconesEquiv F G).unitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cocone (F.comp G)) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone (F.comp G))).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Final.coconesEquiv_counitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Final.coconesEquiv F G).counitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cocone G) =>
CategoryTheory.Limits.Cocones.ext
(CategoryTheory.Iso.refl
(((CategoryTheory.Limits.Cocones.whiskering F).comp CategoryTheory.Functor.Final.extendCocone).obj c).pt)
⋯)
⋯
def
CategoryTheory.Functor.Final.isColimitWhiskerEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.Cocone (F.comp G))
:
CategoryTheory.Limits.IsColimit (CategoryTheory.Functor.Final.extendCocone.obj t) ≃ CategoryTheory.Limits.IsColimit t
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.ColimitCocone G)
:
CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.ColimitCocone G)
:
(CategoryTheory.Functor.Final.colimitCoconeComp F t).cocone = CategoryTheory.Limits.Cocone.whisker F t.cocone
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeComp_isColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.ColimitCocone G)
:
(CategoryTheory.Functor.Final.colimitCoconeComp F t).isColimit = (CategoryTheory.Functor.Final.isColimitWhiskerEquiv F t.cocone).symm t.isColimit
@[instance 100]
instance
CategoryTheory.Functor.Final.comp_hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.Limits.HasColimit G]
:
CategoryTheory.Limits.HasColimit (F.comp G)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.Final.colimit_pre_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.Limits.HasColimit G]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Functor.Final.colimitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
:
CategoryTheory.Limits.colimit (F.comp G) ≅ CategoryTheory.Limits.colimit 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
https://stacks.math.columbia.edu/tag/04E7
Equations
Instances For
theorem
CategoryTheory.Functor.Final.colimitIso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
:
theorem
CategoryTheory.Functor.Final.colimitIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
:
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
(X : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X)
(CategoryTheory.Functor.Final.colimitIso F G).hom = CategoryTheory.Limits.colimit.ι G (F.obj X)
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
(X : C)
{Z : E}
(h : CategoryTheory.Limits.colimit G ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Final.colimitIso F G).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X)) h
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
(X : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X))
(CategoryTheory.Functor.Final.colimitIso F G).inv = CategoryTheory.Limits.colimit.ι (F.comp G) X
@[simp]
theorem
CategoryTheory.Functor.Final.ι_colimitIso_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasColimit G]
(X : C)
{Z : E}
(h : CategoryTheory.Limits.colimit (F.comp G) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (F.obj X))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Final.colimitIso F G).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) X) h
def
CategoryTheory.Functor.Final.colimIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasColimitsOfShape D E]
[CategoryTheory.Limits.HasColimitsOfShape C E]
:
((CategoryTheory.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.colim ≅ CategoryTheory.Limits.colim
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.ColimitCocone (F.comp G))
:
(CategoryTheory.Functor.Final.colimitCoconeOfComp F t).isColimit = (CategoryTheory.Functor.Final.isColimitExtendCoconeEquiv F t.cocone).symm t.isColimit
@[simp]
theorem
CategoryTheory.Functor.Final.colimitCoconeOfComp_cocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.ColimitCocone (F.comp G))
:
(CategoryTheory.Functor.Final.colimitCoconeOfComp F t).cocone = CategoryTheory.Functor.Final.extendCocone.obj t.cocone
theorem
CategoryTheory.Functor.Final.hasColimit_of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.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.hasColimitsOfShape_of_final
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasColimitsOfShape C E]
:
theorem
CategoryTheory.Functor.Final.zigzag_of_eqvGen_quot_rel
{C : Type v}
[CategoryTheory.Category.{v, v} C]
{D : Type u₁}
[CategoryTheory.Category.{v, u₁} D]
{F : CategoryTheory.Functor C D}
{d : D}
{f₁ f₂ : (X : C) × (d ⟶ F.obj X)}
(t :
Relation.EqvGen (CategoryTheory.Limits.Types.Quot.Rel (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d)))) f₁ f₂)
:
theorem
CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit
{C : Type v}
[CategoryTheory.Category.{v, v} C]
{D : Type u₁}
[CategoryTheory.Category.{v, u₁} D]
(F : CategoryTheory.Functor C D)
(I : (d : D) → CategoryTheory.Limits.colimit (F.comp (CategoryTheory.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}
[CategoryTheory.Category.{v, v} C]
{D : Type u₁}
[CategoryTheory.Category.{v, u₁} D]
(F : CategoryTheory.Functor C D)
(h : CategoryTheory.Limits.IsTerminal (CategoryTheory.Limits.colimit (F.comp CategoryTheory.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}
[CategoryTheory.Category.{v, v} C]
{D : Type u₁}
[CategoryTheory.Category.{v, u₁} D]
(F : CategoryTheory.Functor C D)
(d : D)
[CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre (CategoryTheory.coyoneda.obj (Opposite.op d)) F)]
:
CategoryTheory.Limits.colimit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1}
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}
[CategoryTheory.Category.{v, v} C]
{D : Type v}
[CategoryTheory.Category.{v, v} D]
(F : CategoryTheory.Functor C D)
:
F.Final ↔ ∀ (G : CategoryTheory.Functor D (Type v)), CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre G F)
instance
CategoryTheory.Functor.Initial.instNonemptyCostructuredArrow
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
(d : D)
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Functor.Initial.lift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
(d : D)
:
F.obj (CategoryTheory.Functor.Initial.lift F 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₂) → CategoryTheory.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₂) → CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
:
CategoryTheory.Functor (CategoryTheory.Limits.Cone (F.comp G)) (CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cone (F.comp G))
:
(CategoryTheory.Functor.Initial.extendCone.obj c).pt = c.pt
@[simp]
theorem
CategoryTheory.Functor.Initial.extendCone_map_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
{X✝ Y✝ : CategoryTheory.Limits.Cone (F.comp G)}
(f : X✝ ⟶ Y✝)
:
(CategoryTheory.Functor.Initial.extendCone.map f).hom = f.hom
@[simp]
theorem
CategoryTheory.Functor.Initial.extendCone_obj_π_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cone (F.comp G))
(d : D)
:
(CategoryTheory.Functor.Initial.extendCone.obj c).π.app d = CategoryTheory.CategoryStruct.comp (c.π.app (CategoryTheory.Functor.Initial.lift F d))
(G.map (CategoryTheory.Functor.Initial.homToLift F d))
theorem
CategoryTheory.Functor.Initial.extendCone_obj_π_app'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(c : CategoryTheory.Limits.Cone (F.comp G))
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
:
(CategoryTheory.Functor.Initial.extendCone.obj c).π.app Y = CategoryTheory.CategoryStruct.comp (c.π.app X) (G.map f)
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(s : CategoryTheory.Limits.Cone (F.comp G))
(j : C)
:
CategoryTheory.CategoryStruct.comp (s.π.app (CategoryTheory.Functor.Initial.lift F (F.obj j)))
(G.map (CategoryTheory.Functor.Initial.homToLift F (F.obj j))) = s.π.app j
def
CategoryTheory.Functor.Initial.conesEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.Limits.Cone (F.comp G) ≌ CategoryTheory.Limits.Cone G
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Initial.conesEquiv F G).counitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cone G) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl
(((CategoryTheory.Limits.Cones.whiskering F).comp CategoryTheory.Functor.Initial.extendCone).obj c).pt)
⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_inverse
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_unitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Initial.conesEquiv F G).unitIso = CategoryTheory.NatIso.ofComponents
(fun (c : CategoryTheory.Limits.Cone (F.comp G)) =>
CategoryTheory.Limits.Cones.ext
(CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone (F.comp G))).obj c).pt) ⋯)
⋯
@[simp]
theorem
CategoryTheory.Functor.Initial.conesEquiv_functor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
:
(CategoryTheory.Functor.Initial.conesEquiv F G).functor = CategoryTheory.Functor.Initial.extendCone
def
CategoryTheory.Functor.Initial.isLimitWhiskerEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.Cone (F.comp G))
:
CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.Initial.extendCone.obj t) ≃ CategoryTheory.Limits.IsLimit t
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.LimitCone G)
:
CategoryTheory.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_cone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.LimitCone G)
:
(CategoryTheory.Functor.Initial.limitConeComp F t).cone = CategoryTheory.Limits.Cone.whisker F t.cone
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeComp_isLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.LimitCone G)
:
(CategoryTheory.Functor.Initial.limitConeComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F t.cone).symm t.isLimit
@[instance 100]
instance
CategoryTheory.Functor.Initial.comp_hasLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.Limits.HasLimit G]
:
CategoryTheory.Limits.HasLimit (F.comp G)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.Initial.limit_pre_isIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.Limits.HasLimit G]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Functor.Initial.limitIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasLimit G]
:
CategoryTheory.Limits.limit (F.comp G) ≅ CategoryTheory.Limits.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
Instances For
theorem
CategoryTheory.Functor.Initial.limitIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasLimit G]
:
theorem
CategoryTheory.Functor.Initial.limitIso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.HasLimit G]
:
def
CategoryTheory.Functor.Initial.limIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasLimitsOfShape D E]
[CategoryTheory.Limits.HasLimitsOfShape C E]
:
((CategoryTheory.whiskeringLeft C D E).obj F).comp CategoryTheory.Limits.lim ≅ CategoryTheory.Limits.lim
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.LimitCone (F.comp G))
:
(CategoryTheory.Functor.Initial.limitConeOfComp F t).isLimit = (CategoryTheory.Functor.Initial.isLimitExtendConeEquiv F t.cone).symm t.isLimit
@[simp]
theorem
CategoryTheory.Functor.Initial.limitConeOfComp_cone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
(t : CategoryTheory.Limits.LimitCone (F.comp G))
:
(CategoryTheory.Functor.Initial.limitConeOfComp F t).cone = CategoryTheory.Functor.Initial.extendCone.obj t.cone
theorem
CategoryTheory.Functor.Initial.hasLimit_of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{G : CategoryTheory.Functor D E}
[CategoryTheory.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.hasLimitsOfShape_of_initial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
[CategoryTheory.Limits.HasLimitsOfShape C E]
:
theorem
CategoryTheory.Functor.final_of_comp_full_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Final]
[G.IsEquivalence]
:
(F.comp G).Final
See also the strictly more general final_comp below.
theorem
CategoryTheory.Functor.initial_comp_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Initial]
[G.IsEquivalence]
:
(F.comp G).Initial
See also the strictly more general initial_comp below.
theorem
CategoryTheory.Functor.final_equivalence_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.IsEquivalence]
[G.Final]
:
(F.comp G).Final
See also the strictly more general final_comp below.
theorem
CategoryTheory.Functor.initial_equivalence_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.IsEquivalence]
[G.Initial]
:
(F.comp G).Initial
See also the strictly more general inital_comp below.
theorem
CategoryTheory.Functor.final_of_equivalence_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.IsEquivalence]
:
F.Final ↔ (F.comp G).Final
See also the strictly more general final_iff_comp_final_full_faithful below.
theorem
CategoryTheory.Functor.final_iff_equivalence_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.IsEquivalence]
:
G.Final ↔ (F.comp G).Final
See also the strictly more general final_iff_final_comp below.
theorem
CategoryTheory.Functor.initial_iff_comp_equivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.IsEquivalence]
:
F.Initial ↔ (F.comp G).Initial
See also the strictly more general initial_iff_comp_initial_full_faithful below.
theorem
CategoryTheory.Functor.initial_iff_equivalence_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.IsEquivalence]
:
G.Initial ↔ (F.comp G).Initial
See also the strictly more general initial_iff_initial_comp below.
instance
CategoryTheory.Functor.final_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[hF : F.Final]
[hG : G.Final]
:
(F.comp G).Final
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.initial_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Initial]
[G.Initial]
:
(F.comp G).Initial
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.final_of_final_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[hF : F.Final]
[hFG : (F.comp G).Final]
:
G.Final
theorem
CategoryTheory.Functor.initial_of_initial_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Initial]
[(F.comp G).Initial]
:
G.Initial
theorem
CategoryTheory.Functor.final_of_comp_full_faithful'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.Final]
[G.Full]
[G.Faithful]
:
F.Final ↔ (F.comp G).Final
theorem
CategoryTheory.Functor.initial_iff_comp_initial_full_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.Initial]
[G.Full]
[G.Faithful]
:
F.Initial ↔ (F.comp G).Initial
theorem
CategoryTheory.Functor.final_iff_final_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Final]
:
G.Final ↔ (F.comp G).Final
theorem
CategoryTheory.Functor.initial_iff_initial_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Initial]
:
G.Initial ↔ (F.comp G).Initial
theorem
CategoryTheory.IsFilteredOrEmpty.of_final
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
[CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Final]
[CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
[CategoryTheory.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 intial_of_adjunction.
theorem
CategoryTheory.IsCofiltered.of_initial
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Initial]
[CategoryTheory.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 intial_of_adjunction.
instance
CategoryTheory.StructuredArrow.final_pre
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(T : CategoryTheory.Functor C D)
[T.Final]
(S : CategoryTheory.Functor D E)
(X : E)
:
(CategoryTheory.StructuredArrow.pre X T S).Final
The functor StructuredArrow.pre X T S is final if T is final.
Equations
- ⋯ = ⋯
instance
CategoryTheory.CostructuredArrow.initial_pre
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(T : CategoryTheory.Functor C D)
[T.Initial]
(S : CategoryTheory.Functor D E)
(X : E)
:
(CategoryTheory.CostructuredArrow.pre T S X).Initial
The functor CostructuredArrow.pre X T S is initial if T is initial.
Equations
- ⋯ = ⋯
def
CategoryTheory.Grothendieck.structuredArrowToStructuredArrowPre
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor D CategoryTheory.Cat)
(G : CategoryTheory.Functor C D)
(d : D)
(f : ↑(F.obj d))
:
CategoryTheory.StructuredArrow d G ⥤q CategoryTheory.StructuredArrow { base := d, fiber := f } (CategoryTheory.Grothendieck.pre F G)
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor D CategoryTheory.Cat)
(G : CategoryTheory.Functor C D)
[hG : G.Final]
:
(CategoryTheory.Grothendieck.pre F G).Final
Equations
- ⋯ = ⋯