If a functor preserves limits, so does the induced functor in the Over or Under category #
Suppose we are given categories C and D, and object X : C, and a functor F : C ⥤ D.
F induces a functor Over.post F : Over X ⥤ Over (F.obj X). If F preserves limits of a
certain shape WithTerminal J, then Over.post F preserves limits of shape J.
As a corollary, if F preserves finite limits, or limits of a certain size, so does Over.post F.
Dually, if F preserves certain colimits, Under.post F will preserve certain colimits as well.
instance
CategoryTheory.Limits.PreservesLimitsOfShape.ofWidePullbacks
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
{J : Type u_1}
[PreservesLimitsOfShape (WidePullbackShape J) F]
:
instance
CategoryTheory.Limits.PreservesLimitsOfShape.overPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{X : C}
{F : Functor C D}
[PreservesLimitsOfShape (WithTerminal J) F]
:
instance
CategoryTheory.Limits.PreservesFiniteLimits.overPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{X : C}
{F : Functor C D}
[PreservesFiniteLimits F]
:
instance
CategoryTheory.Limits.PreservesLimitsOfSize.overPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{X : C}
{F : Functor C D}
[PreservesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
:
instance
CategoryTheory.Limits.PreservesColimitsOfShape.underPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{J : Type w}
[Category.{w', w} J]
{X : C}
{F : Functor C D}
[PreservesColimitsOfShape (WithInitial J) F]
:
instance
CategoryTheory.Limits.PreservesFiniteColimits.underPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{X : C}
{F : Functor C D}
[PreservesFiniteColimits F]
:
instance
CategoryTheory.Limits.PreservesColimitsOfSize.underPost
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{X : C}
{F : Functor C D}
[PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
: