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₁}
[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.
See https://stacks.math.columbia.edu/tag/04E6
- 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]
:
F.op.Final
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]
:
F.op.Initial
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')
:
F.Final ↔ F'.Final
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')
:
F.Initial ↔ F'.Initial
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
- CategoryTheory.Functor.Final.lift F d = (Classical.arbitrary (CategoryTheory.StructuredArrow d F)).right
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))
:
(extendCocone.obj c).pt = c.pt
@[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)
:
(extendCocone.obj c).ι.app X = CategoryStruct.comp (G.map (homToLift F X)) (c.ι.app (lift F X))
@[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✝)
:
(extendCocone.map f).hom = f.hom
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)
:
(extendCocone.obj c).ι.app X = 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₁}
[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)
:
CategoryStruct.comp (G.map (homToLift F (F.obj j))) (s.ι.app (lift F (F.obj j))) = s.ι.app j
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)
:
Limits.Cocone (F.comp G) ≌ 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₁}
[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).inverse = Limits.Cocones.whiskering F
@[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)
:
(coconesEquiv F G).functor = extendCocone
@[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))
:
Limits.IsColimit (extendCocone.obj t) ≃ 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₁}
[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)
:
(colimitCoconeComp F t).cocone = Limits.Cocone.whisker F t.cocone
@[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)
:
(colimitCoconeComp F t).isColimit = (isColimitWhiskerEquiv F t.cocone).symm t.isColimit
@[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]
:
Limits.colimit (F.comp G) ≅ 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₁}
[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]
:
(colimitIso F G).inv = CategoryTheory.inv (Limits.colimit.pre G F)
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]
:
(colimitIso F G).hom = Limits.colimit.pre G F
@[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]
:
((whiskeringLeft C D E).obj F).comp Limits.colim ≅ 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₁}
[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))
:
(colimitCoconeOfComp F t).isColimit = (isColimitExtendCoconeEquiv F t.cocone).symm t.isColimit
@[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))
:
(colimitCoconeOfComp F t).cocone = extendCocone.obj t.cocone
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_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 (Limits.Types.Quot.Rel (F.comp (coyoneda.obj (Opposite.op d)))) f₁ f₂)
:
Zigzag (StructuredArrow.mk f₁.snd) (StructuredArrow.mk f₂.snd)
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)]
:
Limits.colimit (F.comp (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}
[Category.{v, v} C]
{D : Type v}
[Category.{v, v} D]
(F : Functor C D)
:
F.Final ↔ ∀ (G : Functor D (Type v)), IsIso (Limits.colimit.pre G F)
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_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✝)
:
(extendCone.map f).hom = f.hom
@[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))
:
(extendCone.obj c).pt = c.pt
@[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)
:
(extendCone.obj c).π.app d = CategoryStruct.comp (c.π.app (lift F d)) (G.map (homToLift F d))
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)
:
(extendCone.obj c).π.app Y = 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₁}
[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)
:
CategoryStruct.comp (s.π.app (lift F (F.obj j))) (G.map (homToLift F (F.obj j))) = s.π.app j
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)
:
Limits.Cone (F.comp G) ≌ 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₁}
[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_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)
:
(conesEquiv F G).inverse = Limits.Cones.whiskering F
@[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)
:
(conesEquiv F G).functor = extendCone
@[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) ⋯)
⋯
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))
:
Limits.IsLimit (extendCone.obj t) ≃ 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₁}
[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_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)
:
(limitConeComp F t).cone = Limits.Cone.whisker F t.cone
@[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)
:
(limitConeComp F t).isLimit = (isLimitWhiskerEquiv F t.cone).symm t.isLimit
@[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]
:
Limits.limit (F.comp G) ≅ 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₁}
[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]
:
(limitIso F G).hom = CategoryTheory.inv (Limits.limit.pre G F)
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]
:
(limitIso F G).inv = Limits.limit.pre G F
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]
:
((whiskeringLeft C D E).obj F).comp Limits.lim ≅ 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₁}
[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))
:
(limitConeOfComp F t).isLimit = (isLimitExtendConeEquiv F t.cone).symm t.isLimit
@[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))
:
(limitConeOfComp F t).cone = extendCone.obj t.cone
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]
:
(F.comp G).Final
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]
:
(F.comp G).Initial
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]
:
(F.comp 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]
:
(F.comp 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]
:
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₁}
[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 ↔ (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₁}
[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]
:
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₁}
[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 ↔ (F.comp G).Initial
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]
:
(F.comp 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]
:
(F.comp 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]
:
F.Final ↔ (F.comp G).Final
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]
:
F.Initial ↔ (F.comp G).Initial
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]
:
G.Final ↔ (F.comp G).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]
:
G.Initial ↔ (F.comp G).Initial
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)
:
(pre X T S).Final
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)
:
(pre T S X).Initial
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))
:
StructuredArrow d G ⥤q StructuredArrow { base := d, fiber := f } (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₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor D Cat)
(G : Functor C D)
[hG : G.Final]
:
(pre F G).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]
:
(F.prod G).Final