hasBinaryCoproducts_of_hasInitial_and_pushouts
theorem hasBinaryCoproducts_of_hasInitial_and_pushouts :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
[inst_2 : CategoryTheory.Limits.HasPushouts C], CategoryTheory.Limits.HasBinaryCoproducts C
The theorem `hasBinaryCoproducts_of_hasInitial_and_pushouts` states that for any category `C` which has an initial object and pushouts, it must also have binary coproducts. In the language of category theory, this means that given two objects in the category, there exists an object which serves as their coproduct, provided the category has an initial object (the unique object from which there is exactly one morphism to any other object) and it has pushouts (certain types of colimits or generalized union operations).
More concisely: In any category with an initial object and pushouts, binary coproducts exist.
|
hasBinaryProducts_of_hasTerminal_and_pullbacks
theorem hasBinaryProducts_of_hasTerminal_and_pullbacks :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
[inst_2 : CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasBinaryProducts C
This theorem states that any category, denoted by `C`, which has pullbacks and a terminal object, possesses binary products. In the language of category theory, a category has binary products if for any pair of objects in the category, there exists a product object and product morphisms. This product object has the property that for any other object with morphisms to the given pair, there is a unique factorisation through the product. The theorem thus establishes how the existence of certain limit types (pullbacks and terminal objects) in a category guarantees the existence of another limit type (binary products).
More concisely: In a category with pullbacks and a terminal object, binary products exist and are unique up to isomorphism.
|