Properties of objects that are stable under finite products

We introduce typeclasses IsClosedUnderBinaryProducts and IsClosedUnderFiniteProducts expressing that P : ObjectProperty C is closed under binary products or finite products. We introduce a constructor for P.IsClosedUnderFiniteProducts assuming P.IsClosedUnderBinaryProducts, P.IsClosedUnderLimitsOfShape (Discrete.{0} PEmpty) and that C has finite products.

@[reducible, inline]

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

The typeclass saying that P : ObjectProperty C is stable under binary products.

Equations

• P.IsClosedUnderBinaryProducts = P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

theorem CategoryTheory.ObjectProperty.prop_prod {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderBinaryProducts] (X Y : C) [Limits.HasBinaryProduct X Y] (hX : P X) (hY : P Y) : P (X ⨯ Y)

theorem CategoryTheory.ObjectProperty.prop_of_isTerminal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] (X : C) (hX : Limits.IsTerminal X) : P X

theorem CategoryTheory.ObjectProperty.IsClosedUnderBinaryProducts.closedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasTerminal C] [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderIsomorphisms

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

The typeclass saying that P : ObjectProperty C is stable under finite products.

• isClosedUnderLimitsOfShape (J : Type) [Finite J] : P.IsClosedUnderLimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeDiscreteOfIsClosedUnderFiniteProductsOfFinite {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteProducts] (J : Type u_2) [Finite J] : P.IsClosedUnderLimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeDiscretePEmptyOfContainsZeroOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})

theorem CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.mk' {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} [Limits.HasFiniteProducts C] [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderBinaryProducts] : P.IsClosedUnderFiniteProducts