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_of_isLimit_binaryFan {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderBinaryProducts] {X Y : C} {B : Limits.BinaryFan X Y} (hB : Limits.IsLimit B) (hX : P X) (hY : P Y) : P B.pt

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.prop_terminal {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] [Limits.HasTerminal C] : P (⊤_ C)

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

@[reducible, inline]

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

All objects that are binary products of objects in P.

Equations

• P.binaryProductsClosure = P.limitClosure (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

theorem CategoryTheory.ObjectProperty.binaryProductsClosure_le_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasTerminal C] {P Q : ObjectProperty C} [Q.IsClosedUnderBinaryProducts] [Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})] : P.binaryProductsClosure ≤ Q ↔ P ≤ Q

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.instHasFiniteProductsFullSubcategoryOfIsClosedUnderFiniteProducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasFiniteProducts C] [P.IsClosedUnderFiniteProducts] : Limits.HasFiniteProducts P.FullSubcategory

theorem CategoryTheory.ObjectProperty.prop_of_isLimit_fan {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} {F : Limits.Fan f} (hF : Limits.IsLimit F) (h : ∀ (j : J), P (f j)) : P F.pt

theorem CategoryTheory.ObjectProperty.prop_product {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} [Limits.HasProduct f] (h : ∀ (j : J), P (f j)) : P (∏ᶜ f)

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

@[reducible, inline]

abbrev CategoryTheory.ObjectProperty.IsClosedUnderBinaryCoproducts {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 coproducts.

Equations

• P.IsClosedUnderBinaryCoproducts = P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

theorem CategoryTheory.ObjectProperty.prop_of_isColimit_binaryCofan {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderBinaryCoproducts] {X Y : C} {B : Limits.BinaryCofan X Y} (hB : Limits.IsColimit B) (hX : P X) (hY : P Y) : P B.pt

theorem CategoryTheory.ObjectProperty.prop_coprod {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderBinaryCoproducts] (X Y : C) [Limits.HasBinaryCoproduct X Y] (hX : P X) (hY : P Y) : P (X ⨿ Y)

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

theorem CategoryTheory.ObjectProperty.prop_initial {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})] [Limits.HasInitial C] : P (⊥_ C)

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

@[reducible, inline]

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

All objects that are binary coproducts of objects in P.

Equations

• P.binaryCoproductsClosure = P.colimitClosure (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)

theorem CategoryTheory.ObjectProperty.binaryCoproductsClosure_le_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasInitial C] {P Q : ObjectProperty C} [Q.IsClosedUnderBinaryCoproducts] [Q.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})] : P.binaryCoproductsClosure ≤ Q ↔ P ≤ Q

class CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts {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 coproducts.

• isClosedUnderColimitsOfShape (J : Type) [Finite J] : P.IsClosedUnderColimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeDiscreteOfIsClosedUnderFiniteCoproductsOfFinite {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteCoproducts] (J : Type u_2) [Finite J] : P.IsClosedUnderColimitsOfShape (Discrete J)

instance CategoryTheory.ObjectProperty.instHasFiniteCoproductsFullSubcategoryOfIsClosedUnderFiniteCoproducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasFiniteCoproducts C] [P.IsClosedUnderFiniteCoproducts] : Limits.HasFiniteCoproducts P.FullSubcategory

theorem CategoryTheory.ObjectProperty.prop_of_isColimit_cofan {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C} {F : Limits.Cofan f} (hF : Limits.IsColimit F) (h : ∀ (j : J), P (f j)) : P F.pt

theorem CategoryTheory.ObjectProperty.prop_coproduct {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderFiniteCoproducts] {J : Type u_2} [Finite J] {f : J → C} [Limits.HasCoproduct f] (h : ∀ (j : J), P (f j)) : P (∐ f)

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

theorem CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.mk' {C : Type u_1} [Category.{v_1, u_1} C] {P : ObjectProperty C} [Limits.HasFiniteCoproducts C] [P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})] [P.IsClosedUnderBinaryCoproducts] : P.IsClosedUnderFiniteCoproducts