Closure under binary products

In this file, we introduce the closure of a property of objects under binary (co)products.

@[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

@[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