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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) w)
A functor F preserves limits of K (written as PreservesLimit K F)
if F maps any limit cone over K to a limit cone.
- preserves : {c : CategoryTheory.Limits.Cone K} → CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (F.mapCone c)
Instances
class
CategoryTheory.Limits.PreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) w)
A functor F preserves colimits of K (written as PreservesColimit K F)
if F maps any colimit cocone over K to a colimit cocone.
- preserves : {c : CategoryTheory.Limits.Cocone K} → CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (F.mapCocone c)
Instances
class
CategoryTheory.Limits.PreservesLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
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 : CategoryTheory.Functor J C} → CategoryTheory.Limits.PreservesLimit K F
Instances
class
CategoryTheory.Limits.PreservesColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
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 : CategoryTheory.Functor J C} → CategoryTheory.Limits.PreservesColimit K F
Instances
class
CategoryTheory.Limits.PreservesLimitsOfSize
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
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].
- preservesLimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.PreservesLimitsOfShape J F
Instances
@[reducible, inline]
abbrev
CategoryTheory.Limits.PreservesLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
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].
- preservesColimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.PreservesColimitsOfShape J F
Instances
@[reducible, inline]
abbrev
CategoryTheory.Limits.PreservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
{c : CategoryTheory.Limits.Cone K}
(t : CategoryTheory.Limits.IsLimit c)
[CategoryTheory.Limits.PreservesLimit K F]
:
CategoryTheory.Limits.IsLimit (F.mapCone c)
A convenience function for PreservesLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
def
CategoryTheory.Limits.isColimitOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
{c : CategoryTheory.Limits.Cocone K}
(t : CategoryTheory.Limits.IsColimit c)
[CategoryTheory.Limits.PreservesColimit K F]
:
CategoryTheory.Limits.IsColimit (F.mapCocone c)
A convenience function for PreservesColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
instance
CategoryTheory.Limits.preservesLimit_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.preservesColimit_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.preservesLimitsOfShape_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.preservesColimitsOfShape_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.preserves_limits_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.preserves_colimits_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.idPreservesLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.idPreservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.instHasLimitCompOfPreservesLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
[CategoryTheory.Limits.HasLimit K]
{F : CategoryTheory.Functor C D}
[CategoryTheory.Limits.PreservesLimit K F]
:
CategoryTheory.Limits.HasLimit (K.comp F)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasColimitCompOfPreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
[CategoryTheory.Limits.HasColimit K]
{F : CategoryTheory.Functor C D}
[CategoryTheory.Limits.PreservesColimit K F]
:
CategoryTheory.Limits.HasColimit (K.comp F)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.compPreservesLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimit K F]
[CategoryTheory.Limits.PreservesLimit (K.comp F) G]
:
CategoryTheory.Limits.PreservesLimit K (F.comp G)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.compPreservesLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
[CategoryTheory.Limits.PreservesLimitsOfShape J G]
:
CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp G)
Equations
- CategoryTheory.Limits.compPreservesLimitsOfShape F G = { preservesLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
instance
CategoryTheory.Limits.compPreservesLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
Equations
- CategoryTheory.Limits.compPreservesLimits F G = { preservesLimitsOfShape := fun {J : Type ?u.79} [CategoryTheory.Category.{?u.80, ?u.79} J] => inferInstance }
instance
CategoryTheory.Limits.compPreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimit K F]
[CategoryTheory.Limits.PreservesColimit (K.comp F) G]
:
CategoryTheory.Limits.PreservesColimit K (F.comp G)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.compPreservesColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
[CategoryTheory.Limits.PreservesColimitsOfShape J G]
:
CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp G)
Equations
- CategoryTheory.Limits.compPreservesColimitsOfShape F G = { preservesColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
instance
CategoryTheory.Limits.compPreservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
Equations
- CategoryTheory.Limits.compPreservesColimits F G = { preservesColimitsOfShape := fun {J : Type ?u.79} [CategoryTheory.Category.{?u.80, ?u.79} J] => inferInstance }
def
CategoryTheory.Limits.preservesLimitOfPreservesLimitCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{F : CategoryTheory.Functor C D}
{t : CategoryTheory.Limits.Cone K}
(h : CategoryTheory.Limits.IsLimit t)
(hF : CategoryTheory.Limits.IsLimit (F.mapCone t))
:
If F preserves one limit cone for the diagram K, then it preserves any limit cone for K.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitOfIsoDiagram
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K₁ : CategoryTheory.Functor J C}
{K₂ : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
(h : K₁ ≅ K₂)
[CategoryTheory.Limits.PreservesLimit K₁ F]
:
Transfer preservation of limits along a natural isomorphism in the diagram.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesLimit K F]
:
Transfer preservation of a limit along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
:
Transfer preservation of limits of shape along a natural isomorphism in the functor.
Equations
- CategoryTheory.Limits.preservesLimitsOfShapeOfNatIso h = { preservesLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesLimitOfNatIso K h }
def
CategoryTheory.Limits.preservesLimitsOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer preservation of limits along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{J' : Type w₂}
[CategoryTheory.Category.{w₂', w₂} J']
(e : J ≌ J')
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfShape J F]
:
Transfer preservation of limits along an equivalence in the shape.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfSizeOfUnivLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[UnivLE.{w, w'} ]
[UnivLE.{w₂, w₂'} ]
[CategoryTheory.Limits.PreservesLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor preserving larger limits also preserves smaller limits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfSizeShrink
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
PreservesLimitsOfSizeShrink.{w w'} F tries to obtain PreservesLimitsOfSize.{w w'} F
from some other PreservesLimitsOfSize F.
def
CategoryTheory.Limits.preservesSmallestLimitsOfPreservesLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Preserving limits at any universe level implies preserving limits in universe 0.
def
CategoryTheory.Limits.preservesColimitOfPreservesColimitCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{F : CategoryTheory.Functor C D}
{t : CategoryTheory.Limits.Cocone K}
(h : CategoryTheory.Limits.IsColimit t)
(hF : CategoryTheory.Limits.IsColimit (F.mapCocone t))
:
If F preserves one colimit cocone for the diagram K, then it preserves any colimit cocone for K.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitOfIsoDiagram
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K₁ : CategoryTheory.Functor J C}
{K₂ : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
(h : K₁ ≅ K₂)
[CategoryTheory.Limits.PreservesColimit K₁ F]
:
Transfer preservation of colimits along a natural isomorphism in the shape.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesColimit K F]
:
Transfer preservation of a colimit along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
:
Transfer preservation of colimits of shape along a natural isomorphism in the functor.
Equations
- CategoryTheory.Limits.preservesColimitsOfShapeOfNatIso h = { preservesColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.preservesColimitOfNatIso K h }
def
CategoryTheory.Limits.preservesColimitsOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer preservation of colimits along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{J' : Type w₂}
[CategoryTheory.Category.{w₂', w₂} J']
(e : J ≌ J')
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimitsOfShape J F]
:
Transfer preservation of colimits along an equivalence in the shape.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfSizeOfUnivLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[UnivLE.{w, w'} ]
[UnivLE.{w₂, w₂'} ]
[CategoryTheory.Limits.PreservesColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor preserving larger colimits also preserves smaller colimits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfSizeShrink
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
PreservesColimitsOfSizeShrink.{w w'} F tries to obtain PreservesColimitsOfSize.{w w'} F
from some other PreservesColimitsOfSize F.
def
CategoryTheory.Limits.preservesSmallestColimitsOfPreservesColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Preserving colimits at any universe implies preserving colimits at universe 0.
class
CategoryTheory.Limits.ReflectsLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) w)
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.
- reflects : {c : CategoryTheory.Limits.Cone K} → CategoryTheory.Limits.IsLimit (F.mapCone c) → CategoryTheory.Limits.IsLimit c
Instances
class
CategoryTheory.Limits.ReflectsColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) w)
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.
- reflects : {c : CategoryTheory.Limits.Cocone K} → CategoryTheory.Limits.IsColimit (F.mapCocone c) → CategoryTheory.Limits.IsColimit c
Instances
class
CategoryTheory.Limits.ReflectsLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
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 : CategoryTheory.Functor J C} → CategoryTheory.Limits.ReflectsLimit K F
Instances
class
CategoryTheory.Limits.ReflectsColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
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 : CategoryTheory.Functor J C} → CategoryTheory.Limits.ReflectsColimit K F
Instances
class
CategoryTheory.Limits.ReflectsLimitsOfSize
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
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.
- reflectsLimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.ReflectsLimitsOfShape J F
Instances
@[reducible, inline]
abbrev
CategoryTheory.Limits.ReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max (max u₁ u₂) v₁) v₂) (w + 1)) (w' + 1))
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.
- reflectsColimitsOfShape : {J : Type w} → [inst : CategoryTheory.Category.{w', w} J] → CategoryTheory.Limits.ReflectsColimitsOfShape J F
Instances
@[reducible, inline]
abbrev
CategoryTheory.Limits.ReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
{c : CategoryTheory.Limits.Cone K}
(t : CategoryTheory.Limits.IsLimit (F.mapCone c))
[CategoryTheory.Limits.ReflectsLimit K F]
:
A convenience function for ReflectsLimit, which takes the functor as an explicit argument to
guide typeclass resolution.
def
CategoryTheory.Limits.isColimitOfReflects
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
{c : CategoryTheory.Limits.Cocone K}
(t : CategoryTheory.Limits.IsColimit (F.mapCocone c))
[CategoryTheory.Limits.ReflectsColimit K F]
:
A convenience function for ReflectsColimit, which takes the functor as an explicit argument to
guide typeclass resolution.
instance
CategoryTheory.Limits.reflectsLimit_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.reflectsColimit_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.reflectsLimitsOfShape_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.reflectsColimitsOfShape_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.reflects_limits_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.reflects_colimits_subsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Equations
- ⋯ = ⋯
@[instance 100]
instance
CategoryTheory.Limits.reflectsLimitOfReflectsLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimitsOfShape J F]
:
Equations
- CategoryTheory.Limits.reflectsLimitOfReflectsLimitsOfShape K F = CategoryTheory.Limits.ReflectsLimitsOfShape.reflectsLimit
@[instance 100]
instance
CategoryTheory.Limits.reflectsColimitOfReflectsColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimitsOfShape J F]
:
Equations
- CategoryTheory.Limits.reflectsColimitOfReflectsColimitsOfShape K F = CategoryTheory.Limits.ReflectsColimitsOfShape.reflectsColimit
@[instance 100]
instance
CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
Equations
- CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsLimits J F = CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsLimitsOfShape
@[instance 100]
instance
CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(J : Type w)
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
Equations
- CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsColimits J F = CategoryTheory.Limits.ReflectsColimitsOfSize.reflectsColimitsOfShape
instance
CategoryTheory.Limits.idReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.idReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.compReflectsLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsLimit K F]
[CategoryTheory.Limits.ReflectsLimit (K.comp F) G]
:
CategoryTheory.Limits.ReflectsLimit K (F.comp G)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.compReflectsLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsLimitsOfShape J F]
[CategoryTheory.Limits.ReflectsLimitsOfShape J G]
:
CategoryTheory.Limits.ReflectsLimitsOfShape J (F.comp G)
Equations
- CategoryTheory.Limits.compReflectsLimitsOfShape F G = { reflectsLimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
instance
CategoryTheory.Limits.compReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
Equations
- CategoryTheory.Limits.compReflectsLimits F G = { reflectsLimitsOfShape := fun {J : Type ?u.79} [CategoryTheory.Category.{?u.80, ?u.79} J] => inferInstance }
instance
CategoryTheory.Limits.compReflectsColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsColimit K F]
[CategoryTheory.Limits.ReflectsColimit (K.comp F) G]
:
CategoryTheory.Limits.ReflectsColimit K (F.comp G)
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.compReflectsColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsColimitsOfShape J F]
[CategoryTheory.Limits.ReflectsColimitsOfShape J G]
:
CategoryTheory.Limits.ReflectsColimitsOfShape J (F.comp G)
Equations
- CategoryTheory.Limits.compReflectsColimitsOfShape F G = { reflectsColimit := fun {K : CategoryTheory.Functor J C} => inferInstance }
instance
CategoryTheory.Limits.compReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
Equations
- CategoryTheory.Limits.compReflectsColimits F G = { reflectsColimitsOfShape := fun {J : Type ?u.79} [CategoryTheory.Category.{?u.80, ?u.79} J] => inferInstance }
def
CategoryTheory.Limits.preservesLimitOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimit K (F.comp G)]
[CategoryTheory.Limits.ReflectsLimit (K.comp F) G]
:
If F ⋙ G preserves limits for K, and G reflects limits for K ⋙ F,
then F preserves limits for K.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfShapeOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfShape J (F.comp G)]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesLimitsOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
If F ⋙ G preserves limits and G reflects limits, then F preserves limits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitOfIsoDiagram
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K₁ : CategoryTheory.Functor J C}
{K₂ : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
(h : K₁ ≅ K₂)
[CategoryTheory.Limits.ReflectsLimit K₁ F]
:
Transfer reflection of limits along a natural isomorphism in the diagram.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsLimit K F]
:
Transfer reflection of a limit along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsLimitsOfShape J F]
:
Transfer reflection of limits of shape along a natural isomorphism in the functor.
Equations
- CategoryTheory.Limits.reflectsLimitsOfShapeOfNatIso h = { reflectsLimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.reflectsLimitOfNatIso K h }
def
CategoryTheory.Limits.reflectsLimitsOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
Transfer reflection of limits along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfShapeOfEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{J' : Type w₂}
[CategoryTheory.Category.{w₂', w₂} J']
(e : J ≌ J')
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimitsOfShape J F]
:
Transfer reflection of limits along an equivalence in the shape.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfSizeOfUnivLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[UnivLE.{w, w'} ]
[UnivLE.{w₂, w₂'} ]
[CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor reflecting larger limits also reflects smaller limits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfSizeShrink
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
reflectsLimitsOfSizeShrink.{w w'} F tries to obtain reflectsLimitsOfSize.{w w'} F
from some other reflectsLimitsOfSize F.
def
CategoryTheory.Limits.reflectsSmallestLimitsOfReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Reflecting limits at any universe implies reflecting limits at universe 0.
def
CategoryTheory.Limits.reflectsLimitOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasLimit F]
[CategoryTheory.Limits.PreservesLimit F G]
:
If the limit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the limit of F.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfShapeOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{G : CategoryTheory.Functor C D}
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasLimitsOfShape J C]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsLimitsOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor C D}
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasLimitsOfSize.{w', w, v₁, u₁} C]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K : CategoryTheory.Functor J C}
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimit K (F.comp G)]
[CategoryTheory.Limits.ReflectsColimit (K.comp F) G]
:
If F ⋙ G preserves colimits for K, and G reflects colimits for K ⋙ F,
then F preserves colimits for K.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfShapeOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfShape J (F.comp G)]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.preservesColimitsOfReflectsOfPreserves
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[ℰ : CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₃, u₁, u₃} (F.comp G)]
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w, v₂, v₃, u₂, u₃} G]
:
If F ⋙ G preserves colimits and G reflects colimits, then F preserves colimits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitOfIsoDiagram
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{K₁ : CategoryTheory.Functor J C}
{K₂ : CategoryTheory.Functor J C}
(F : CategoryTheory.Functor C D)
(h : K₁ ≅ K₂)
[CategoryTheory.Limits.ReflectsColimit K₁ F]
:
Transfer reflection of colimits along a natural isomorphism in the diagram.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(K : CategoryTheory.Functor J C)
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsColimit K F]
:
Transfer reflection of a colimit along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsColimitsOfShape J F]
:
Transfer reflection of colimits of shape along a natural isomorphism in the functor.
Equations
- CategoryTheory.Limits.reflectsColimitsOfShapeOfNatIso h = { reflectsColimit := fun {K : CategoryTheory.Functor J C} => CategoryTheory.Limits.reflectsColimitOfNatIso K h }
def
CategoryTheory.Limits.reflectsColimitsOfNatIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(h : F ≅ G)
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F]
:
Transfer reflection of colimits along a natural isomorphism in the functor.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfShapeOfEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{J' : Type w₂}
[CategoryTheory.Category.{w₂', w₂} J']
(e : J ≌ J')
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimitsOfShape J F]
:
Transfer reflection of colimits along an equivalence in the shape.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfSizeOfUnivLE
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[UnivLE.{w, w'} ]
[UnivLE.{w₂, w₂'} ]
[CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F]
:
A functor reflecting larger colimits also reflects smaller colimits.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfSizeShrink
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F]
:
reflectsColimitsOfSizeShrink.{w w'} F tries to obtain reflectsColimitsOfSize.{w w'} F
from some other reflectsColimitsOfSize F.
def
CategoryTheory.Limits.reflectsSmallestColimitsOfReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F]
:
Reflecting colimits at any universe implies reflecting colimits at universe 0.
def
CategoryTheory.Limits.reflectsColimitOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
(F : CategoryTheory.Functor J C)
(G : CategoryTheory.Functor C D)
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasColimit F]
[CategoryTheory.Limits.PreservesColimit F G]
:
If the colimit of F exists and G preserves it, then if G reflects isomorphisms then it
reflects the colimit of F.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfShapeOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{J : Type w}
[CategoryTheory.Category.{w', w} J]
{G : CategoryTheory.Functor C D}
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasColimitsOfShape J C]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
def
CategoryTheory.Limits.reflectsColimitsOfReflectsIsomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{G : CategoryTheory.Functor C D}
[G.ReflectsIsomorphisms]
[CategoryTheory.Limits.HasColimitsOfSize.{w', w, v₁, u₁} C]
[CategoryTheory.Limits.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.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.fullyFaithfulReflectsLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
[F.Faithful]
:
A fully faithful functor reflects limits.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.Limits.fullyFaithfulReflectsColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
[F.Faithful]
:
A fully faithful functor reflects colimits.
Equations
- One or more equations did not get rendered due to their size.