Properties of objects that are closed under finite limits

In this file, we introduce a typeclass IsClosedUnderFiniteLimits saying that a property of objects P : ObjectProperty C of a category C is closed under finite limits. The dual definition IsClosedUnderFiniteLimits is also introduced.

class CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) : Prop

A typeclass expressing that a property of objects is closed under finite limits.

• isClosedUnderLimitsOfShape (J : Type) [SmallCategory J] [FinCategory J] : P.IsClosedUnderLimitsOfShape J

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instIsClosedUnderFiniteProducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteLimits] : P.IsClosedUnderFiniteProducts

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instHasFiniteLimitsFullSubcategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteLimits] [Limits.HasFiniteLimits C] : Limits.HasFiniteLimits P.FullSubcategory

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteLimits.instPreservesFiniteLimitsFullSubcategoryι {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteLimits] [Limits.HasFiniteLimits C] : Limits.PreservesFiniteLimits P.ι

class CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) : Prop

A typeclass expressing that a property of objects is closed under finite colimits.

• isClosedUnderColimitsOfShape (J : Type) [SmallCategory J] [FinCategory J] : P.IsClosedUnderColimitsOfShape J

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instIsClosedUnderFiniteCoproducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteColimits] : P.IsClosedUnderFiniteCoproducts

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instHasFiniteColimitsFullSubcategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteColimits] [Limits.HasFiniteColimits C] : Limits.HasFiniteColimits P.FullSubcategory

instance CategoryTheory.ObjectProperty.IsClosedUnderFiniteColimits.instPreservesFiniteColimitsFullSubcategoryι {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteColimits] [Limits.HasFiniteColimits C] : Limits.PreservesFiniteColimits P.ι