CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers
theorem CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
[inst_2 : CategoryTheory.Limits.HasEqualizers C], CategoryTheory.Limits.HasPullbacks C
The theorem `CategoryTheory.Limits.hasPullbacks_of_hasBinaryProducts_of_hasEqualizers` states that for any category `C`, if `C` has binary products and equalizers, it also has pullbacks. Here, a binary product is a choice of product for every pair of objects in the category, an equalizer is a choice of equalizer for every pair of morphisms in the category, and a pullback is a choice of pullback for every pair of morphisms in the category. This theorem is not provided as an instance, indicating there might be more efficient ways to construct pullbacks.
More concisely: In any category with binary products and equalizers, pullbacks exist.
|
CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair
theorem CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
[inst : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair Y Z)]
[inst :
CategoryTheory.Limits.HasColimit
(CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl)
(CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr))],
CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)
The theorem states that in any category `C`, given objects `X`, `Y`, `Z` and morphisms `f` from `X` to `Y` and `g` from `X` to `Z`, if we have a colimit (also known as a coequalizer) for the coproduct of `Y` and `Z` and also for the parallel pair of morphisms formed by composing `f` with the inclusion map from the first component of the coproduct and `g` with the inclusion map from the second component of the coproduct, then we also have a colimit for the span of `f` and `g`. Here, the term 'span' refers to a functor from the walking span category (a category with three objects and two non-identity morphisms) to `C` that maps to `f` and `g`. The pushout of `f` and `g`, if it exists, is obtained by composing the inclusions with the coequalizer.
More concisely: Given objects X, Y, Z in any category C and morphisms f : X -> Y and g : X -> Z, if there exist colimits for the coproduct of Y and Z and their parallel morphisms under the inclusion maps, then there exists a colimit for the span of f and g, and their pushout is obtained by composing the inclusions with the coequalizer.
|
CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair
theorem CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair :
∀ {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.pair X Y)]
[inst :
CategoryTheory.Limits.HasLimit
(CategoryTheory.Limits.parallelPair (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst f)
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g))],
CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.cospan f g)
The theorem `CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair` states that if a category `C` has the product `X ⨯ Y` and the equalizer of the compositions `π₁ ≫ f` and `π₂ ≫ g`, then the pullback of the morphisms `f` and `g` also exists within that category. Here, `π₁` and `π₂` are projection maps to the first and the second components of the product, respectively. Essentially, this theorem tells us that the existence of certain limits in a category can ensure the existence of other limits. In this case, the existence of the product and equalizer guarantees the existence of the pullback. The pullback can be obtained by composing the equalizer with the respective projection.
More concisely: If a category has the product and the equalizer of the compositions of its projections with morphisms between the product's factors, then it has the pullback of those morphisms.
|
CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers
theorem CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
[inst_2 : CategoryTheory.Limits.HasCoequalizers C], CategoryTheory.Limits.HasPushouts C
The theorem `CategoryTheory.Limits.hasPushouts_of_hasBinaryCoproducts_of_hasCoequalizers` states that if a category has all binary coproducts and all coequalizers, then it necessarily has all pushouts. In the context of category theory, binary coproducts, coequalizers, and pushouts are certain kinds of limits and colimits, which are fundamental constructions that allow us to 'glue' together objects in a category. The theorem is not made as an instance, which means it won't be automatically used by Lean's type class system, because there might be a more efficient or direct way to construct pushouts in a specific category.
More concisely: In a category with binary coproducts and coequalizers, pushouts exist.
|