Preservation and reflection of (co)limits. #
There are various distinct notions of "preserving limits". The one we aim to capture here is: A functor F : C ⥤ D "preserves limits" if it sends every limit cone in C to a limit cone in D. Informally, F preserves all the limits which exist in C.
Note that:
Of course, we do not want to require F to strictly take chosen limit cones of C to chosen limit cones of D. Indeed, the above definition makes no reference to a choice of limit cones so it makes sense without any conditions on C or D.
Some diagrams in C may have no limit. In this case, there is no condition on the behavior of F on such diagrams. There are other notions (such as "flat functor") which impose conditions also on diagrams in C with no limits, but these are not considered here.
In order to be able to express the property of preserving limits of a certain form, we say that a functor F preserves the limit of a diagram K if F sends every limit cone on K to a limit cone. This is vacuously satisfied when K does not admit a limit, which is consistent with the above definition of "preserves limits".
class
CategoryTheory.Limits.PreservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
A functor F preserves limits of K (written as PreservesLimit K F)
if F maps any limit cone over K to a limit cone.
Instances
- CategoryTheory.Functor.Initial.comp_preservesLimit
- CategoryTheory.Functor.corepresentable_preservesLimit
- CategoryTheory.Functor.representable_preservesLimit
- CategoryTheory.Limits.comp_preservesLimit
- CategoryTheory.Limits.evaluation_preservesLimit
- CategoryTheory.coyoneda_preservesLimit
- CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
- CategoryTheory.yoneda_preservesLimit
class
CategoryTheory.Limits.PreservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
A functor F preserves colimits of K (written as PreservesColimit K F)
if F maps any colimit cocone over K to a colimit cocone.
class
CategoryTheory.Limits.PreservesLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
We say that F preserves limits of shape J if F preserves limits for every diagram
K : J ⥤ C, i.e., F maps limit cones over K to limit cones.
- preservesLimit {K : Functor J C} : PreservesLimit K F
Instances
- CategoryTheory.Functor.corepresentable_preservesLimitsOfShape
- CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint
- CategoryTheory.Functor.representable_preservesLimitsOfShape
- CategoryTheory.Limits.comp_preservesLimitsOfShape
- CategoryTheory.Limits.evaluation_preservesLimitsOfShape
- CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts
- CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits
- CategoryTheory.coyonedaPreservesLimitsOfShape
- CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape
- CategoryTheory.yoneda_preservesLimitsOfShape
class
CategoryTheory.Limits.PreservesColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
We say that F preserves colimits of shape J if F preserves colimits for every diagram
K : J ⥤ C, i.e., F maps colimit cocones over K to colimit cocones.
- preservesColimit {K : Functor J C} : PreservesColimit K F
Instances
- CategoryTheory.Functor.Monoidal.instPreservesColimitsOfShapeTensorLeftOfHasColimitsOfShape
- CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint
- CategoryTheory.Limits.comp_preservesColimitsOfShape
- CategoryTheory.Limits.evaluation_preservesColimitsOfShape
- CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts
- CategoryTheory.Limits.preservesColimitsOfShapeOfPreservesFiniteColimits
- CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
class
CategoryTheory.Limits.PreservesLimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
PreservesLimitsOfSize.{v u} F means that F sends all limit cones over any
diagram J ⥤ C to limit cones, where J : Type u with [Category.{v} J].
Instances
- CategoryTheory.Adjunction.isEquivalencePreservesLimits
- CategoryTheory.Adjunction.lim_preservesLimits
- CategoryTheory.Functor.corepresentable_preservesLimits
- CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint
- CategoryTheory.Functor.representable_preservesLimits
- CategoryTheory.Limits.comp_preservesLimits
- CategoryTheory.Limits.evaluationPreservesLimits
- CategoryTheory.Limits.id_preservesLimitsOfSize
- CategoryTheory.Limits.preservesLimits_const
- CategoryTheory.coyonedaFunctor_preservesLimits
- CategoryTheory.coyoneda_preservesLimits
- CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits
- CategoryTheory.yonedaFunctor_preservesLimits
- CategoryTheory.yoneda_preservesLimits
@[reducible, inline]
abbrev
CategoryTheory.Limits.PreservesLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
We say that F preserves (small) limits if it sends small
limit cones over any diagram to limit cones.
class
CategoryTheory.Limits.PreservesColimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
PreservesColimitsOfSize.{v u} F means that F sends all colimit cocones over any
diagram J ⥤ C to colimit cocones, where J : Type u with [Category.{v} J].
Instances
- CategoryTheory.Adjunction.colim_preservesColimits
- CategoryTheory.Adjunction.isEquivalence_preservesColimits
- CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint
- CategoryTheory.Limits.comp_preservesColimits
- CategoryTheory.Limits.evaluation_preservesColimits
- CategoryTheory.Limits.id_preservesColimitsOfSize
- CategoryTheory.Limits.preservesColimits_const
- CategoryTheory.instPreservesColimitsTensorLeft
- CategoryTheory.instPreservesColimitsTensorLeft_1
- CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits
@[reducible, inline]
abbrev
CategoryTheory.Limits.PreservesColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
We say that F preserves (small) limits if it sends small
limit cones over any diagram to limit cones.
def
CategoryTheory.Limits.isLimitOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
(F : Functor C D)
{c : Cone K}
(t : IsLimit c)
[PreservesLimit K F]
:
A convenience function for PreservesLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
def
CategoryTheory.Limits.isColimitOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
(F : Functor C D)
{c : Cocone K}
(t : IsColimit c)
[PreservesColimit K F]
:
A convenience function for PreservesColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
instance
CategoryTheory.Limits.preservesLimit_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
Subsingleton (PreservesLimit K F)
instance
CategoryTheory.Limits.preservesColimit_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
Subsingleton (PreservesColimit K F)
instance
CategoryTheory.Limits.preservesLimitsOfShape_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
instance
CategoryTheory.Limits.preservesColimitsOfShape_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
instance
CategoryTheory.Limits.preservesLimitsOfSize_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
instance
CategoryTheory.Limits.preservesColimitsOfSize_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
@[deprecated "use id_preservesLimitsOfSize" (since := "2024-11-19")]
@[deprecated "use id_preservesColimitsOfSize" (since := "2024-11-19")]
instance
CategoryTheory.Limits.instHasLimitCompOfPreservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
[HasLimit K]
{F : Functor C D}
[PreservesLimit K F]
:
instance
CategoryTheory.Limits.instHasColimitCompOfPreservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
[HasColimit K]
{F : Functor C D}
[PreservesColimit K F]
:
HasColimit (K.comp F)
instance
CategoryTheory.Limits.comp_preservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimit K F]
[PreservesLimit (K.comp F) G]
:
PreservesLimit K (F.comp G)
instance
CategoryTheory.Limits.comp_preservesLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimitsOfShape J F]
[PreservesLimitsOfShape J G]
:
PreservesLimitsOfShape J (F.comp G)
instance
CategoryTheory.Limits.comp_preservesLimits
{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)
[PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[PreservesLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
instance
CategoryTheory.Limits.comp_preservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimit K F]
[PreservesColimit (K.comp F) G]
:
PreservesColimit K (F.comp G)
instance
CategoryTheory.Limits.comp_preservesColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimitsOfShape J F]
[PreservesColimitsOfShape J G]
:
PreservesColimitsOfShape J (F.comp G)
instance
CategoryTheory.Limits.comp_preservesColimits
{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)
[PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[PreservesColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
@[deprecated "use comp_preservesLimit" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimit K F]
[PreservesLimit (K.comp F) G]
:
PreservesLimit K (F.comp G)
@[deprecated "use comp_preservesLimitsOfShape" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimitsOfShape J F]
[PreservesLimitsOfShape J G]
:
PreservesLimitsOfShape J (F.comp G)
@[deprecated "use comp_preservesLimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesLimits
{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)
[PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[PreservesLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
@[deprecated "use comp_preservesColimit" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimit K F]
[PreservesColimit (K.comp F) G]
:
PreservesColimit K (F.comp G)
@[deprecated "use comp_preservesColimitsOfShape" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimitsOfShape J F]
[PreservesColimitsOfShape J G]
:
PreservesColimitsOfShape J (F.comp G)
@[deprecated "use comp_preservesColimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compPreservesColimits
{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)
[PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[PreservesColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
theorem
CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{F : Functor C D}
{t : Cone K}
(h : IsLimit t)
(hF : IsLimit (F.mapCone t))
:
PreservesLimit K F
If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.
@[deprecated "use preservesLimit_of_preserves_limit_cone" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitOfPreservesLimitCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{F : Functor C D}
{t : Cone K}
(h : IsLimit t)
(hF : IsLimit (F.mapCone t))
:
PreservesLimit K F
theorem
CategoryTheory.Limits.preservesLimit_of_iso_diagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[PreservesLimit K₁ F]
:
PreservesLimit K₂ F
Transfer preservation of limits along a natural isomorphism in the diagram.
@[deprecated "use preservesLimit_of_iso_diagram" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitOfIsoDiagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[PreservesLimit K₁ F]
:
PreservesLimit K₂ F
theorem
CategoryTheory.Limits.preservesLimit_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimit K F]
:
PreservesLimit K G
Transfer preservation of a limit along a natural isomorphism in the functor.
@[deprecated "use preservesLimit_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimit K F]
:
PreservesLimit K G
theorem
CategoryTheory.Limits.preservesLimitsOfShape_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimitsOfShape J F]
:
Transfer preservation of limits of shape along a natural isomorphism in the functor.
@[deprecated "use preservesLimitsOfShape_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimitsOfShape J F]
:
theorem
CategoryTheory.Limits.preservesLimits_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer preservation of limits along a natural isomorphism in the functor.
@[deprecated "use preservesLimits_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesLimitsOfShape_of_equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[PreservesLimitsOfShape J F]
:
Transfer preservation of limits along an equivalence in the shape.
@[deprecated "use preservesLimitsOfShape_of_equiv" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[PreservesLimitsOfShape J F]
:
theorem
CategoryTheory.Limits.preservesLimitsOfSize_of_univLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[PreservesLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor preserving larger limits also preserves smaller limits.
@[deprecated "use preservesLimitsOfSize_of_univLE" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[PreservesLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesLimitsOfSize_shrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
PreservesLimitsOfSize_shrink.{w w'} F tries to obtain PreservesLimitsOfSize.{w w'} F
from some other PreservesLimitsOfSize F.
@[deprecated "use preservesLimitsOfSize_shrink" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.PreservesLimitsOfSizeShrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Preserving limits at any universe level implies preserving limits in universe 0.
@[deprecated "use preservesSmallestLimits_of_preservesLimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{F : Functor C D}
{t : Cocone K}
(h : IsColimit t)
(hF : IsColimit (F.mapCocone t))
:
PreservesColimit K F
If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.
@[deprecated "use preservesColimit_of_preserves_colimit_cocone" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{F : Functor C D}
{t : Cocone K}
(h : IsColimit t)
(hF : IsColimit (F.mapCocone t))
:
PreservesColimit K F
theorem
CategoryTheory.Limits.preservesColimit_of_iso_diagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[PreservesColimit K₁ F]
:
PreservesColimit K₂ F
Transfer preservation of colimits along a natural isomorphism in the shape.
@[deprecated "use preservesColimit_of_iso_diagram" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitOfIsoDiagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[PreservesColimit K₁ F]
:
PreservesColimit K₂ F
theorem
CategoryTheory.Limits.preservesColimit_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimit K F]
:
PreservesColimit K G
Transfer preservation of a colimit along a natural isomorphism in the functor.
@[deprecated CategoryTheory.Limits.preservesColimit_of_natIso (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimit K F]
:
PreservesColimit K G
theorem
CategoryTheory.Limits.preservesColimitsOfShape_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimitsOfShape J F]
:
Transfer preservation of colimits of shape along a natural isomorphism in the functor.
@[deprecated "use preservesColimitsOfShape_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimitsOfShape J F]
:
theorem
CategoryTheory.Limits.preservesColimits_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer preservation of colimits along a natural isomorphism in the functor.
@[deprecated "use preservesColimits_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesColimitsOfShape_of_equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[PreservesColimitsOfShape J F]
:
Transfer preservation of colimits along an equivalence in the shape.
@[deprecated "use preservesColimitsOfShape_of_equiv" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[PreservesColimitsOfShape J F]
:
theorem
CategoryTheory.Limits.preservesColimitsOfSize_of_univLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[PreservesColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor preserving larger colimits also preserves smaller colimits.
@[deprecated "use preservesColimitsOfSize_of_univLE" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[PreservesColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesColimitsOfSize_shrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
PreservesColimitsOfSize_shrink.{w w'} F tries to obtain PreservesColimitsOfSize.{w w'} F
from some other PreservesColimitsOfSize F.
@[deprecated "use preservesColimitsOfSize_shrink" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.PreservesColimitsOfSizeShrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.preservesSmallestColimits_of_preservesColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Preserving colimits at any universe implies preserving colimits at universe 0.
@[deprecated "use preservesSmallestColimits_of_preservesColimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
class
CategoryTheory.Limits.ReflectsLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
A functor F : C ⥤ D reflects limits for K : J ⥤ C if
whenever the image of a cone over K under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
class
CategoryTheory.Limits.ReflectsColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
A functor F : C ⥤ D reflects colimits for K : J ⥤ C if
whenever the image of a cocone over K under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
class
CategoryTheory.Limits.ReflectsLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
A functor F : C ⥤ D reflects limits of shape J if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
- reflectsLimit {K : Functor J C} : ReflectsLimit K F
class
CategoryTheory.Limits.ReflectsColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
A functor F : C ⥤ D reflects colimits of shape J if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
- reflectsColimit {K : Functor J C} : ReflectsColimit K F
class
CategoryTheory.Limits.ReflectsLimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D reflects limits if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
Instances
- CategoryTheory.Functor.reflectsLimits_of_isEquivalence
- CategoryTheory.Limits.comp_reflectsLimits
- CategoryTheory.Limits.fullyFaithful_reflectsLimits
- CategoryTheory.Limits.id_reflectsLimits
- CategoryTheory.coyonedaFunctor_reflectsLimits
- CategoryTheory.reflectsLimitsOfCreatesLimits
- CategoryTheory.yonedaFunctor_reflectsLimits
@[reducible, inline]
abbrev
CategoryTheory.Limits.ReflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D reflects (small) limits if
whenever the image of a cone over some K : J ⥤ C under F is a limit cone in D,
the cone was already a limit cone in C.
Note that we do not assume a priori that D actually has any limits.
class
CategoryTheory.Limits.ReflectsColimitsOfSize
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D reflects colimits if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
@[reducible, inline]
abbrev
CategoryTheory.Limits.ReflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor F : C ⥤ D reflects (small) colimits if
whenever the image of a cocone over some K : J ⥤ C under F is a colimit cocone in D,
the cocone was already a colimit cocone in C.
Note that we do not assume a priori that D actually has any colimits.
def
CategoryTheory.Limits.isLimitOfReflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
(F : Functor C D)
{c : Cone K}
(t : IsLimit (F.mapCone c))
[ReflectsLimit K F]
:
IsLimit c
A convenience function for ReflectsLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
def
CategoryTheory.Limits.isColimitOfReflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
(F : Functor C D)
{c : Cocone K}
(t : IsColimit (F.mapCocone c))
[ReflectsColimit K F]
:
A convenience function for ReflectsColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
Equations
instance
CategoryTheory.Limits.reflectsLimit_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
Subsingleton (ReflectsLimit K F)
instance
CategoryTheory.Limits.reflectsColimit_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
:
Subsingleton (ReflectsColimit K F)
instance
CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
instance
CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
:
instance
CategoryTheory.Limits.reflects_limits_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
instance
CategoryTheory.Limits.reflects_colimits_subsingleton
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
@[instance 100]
instance
CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
[ReflectsLimitsOfShape J F]
:
ReflectsLimit K F
@[instance 100]
instance
CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
(F : Functor C D)
[ReflectsColimitsOfShape J F]
:
ReflectsColimit K F
@[instance 100]
instance
CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
[ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
@[instance 100]
instance
CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(J : Type w)
[Category.{w', w} J]
(F : Functor C D)
[ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
@[deprecated "use id_reflectsLimits" (since := "2024-11-19")]
@[deprecated "use id_reflectsColimits" (since := "2024-11-19")]
instance
CategoryTheory.Limits.comp_reflectsLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsLimit K F]
[ReflectsLimit (K.comp F) G]
:
ReflectsLimit K (F.comp G)
instance
CategoryTheory.Limits.comp_reflectsLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsLimitsOfShape J F]
[ReflectsLimitsOfShape J G]
:
ReflectsLimitsOfShape J (F.comp G)
instance
CategoryTheory.Limits.comp_reflectsLimits
{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)
[ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
instance
CategoryTheory.Limits.comp_reflectsColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsColimit K F]
[ReflectsColimit (K.comp F) G]
:
ReflectsColimit K (F.comp G)
instance
CategoryTheory.Limits.comp_reflectsColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsColimitsOfShape J F]
[ReflectsColimitsOfShape J G]
:
ReflectsColimitsOfShape J (F.comp G)
instance
CategoryTheory.Limits.comp_reflectsColimits
{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)
[ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
@[deprecated "use comp_reflectsLimit" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsLimit K F]
[ReflectsLimit (K.comp F) G]
:
ReflectsLimit K (F.comp G)
@[deprecated "use comp_reflectsLimitsOfShape " (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsLimitsOfShape J F]
[ReflectsLimitsOfShape J G]
:
ReflectsLimitsOfShape J (F.comp G)
@[deprecated "use comp_reflectsLimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsLimits
{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)
[ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
@[deprecated "use comp_reflectsColimit" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsColimit K F]
[ReflectsColimit (K.comp F) G]
:
ReflectsColimit K (F.comp G)
@[deprecated "use comp_reflectsColimitsOfShape " (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[ReflectsColimitsOfShape J F]
[ReflectsColimitsOfShape J G]
:
ReflectsColimitsOfShape J (F.comp G)
@[deprecated "use comp_reflectsColimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.compReflectsColimits
{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)
[ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
theorem
CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimit K (F.comp G)]
[ReflectsLimit (K.comp F) G]
:
PreservesLimit K F
If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F,
then F preserves limits for K.
@[deprecated "use preservesLimit_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimit K (F.comp G)]
[ReflectsLimit (K.comp F) G]
:
PreservesLimit K F
theorem
CategoryTheory.Limits.preservesLimitsOfShape_of_reflects_of_preserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimitsOfShape J (F.comp G)]
[ReflectsLimitsOfShape J G]
:
If F ⋙ G preserves limits of shape J and G reflects limits of shape J, then F preserves
limits of shape J.
@[deprecated "use preservesLimitsOfShape_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesLimitsOfShape J (F.comp G)]
[ReflectsLimitsOfShape J G]
:
theorem
CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves
{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)
[PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
If F ⋙ G preserves limits and G reflects limits, then F preserves limits.
@[deprecated "use preservesLimits_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves
{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)
[PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
theorem
CategoryTheory.Limits.reflectsLimit_of_iso_diagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[ReflectsLimit K₁ F]
:
ReflectsLimit K₂ F
Transfer reflection of limits along a natural isomorphism in the diagram.
@[deprecated "use reflectsLimit_of_iso_diagram" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitOfIsoDiagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[ReflectsLimit K₁ F]
:
ReflectsLimit K₂ F
theorem
CategoryTheory.Limits.reflectsLimit_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimit K F]
:
ReflectsLimit K G
Transfer reflection of a limit along a natural isomorphism in the functor.
@[deprecated "use reflectsLimit_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimit K F]
:
ReflectsLimit K G
theorem
CategoryTheory.Limits.reflectsLimitsOfShape_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimitsOfShape J F]
:
Transfer reflection of limits of shape along a natural isomorphism in the functor.
@[deprecated "use reflectsLimitsOfShape_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimitsOfShape J F]
:
theorem
CategoryTheory.Limits.reflectsLimits_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
Transfer reflection of limits along a natural isomorphism in the functor.
@[deprecated "use reflectsLimits_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsLimitsOfShape_of_equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[ReflectsLimitsOfShape J F]
:
Transfer reflection of limits along an equivalence in the shape.
@[deprecated "use reflectsLimitsOfShape_of_equiv" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[ReflectsLimitsOfShape J F]
:
theorem
CategoryTheory.Limits.reflectsLimitsOfSize_of_univLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[ReflectsLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor reflecting larger limits also reflects smaller limits.
@[deprecated "use reflectsLimitsOfSize_of_univLE" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[ReflectsLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsLimitsOfSize_shrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
reflectsLimitsOfSize_shrink.{w w'} F tries to obtain reflectsLimitsOfSize.{w w'} F
from some other reflectsLimitsOfSize F.
@[deprecated "use reflectsLimitsOfSize_shrink" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfSizeShrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsSmallestLimits_of_reflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Reflecting limits at any universe implies reflecting limits at universe 0.
@[deprecated "use reflectsSmallestLimits_of_reflectsLimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsLimit_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
(G : Functor C D)
[G.ReflectsIsomorphisms]
[HasLimit F]
[PreservesLimit F G]
:
ReflectsLimit F G
If the limit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the limit of F.
@[deprecated "use reflectsLimit_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
(G : Functor C D)
[G.ReflectsIsomorphisms]
[HasLimit F]
[PreservesLimit F G]
:
ReflectsLimit F G
theorem
CategoryTheory.Limits.reflectsLimitsOfShape_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasLimitsOfShape J C]
[PreservesLimitsOfShape J G]
:
If C has limits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects limits of shape J.
@[deprecated "use reflectsLimitsOfShape_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasLimitsOfShape J C]
[PreservesLimitsOfShape J G]
:
theorem
CategoryTheory.Limits.reflectsLimits_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasLimitsOfSize.{w', w, v₁, u₁} C]
[PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G]
:
If C has limits and G preserves limits, then if G reflects isomorphisms then it reflects
limits.
@[deprecated "use reflectsLimits_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasLimitsOfSize.{w', w, v₁, u₁} C]
[PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G]
:
theorem
CategoryTheory.Limits.preservesColimit_of_reflects_of_preserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimit K (F.comp G)]
[ReflectsColimit (K.comp F) G]
:
PreservesColimit K F
If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F,
then F preserves colimits for K.
@[deprecated "use preservesColimit_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K : Functor J C}
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimit K (F.comp G)]
[ReflectsColimit (K.comp F) G]
:
PreservesColimit K F
theorem
CategoryTheory.Limits.preservesColimitsOfShape_of_reflects_of_preserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimitsOfShape J (F.comp G)]
[ReflectsColimitsOfShape J G]
:
If F ⋙ G preserves colimits of shape J and G reflects colimits of shape J, then F
preserves colimits of shape J.
@[deprecated "use preservesColimitsOfShape_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{E : Type u₃}
[ℰ : Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[PreservesColimitsOfShape J (F.comp G)]
[ReflectsColimitsOfShape J G]
:
theorem
CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves
{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)
[PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
If F ⋙ G preserves colimits and G reflects colimits, then F preserves colimits.
@[deprecated "use preservesColimits_of_reflects_of_preserves" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves
{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)
[PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
theorem
CategoryTheory.Limits.reflectsColimit_of_iso_diagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[ReflectsColimit K₁ F]
:
ReflectsColimit K₂ F
Transfer reflection of colimits along a natural isomorphism in the diagram.
@[deprecated "use reflectsColimit_of_iso_diagram" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitOfIsoDiagram
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{K₁ K₂ : Functor J C}
(F : Functor C D)
(h : K₁ ≅ K₂)
[ReflectsColimit K₁ F]
:
ReflectsColimit K₂ F
theorem
CategoryTheory.Limits.reflectsColimit_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimit K F]
:
ReflectsColimit K G
Transfer reflection of a colimit along a natural isomorphism in the functor.
@[deprecated "use reflectsColimit_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(K : Functor J C)
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimit K F]
:
ReflectsColimit K G
theorem
CategoryTheory.Limits.reflectsColimitsOfShape_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimitsOfShape J F]
:
Transfer reflection of colimits of shape along a natural isomorphism in the functor.
@[deprecated "use reflectsColimitsOfShape_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimitsOfShape J F]
:
theorem
CategoryTheory.Limits.reflectsColimits_of_natIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer reflection of colimits along a natural isomorphism in the functor.
@[deprecated "use reflectsColimits_of_natIso" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfNatIso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(h : F ≅ G)
[ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsColimitsOfShape_of_equiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[ReflectsColimitsOfShape J F]
:
Transfer reflection of colimits along an equivalence in the shape.
@[deprecated "use reflectsColimitsOfShape_of_equiv" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{J' : Type w₂}
[Category.{w₂', w₂} J']
(e : J ≌ J')
(F : Functor C D)
[ReflectsColimitsOfShape J F]
:
theorem
CategoryTheory.Limits.reflectsColimitsOfSize_of_univLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[ReflectsColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor reflecting larger colimits also reflects smaller colimits.
@[deprecated "use reflectsColimitsOfSize_of_univLE" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[UnivLE.{w, w'}]
[UnivLE.{w₂, w₂'}]
[ReflectsColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsColimitsOfSize_shrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
reflectsColimitsOfSize_shrink.{w w'} F tries to obtain reflectsColimitsOfSize.{w w'} F
from some other reflectsColimitsOfSize F.
@[deprecated "use reflectsColimitsOfSize_shrink" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfSizeShrink
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsSmallestColimits_of_reflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Reflecting colimits at any universe implies reflecting colimits at universe 0.
@[deprecated "use reflectsSmallestColimits_of_reflectsColimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
theorem
CategoryTheory.Limits.reflectsColimit_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
(G : Functor C D)
[G.ReflectsIsomorphisms]
[HasColimit F]
[PreservesColimit F G]
:
ReflectsColimit F G
If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the colimit of F.
@[deprecated "use reflectsColimit_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
(F : Functor J C)
(G : Functor C D)
[G.ReflectsIsomorphisms]
[HasColimit F]
[PreservesColimit F G]
:
ReflectsColimit F G
theorem
CategoryTheory.Limits.reflectsColimitsOfShape_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasColimitsOfShape J C]
[PreservesColimitsOfShape J G]
:
If C has colimits of shape J and G preserves them, then if G reflects isomorphisms then it
reflects colimits of shape J.
@[deprecated "use reflectsColimitsOfShape_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasColimitsOfShape J C]
[PreservesColimitsOfShape J G]
:
theorem
CategoryTheory.Limits.reflectsColimits_of_reflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasColimitsOfSize.{w', w, v₁, u₁} C]
[PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G]
:
If C has colimits and G preserves colimits, then if G reflects isomorphisms then it reflects
colimits.
@[deprecated "use reflectsColimits_of_reflectsIsomorphisms" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{G : Functor C D}
[G.ReflectsIsomorphisms]
[HasColimitsOfSize.{w', w, v₁, u₁} C]
[PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} G]
:
instance
CategoryTheory.Limits.fullyFaithful_reflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Full]
[F.Faithful]
:
A fully faithful functor reflects limits.
@[deprecated "use fullyFaithful_reflectsLimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.fullyFaithfulReflectsLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Full]
[F.Faithful]
:
instance
CategoryTheory.Limits.fullyFaithful_reflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Full]
[F.Faithful]
:
A fully faithful functor reflects colimits.
@[deprecated "use fullyFaithful_reflectsColimits" (since := "2024-11-19")]
theorem
CategoryTheory.Limits.fullyFaithfulReflectsColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Full]
[F.Faithful]
: