CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts
theorem CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
[inst_2 : CategoryTheory.Limits.HasPushouts C], CategoryTheory.Limits.HasCoequalizers C
The theorem `CategoryTheory.Limits.hasCoequalizers_of_hasPushouts_and_binary_coproducts` asserts that, for any category `C` with binary coproducts and pushouts, the category `C` also has coequalizers. In other words, if a category can form a coproduct from any two objects and has a pushout for every pair of morphisms, then there exists a coequalizer for any pair of morphisms in the same category.
More concisely: In any category with binary coproducts and pushouts, every pair of morphisms has a coequalizer.
|
CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products
theorem CategoryTheory.Limits.hasEqualizers_of_hasPullbacks_and_binary_products :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
[inst_2 : CategoryTheory.Limits.HasPullbacks C], CategoryTheory.Limits.HasEqualizers C
This theorem states that in the field of category theory, any category 'C' that has both pullbacks and binary products will also have equalizers. Specifically, if we have a category 'C' (of any type 'u'), and this category has structures of binary products and pullbacks (as defined by `CategoryTheory.Limits.HasBinaryProducts C` and `CategoryTheory.Limits.HasPullbacks C` respectively), then it is guaranteed that this category 'C' also has the structure of equalizers (as defined by `CategoryTheory.Limits.HasEqualizers C`). The details of the proof are not provided here.
More concisely: In any category with binary products and pullbacks, equalizers exist.
|