CategoryTheory.IsPullback.of_bot
theorem CategoryTheory.IsPullback.of_bot :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
(CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ →
CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ → CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
The theorem `CategoryTheory.IsPullback.of_bot` states that in the context of a category `C`, given three objects `X₁₁`, `X₁₂`, `X₂₁`, `X₂₂`, `X₃₁`, `X₃₂` in `C`, and morphisms `h₁₁ : X₁₁ ⟶ X₁₂`, `h₂₁ : X₂₁ ⟶ X₂₂`, `h₃₁ : X₃₁ ⟶ X₃₂`, `v₁₁ : X₁₁ ⟶ X₂₁`, `v₁₂ : X₁₂ ⟶ X₂₂`, `v₂₁ : X₂₁ ⟶ X₃₁`, `v₂₂ : X₂₂ ⟶ X₃₂`, if we have a commuting square composed of the top square and a pullback square on the bottom, and if the composition of `h₁₁` and `v₁₂` equals the composition of `v₁₁` and `h₂₁`, then if the bottom square is a pullback square, the top square is also a pullback square.
In categorical language, a pullback square is a diagram that depicts a certain limit in a category. If we can show that the bottom square is a pullback, and the top square commutes, then the whole square is also a pullback.
More concisely: If a commutative square in a category has a pullback square at its bottom and the compositions of the outer two rectangular paths are equal, then the whole square is a pullback square.
|
CategoryTheory.IsPushout.of_horiz_isIso
theorem CategoryTheory.IsPushout.of_horiz_isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
{inr : Y ⟶ P} [inst_1 : CategoryTheory.IsIso f] [inst_2 : CategoryTheory.IsIso inr],
CategoryTheory.CommSq f g inl inr → CategoryTheory.IsPushout f g inl inr
This theorem states that in any category `C` with objects `Z`, `X`, `Y`, and `P`, and morphisms `f : Z ⟶ X`, `g : Z ⟶ Y`, `inl : X ⟶ P`, and `inr : Y ⟶ P`, if `f` and `inr` are isomorphisms and the diagram composed of these morphisms commutes, then the diagram is a pushout in the category. In category theory, a pushout is a kind of limit which can be thought of as a way of "gluing" objects together along a shared part.
More concisely: Given any commutative diagram of isomorphisms in a category with objects Z, X, Y, and P, where inl : X ⟶ P and inr : Y ⟶ P are the inclusion morphisms of a coproduct, if f : Z ⟶ X and g : Z ⟶ Y are the coproduct's unique coprojections, then this diagram is a pushout.
|
CategoryTheory.IsPushout.inr_fst
theorem CategoryTheory.IsPushout.inr_fst :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
This theorem is stating that in the category C, given that C has a zero object, has zero morphisms, and has a binary biproduct of objects X and Y, the square diagram where Y maps to the binary biproduct X ⊞ Y via the inclusion into the second summand `biprod.inr`, and where both Y and X ⊞ Y separately map to the zero object via the zero morphism, and where X ⊞ Y maps to X via the projection onto the first summand `biprod.fst`, is a pushout square. In categorical terms, a pushout is the colimit of a diagram consisting of two morphisms with a common domain.
More concisely: Given a category C with a zero object, zero morphisms, and binary biproducts, the diagram where the inclusion into the second summand forms a pushout with the zero morphism to the zero object and the projection onto the first summand, is a pushout square for any objects X and Y.
|
CategoryTheory.IsPullback.zero_left
theorem CategoryTheory.IsPullback.zero_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPullback 0 0 (CategoryTheory.CategoryStruct.id X) 0
The theorem `CategoryTheory.IsPullback.zero_left` states that for any category `C` (of type `Type u₁`) equipped with a zero object and zero morphisms, and for any object `X` in `C`, the square with the zero morphism `0 : 0 ⟶ 0` on the left and the identity morphism `𝟙 X` on the right is a pullback square. In category theory, a pullback square is a specific type of commutative square that exhibits the limit of a diagram. Here, it is showing that such a limit exists in the particular case of a diagram with a zero morphism and an identity morphism.
More concisely: In any category with a zero object and zero morphisms, the square formed by the zero morphism to the zero object and the identity morphism to an arbitrary object is a pullback square.
|
CategoryTheory.IsPullback.zero_top
theorem CategoryTheory.IsPullback.zero_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPullback 0 0 0 (CategoryTheory.CategoryStruct.id X)
The theorem `CategoryTheory.IsPullback.zero_top` states that for any category `C` that has a zero object and zero morphisms, and for any object `X` of `C`, the square with the zero morphism `0 : 0 ⟶ 0` as the top edge and the identity morphism on `X` as the bottom edge, is a pullback square in the categorical sense. In other words, for each object `X`, the diagram formed by the zero morphisms and the identity morphism on `X` has the universal property defining a pullback.
More concisely: In any category with a zero object and zero morphisms, the diagram consisting of the zero morphism to the zero object and the identity morphism on any object forms a pullback square.
|
CategoryTheory.IsPushout.of_bot
theorem CategoryTheory.IsPushout.of_bot :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
(CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ →
CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁ →
CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ → CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁
The theorem `CategoryTheory.IsPushout.of_bot` in the Category Theory states that given a "pushout" square which is assembled from an upper pushout square and a lower commuting square, the lower square will also be a pushout square under certain conditions. In more detail, for any objects `X₁₁`, `X₁₂`, `X₂₁`, `X₂₂`, `X₃₁`, `X₃₂` and morphisms `h₁₁`, `h₂₁`, `h₃₁`, `v₁₁`, `v₁₂`, `v₂₁`, `v₂₂` in a category `C`, if the composite of `v₁₁` and `v₂₁` along with `h₁₁` forms a pushout, and the composite of `v₁₂` and `v₂₂` along with `h₃₁` forms a pushout, and the composite of `h₂₁` and `v₂₂` is equal to the composite of `v₂₁` and `h₃₁`, then if the composite of `h₁₁` and `v₁₁` along with `h₂₁` forms a pushout, it implies that the composite of `h₂₁` and `v₂₁` along with `h₃₁` also forms a pushout.
More concisely: If a pushout square is obtained by assembling an upper pushout square and a commutative lower square, and the two composites in the lower square form pushouts, then the composite of the morphisms in the lower square forming the pushout in the upper square also forms a pushout.
|
CategoryTheory.IsPushout.of_is_coproduct
theorem CategoryTheory.IsPushout.of_is_coproduct :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y},
CategoryTheory.Limits.IsColimit c →
∀ (t : CategoryTheory.Limits.IsInitial Z),
CategoryTheory.IsPushout
(t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
(t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl
c.inr
The theorem `CategoryTheory.IsPushout.of_is_coproduct` states that if `c` is a colimiting binary coproduct cocone in a category `C`, and we have an initial object `Z`, then we can construct a pushout square. Specifically, the morphisms of the pushout square are the unique morphisms from the initial object to `X` and `Y` (given by the functor `CategoryTheory.Limits.pair X Y`), and the injections `c.inl` and `c.inr` of the binary cofan `c`. In terms of category theory, this provides a connection between the concepts of coproducts, initial objects, and pushouts.
More concisely: Given a category with an initial object and a binary coproduct cocone with colimit `c` in it, the pushout of the morphisms from the initial object to the coproduct components exists and is given by the unique morphisms from the initial object to each component and the injections of the coproduct.
|
CategoryTheory.IsPushout.inl_snd
theorem CategoryTheory.IsPushout.inl_snd :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
The theorem `CategoryTheory.IsPushout.inl_snd` states that for any Type `C`, which forms a Category, `X` and `Y` being objects in that Category, and given that the Category `C` has a zero object, zero morphisms, and a binary biproduct for `X` and `Y`, the square diagram with `X` and `0` as objects on the left, `X ⊞ Y` and `Y` as objects on the right, `CategoryTheory.Limits.biprod.inl` and the zero morphism as morphisms from top to bottom on the left, and `CategoryTheory.Limits.biprod.snd` and the zero morphism as morphisms from top to bottom on the right, constitutes a pushout. In other words, the diagram is a pushout square, meaning that for any other object `Z` in the category and any pair of morphisms from `X` to `Z` and `Y` to `Z` making the diagram commute, there exists a unique morphism from `X ⊞ Y` to `Z` making the entire diagram commute.
More concisely: Given a Category `C` with a zero object, zero morphisms, and binary biproducts, the diagram formed by `X`, `Y`, `X ⊞ Y`, `0`, the zero morphisms, `CategoryTheory.Limits.biprod.inl`, and `CategoryTheory.Limits.biprod.snd` is a pushout square in `C`.
|
CategoryTheory.IsPullback.paste_vert
theorem CategoryTheory.IsPullback.paste_vert :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁ →
CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁ →
CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
(CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁
This theorem in Category Theory states that given two squares in a category that are designated as pullbacks, if these squares are "pasted" together vertically, the resulting larger square is also a pullback.
The pullback squares are determined by morphisms from certain objects in the category. In this theorem, the category is denoted by `C` and the objects in the category are `X₁₁, X₁₂, X₂₁, X₂₂, X₃₁, X₃₂`. The morphisms are `h₁₁, h₂₁, h₃₁` (the vertical arrows in the squares) and `v₁₁, v₁₂, v₂₁, v₂₂` (the horizontal arrows in the squares).
The theorem further states that if `h₁₁` and `v₁₁` to `v₁₂` form a pullback square with `h₂₁`, and `h₂₁` and `v₂₁` to `v₂₂` form another pullback square with `h₃₁`, then `h₁₁` and the composition of `v₁₁` and `v₂₁` to the composition of `v₁₂` and `v₂₂` also form a pullback square with `h₃₁`.
More concisely: Given two pullback squares in a category with the given morphisms, if their vertical arrows compose to form another vertical arrow and the horizontal arrows compose to form another horizontal arrow, then the resulting rectangle is a pullback square.
|
CategoryTheory.IsPullback.paste_horiz
theorem CategoryTheory.IsPullback.paste_horiz :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁ →
CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂ →
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
(CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)
This theorem states that in a category `C`, given two pairs of objects `(X₁₁, X₂₁)`, `(X₁₃, X₂₃)` and morphisms `h₁₁ : X₁₁ ⟶ X₁₂`, `h₁₂ : X₁₂ ⟶ X₁₃`, `h₂₁ : X₂₁ ⟶ X₂₂`, `h₂₂ : X₂₂ ⟶ X₂₃`, `v₁₁ : X₁₁ ⟶ X₂₁`, `v₁₂ : X₁₂ ⟶ X₂₂`, `v₁₃ : X₁₃ ⟶ X₂₃`. If we have pullback squares formed by `h₁₁, v₁₁, v₁₂, h₂₁` and `h₁₂, v₁₂, v₁₃, h₂₂`, then we can "paste" these two pullback squares "horizontally" to construct another pullback square. This new square is formed by the composite morphisms `h₁₁ ≫ h₁₂` and `h₂₁ ≫ h₂₂`, with `v₁₁` and `v₁₃` as the vertical morphisms.
More concisely: Given pullback squares in a category with morphisms `h₁₁, h₁₂, h₂₁, h₂₂, v₁₁, v₁₂, v₁₃`, if the outer rectangle commutes, then the inner rectangle formed by composing the horizontal morphisms and using the vertical morphisms as the vertical morphisms in the new square, also forms a pullback square.
|
CategoryTheory.IsPushout.zero_left
theorem CategoryTheory.IsPushout.zero_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPushout 0 0 (CategoryTheory.CategoryStruct.id X) 0
This theorem states that for any category 'C' with zero objects and zero morphisms, and for any object 'X' in 'C', the square diagram with the zero morphism '0 : 0 ⟶ 0' on the left and the identity morphism '𝟙 X' on the right is a pushout square. In category theory, a pushout is the categorical dual of a pullback. Thus, this theorem asserts a specific condition under which a pushout configuration is achieved in a category with zero objects and morphisms.
More concisely: In any category with zero objects and morphisms, the square formed by a zero morphism and the identity morphism is a pushout square for any object.
|
CategoryTheory.IsPullback.inr_fst
theorem CategoryTheory.IsPullback.inr_fst :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0
This theorem states that in the context of a category `C` that has a zero object and zero morphisms, and for any two objects `X` and `Y` in `C` that have a binary biproduct, the given square diagram is a pullback square. In this diagram, the object `Y` is mapped to the biproduct `X ⊞ Y` via the inclusion `inr`, and both `Y` and `X ⊞ Y` are mapped to the zero object via zero morphisms. Finally, the biproduct `X ⊞ Y` is mapped to `X` via the projection `fst`. In categorical terms, a pullback square is a commutative diagram where the unique morphism satisfying the universal property of the pullback exists.
More concisely: In a category with a zero object and zero morphisms, the square diagram formed by the inclusion, zero morphism, and projection of a binary biproduct is a pullback square.
|
CategoryTheory.IsPushout.of_hasPushout
theorem CategoryTheory.IsPushout.of_hasPushout :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} (f : Z ⟶ X) (g : Z ⟶ Y)
[inst_1 : CategoryTheory.Limits.HasPushout f g],
CategoryTheory.IsPushout f g CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr
This theorem states that for any category `C` and any objects `Z`, `X`, `Y` in `C`, if we have morphisms `f : Z ⟶ X` and `g : Z ⟶ Y` and the pushout of `f` and `g` exists, then the structure formed by `f`, `g` and the inclusions `CategoryTheory.Limits.pushout.inl` and `CategoryTheory.Limits.pushout.inr` into the pushout is indeed an `IsPushout`. In terms of category theory, it means that the specific choice of colimiting cocone provided by the `HasPushout` structure is actually a pushout.
More concisely: Given any category `C` and objects `Z`, `X`, `Y` with morphisms `f : Z ⟶ X` and `g : Z ⟶ Y` having a pushout, the resulting structure formed by `f`, `g`, and the inclusion morphisms into the pushout is an isomorphism of categories, i.e., a pushout.
|
CategoryTheory.BicartesianSq.of_is_biproduct₁
theorem CategoryTheory.BicartesianSq.of_is_biproduct₁ :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
{b : CategoryTheory.Limits.BinaryBicone X Y}, b.IsBilimit → CategoryTheory.BicartesianSq b.fst b.snd 0 0
This theorem states that in any category `C` endowed with a zero object and zero morphisms, given any two objects `X` and `Y` and a binary bicone `b` which is a bilimit, we have a bicartesian square. A bicartesian square involves two morphisms (`b.fst` and `b.snd`) from the binary product `X ⊞ Y` to `X` and `Y`, respectively, and two zero morphisms from `X` and `Y` to a zero object, forming a commutative square.
More concisely: In any category with a zero object and zero morphisms, given a binary bicone over the product of two objects that is a bilimit, there exist unique morphisms from the product to each object making a commutative square with the zero morphisms to the zero object.
|
CategoryTheory.BicartesianSq.of_has_biproduct₂
theorem CategoryTheory.BicartesianSq.of_has_biproduct₂ :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.BicartesianSq 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
This theorem states that in any category 'C' with a zero object and zero morphisms, and for any two objects 'X' and 'Y' in 'C' for which a binary biproduct exists, the diagram consisting of the zero morphisms from the zero object to 'X' and 'Y', and the inclusion morphisms 'inl' and 'inr' from 'X' and 'Y' to the binary biproduct 'X ⊞ Y', forms a bicartesian square. A bicartesian square is a commutative diagram in a category where all the morphisms involved have both left and right adjoints.
More concisely: In any category with a zero object and zero morphisms, the diagram formed by the zero morphisms to two objects X and Y, and the inclusion morphisms to their binary biproduct, is a commutative square where all morphisms have both left and right adjoints.
|
CategoryTheory.IsPushout.of_right
theorem CategoryTheory.IsPushout.of_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
(CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) →
CategoryTheory.CategoryStruct.comp h₁₂ v₁₃ = CategoryTheory.CategoryStruct.comp v₁₂ h₂₂ →
CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ → CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂
In a category `C` with objects `X₁₁`, `X₁₂`, `X₁₃`, `X₂₁`, `X₂₂`, and `X₂₃`, and morphisms `h₁₁`, `h₁₂`, `h₂₁`, `h₂₂`, `v₁₁`, `v₁₂`, and `v₁₃`, the theorem `CategoryTheory.IsPushout.of_right` states that if we have a pushout square composed of a left pushout square and a right commuting square, then the right square is also a pushout square. This is under the condition that the composite of `h₁₂` and `v₁₃` is equal to the composite of `v₁₂` and `h₂₂`, and `h₁₁`, `v₁₁`, `v₁₂`, and `h₂₁` form a pushout square. In other words, given a commutative cube where the front and back faces are pushouts, if the left face and the top, bottom and right faces commute, then the right face is also a pushout.
More concisely: Given a commutative cube in a category with front and back faces being pushout squares, if the left face and the top, bottom, and right faces commute, then the right face is also a pushout square.
|
CategoryTheory.IsPullback.zero_right
theorem CategoryTheory.IsPullback.zero_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPullback 0 (CategoryTheory.CategoryStruct.id X) 0 0
The theorem `CategoryTheory.IsPullback.zero_right` states that for any category `C` with a zero object and zero morphisms, and any object `X` in `C`, the square with `0 : 0 ⟶ 0` on the right and the identity morphism on `X` (notated as `𝟙 X`) on the left is a pullback square. In category theory, a pullback (also called a fiber product, Cartesian square, or limit of a diagram) is the most general way of defining a "product" of two morphisms. Here, the product of the zero morphism and the identity morphism on `X` is itself a zero morphism.
More concisely: In any category with a zero object and zero morphisms, the square with a zero morphism on the right and the identity morphism on an object X is a pullback square, making the zero morphism the product of the zero morphism and identity morphism on X.
|
CategoryTheory.IsPullback.inl_snd
theorem CategoryTheory.IsPullback.inl_snd :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0
The theorem `CategoryTheory.IsPullback.inl_snd` states that in any category `C` that has a zero object and zero morphisms, as well as binary biproducts, the square diagram formed by the inclusion of an object `X` into the binary biproduct `X ⊞ Y` (denoted as `CategoryTheory.Limits.biprod.inl`), the projection of `X ⊞ Y` onto `Y` (denoted as `CategoryTheory.Limits.biprod.snd`), and the zero morphisms, is a pullback square. In other words, any morphism into `X` that makes the outer rectangle commute (i.e., the composition of morphisms along the top and right equals the composition along the bottom and left) can be factored uniquely through the morphism `X --inl--> X ⊞ Y`, which is a characteristic property of pullback squares in category theory.
More concisely: In a category with a zero object, zero morphisms, and binary biproducts, the square formed by the inclusion of an object into its binary biproduct, the projection of the binary biproduct onto the second factor, and the zero morphisms is a pullback square.
|
CategoryTheory.IsPushout.paste_horiz
theorem CategoryTheory.IsPushout.paste_horiz :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂ →
CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
(CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)
The theorem `CategoryTheory.IsPushout.paste_horiz` states that within a category `C`, for any two pushout squares which horizontally share a common morphism, a new pushout square can be formed by pasting the two squares horizontally. More specifically, given six objects `X₁₁`, `X₁₂`, `X₁₃`, `X₂₁`, `X₂₂` and `X₂₃` in `C`, and nine morphisms between them (`h₁₁`, `h₁₂`, `h₂₁`, `h₂₂`, `v₁₁`, `v₁₂`, and `v₁₃`), if the objects and morphisms form two pushout squares (`h₁₁, v₁₁, v₁₂, h₂₁` and `h₁₂, v₁₂, v₁₃, h₂₂`), then a new pushout square can be formed by using the composition of `h₁₁` and `h₁₂`, and the composition of `h₂₁` and `h₂₂`. The concept of a pushout square comes from category theory and represents a certain kind of limit called a colimit. It essentially represents a "union" operation in the category that combines objects while preserving the morphisms between them.
More concisely: Given any two commutative pushout squares in a category with a common morphism, their horizontal composition forms a new pushout square.
|
CategoryTheory.IsPushout.paste_vert
theorem CategoryTheory.IsPushout.paste_vert :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂},
CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁ →
CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁ →
CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁)
(CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁
The theorem `CategoryTheory.IsPushout.paste_vert` states that in a category `C`, given two pushout squares, one with objects `X₁₁`, `X₁₂`, `X₂₁`, `X₂₂`, and the other with objects `X₂₁`, `X₂₂`, `X₃₁`, `X₃₂`, and morphisms as described in the theorem, if the first square is a pushout along the morphisms `h₁₁` and `h₂₁`, and the second square is a pushout along the morphisms `h₂₁` and `h₃₁`, then pasting the two squares vertically (i.e., identifying `X₂₁` and `X₂₂` of the first square with `X₂₁` and `X₂₂` of the second square, respectively) yields another pushout square, this time along the morphisms `h₁₁` and `h₃₁`. In essence, the theorem says that pushouts in a category can be "stitched" together vertically to obtain a larger pushout.
More concisely: Given two pushout squares in a category with common morphism, if both squares are pushouts along the common morphism, then their vertical pasting forms another pushout.
|
CategoryTheory.BicartesianSq.of_isPullback_isPushout
theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z},
CategoryTheory.IsPullback f g h i → CategoryTheory.IsPushout f g h i → CategoryTheory.BicartesianSq f g h i
This theorem states that for any category `C` with objects `W`, `X`, `Y`, `Z`, and morphisms `f : W ⟶ X`, `g : W ⟶ Y`, `h : X ⟶ Z`, `i : Y ⟶ Z`, if the diagram formed by these objects and morphisms is a pullback and a pushout, then it is a bicartesian square. In the context of category theory, a pullback is a limit of a diagram, while a pushout is a colimit. A bicartesian square is a particular kind of diagram in a category that has both a pullback and a pushout.
More concisely: If a diagram consisting of objects W, X, Y, Z and morphisms f : W ⟶ X, g : W ⟶ Y, h : X ⟶ Z, i : Y ⟶ Z forms both a pullback and a pushout square, then it is a bicartesian square.
|
CategoryTheory.BicartesianSq.isColimit'
theorem CategoryTheory.BicartesianSq.isColimit' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
{i : Y ⟶ Z} (self : CategoryTheory.BicartesianSq f g h i),
Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯))
This theorem asserts that for any bicartesian square in a category, the pushout cocone is a colimit. Specifically, given a category `C` and objects `W`, `X`, `Y`, `Z` in `C`, along with morphisms `f : W ⟶ X`, `g : W ⟶ Y`, `h : X ⟶ Z`, and `i : Y ⟶ Z` that form a bicartesian square, there exists a colimit for the pushout cocone generated by `h` and `i`.
More concisely: Given a bicartesian square in a category, the pushout cocone exists and is a colimit.
|
CategoryTheory.IsPullback.of_right
theorem CategoryTheory.IsPullback.of_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂}
{h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃},
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃
(CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) →
CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁ →
CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂ → CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁
This theorem, `CategoryTheory.IsPullback.of_right`, states that in the context of a Category Theory, given a type `C` that forms a category, and six objects `X₁₁, X₁₂, X₁₃, X₂₁, X₂₂, X₂₃` in this category, along with morphisms between these objects (`h₁₁, h₁₂, h₂₁, h₂₂` as horizontal morphisms and `v₁₁, v₁₂, v₁₃` as vertical morphisms), if we have a commuting square formed by `h₁₁, h₁₂, v₁₁, v₁₃` on the left and a pullback square formed by `h₂₁, h₂₂, v₁₂, v₁₃` on the right such that the compositions of `h₁₁` with `v₁₂` and `v₁₁` with `h₂₁` are equal, then the left square (formed by `h₁₁, v₁₁, v₁₂, h₂₁`) is also a pullback square. In simpler words, it states that if the right square is a pullback square, then the left square is also a pullback square under certain conditions.
More concisely: If a commutative diagram in a category with given morphisms and objects forms a pullback square on the right and the conditions of commutativity and vertical compositions with the morphisms on the left side are met, then the diagram forms a pullback square on the left.
|
CategoryTheory.IsPushout.zero_right
theorem CategoryTheory.IsPushout.zero_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPushout 0 (CategoryTheory.CategoryStruct.id X) 0 0
This theorem, named `CategoryTheory.IsPushout.zero_right`, states that for any category `C` with a zero object and zero morphisms, and for any object `X` in `C`, the square with `0 : 0 ⟶ 0` on the right and the identity morphism on `X` on the left is a pushout square. In the context of category theory, a pushout square is a diagram that allows us to "glue" objects together along maps. The zero object and zero morphisms are special objects and morphisms, respectively, that behave like the number zero in ordinary arithmetic.
More concisely: For any category with a zero object and zero morphisms, the square with the zero morphism on the right and the identity on any object X is a pushout square.
|
CategoryTheory.IsPushout.of_isColimit
theorem CategoryTheory.IsPushout.of_isColimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y}
{c : CategoryTheory.Limits.PushoutCocone f g},
CategoryTheory.Limits.IsColimit c → CategoryTheory.IsPushout f g c.inl c.inr
The theorem `CategoryTheory.IsPushout.of_isColimit` states that for any category `C`, and any objects `Z`, `X`, `Y` in `C`, if `c` is a pushout cocone formed by two morphisms `f : Z ⟶ X` and `g : Z ⟶ Y`, and if `c` is a colimit cocone, then we can form a pushout structure with `f` and `g` as the incoming morphisms and `c.inl` and `c.inr` (the first and second inclusions of the pushout cocone) as the outgoing morphisms. In other words, if a pushout cocone is a colimit, it induces a pushout structure.
More concisely: If a pushout cocone in a category is a colimit cocone, then it induces a pushout structure.
|
CategoryTheory.IsPullback.of_is_product'
theorem CategoryTheory.IsPullback.of_is_product' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y},
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd) →
∀ (t : CategoryTheory.Limits.IsTerminal Z), CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)
The theorem `CategoryTheory.IsPullback.of_is_product'` states that for any category `C` with objects `P`, `X`, `Y`, `Z`, and morphisms `fst` from `P` to `X` and `snd` from `P` to `Y`, if the binary fan made of `fst` and `snd` is a limit, and `Z` is a terminal object in the category, then the pair of morphisms `fst` and `snd` form a pullback with respect to the unique morphisms from `Z` to `X` and `Z` to `Y` respectively. In other words, the square formed by `fst`, `snd`, and the unique morphisms from `Z` to `X` and `Z` to `Y` is a pullback square.
More concisely: If in a category with a terminal object, the binary product of two morphisms forms a limit, then those morphisms form a pullback with respect to the unique morphisms to the terminal object from each domain.
|
CategoryTheory.IsPushout.of_isBilimit
theorem CategoryTheory.IsPushout.of_isBilimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
{b : CategoryTheory.Limits.BinaryBicone X Y}, b.IsBilimit → CategoryTheory.IsPushout 0 0 b.inl b.inr
This theorem states that for any category `C` with zero objects and zero morphisms, and any pair `X, Y` of objects in `C` forming a binary bicone `b`, if `b` is a bilimit in `C`, then the morphisms `b.inl` and `b.inr` form a pushout at the zero morphism. In the language of category theory, a pushout is a universal construction which is the categorical dual of a pullback, while a bilimit is a limit for a diagram indexed by a finite category.
More concisely: Given a category with zero objects and morphisms, if a binary bicone in this category is a bilimit, then its two components form a pushout at the zero morphism.
|
CategoryTheory.IsPullback.of_is_product
theorem CategoryTheory.IsPullback.of_is_product :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y},
CategoryTheory.Limits.IsLimit c →
∀ (t : CategoryTheory.Limits.IsTerminal Z),
CategoryTheory.IsPullback c.fst c.snd
(t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }))
(t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))
This theorem states that if `c` is a limiting binary product cone in a category `C`, and we also have a terminal object `Z` in `C`, then `c` forms a pullback diagram with the unique morphisms from `X` and `Y` (the objects of the binary product) to the terminal object `Z`. In simple words, when we have a product and a terminal object in a category, we can form a pullback using the product morphisms and the unique morphisms to the terminal object.
More concisely: Given a category with a product and a terminal object, every limiting binary product cone forms a pullback diagram with the unique morphisms to the terminal object from the product's factors.
|
CategoryTheory.IsPullback.flip
theorem CategoryTheory.IsPullback.flip :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
{g : Y ⟶ Z}, CategoryTheory.IsPullback fst snd f g → CategoryTheory.IsPullback snd fst g f
This theorem states that in any category `C`, if we have objects `P`, `X`, `Y`, and `Z` with morphisms `fst : P ⟶ X`, `snd : P ⟶ Y`, `f : X ⟶ Z` and `g : Y ⟶ Z` that form a pullback square (meaning that the diagram commutes and `P` is a product of `X` and `Y` over `Z` with projections `fst` and `snd`), then flipping the roles of `X` and `Y`, and `fst` and `snd`, also results in a pullback square. In other words, a pullback in a category is symmetric with respect to the two projection morphisms.
More concisely: In a category C, if objects P, X, Y, and Z, and morphisms fst : P → X, snd : P → Y, f : X → Z, and g : Y → Z form a pullback square, then interchanging X and Y, and fst and snd, also results in a pullback square.
|
CategoryTheory.BicartesianSq.of_is_biproduct₂
theorem CategoryTheory.BicartesianSq.of_is_biproduct₂ :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
{b : CategoryTheory.Limits.BinaryBicone X Y}, b.IsBilimit → CategoryTheory.BicartesianSq 0 0 b.inl b.inr
The theorem `CategoryTheory.BicartesianSq.of_is_biproduct₂` states that for any category `C` with zero objects and zero morphisms, and any two objects `X` and `Y` in `C`, if we have a binary bicone `b` of `X` and `Y` that is a bilimit, then the square composed of the zero morphisms from 0 to `X` and `Y`, and the inclusion morphisms `inl` and `inr` from `X` and `Y` to the coproduct `X ⊞ Y`, is a bicartesian square. In other words, this theorem asserts the commutativity of the square diagram where the top and left sides are zero morphisms, and the right and bottom sides are the inclusions to the coproduct.
More concisely: Given a category with zero objects and morphisms, if a binary bicone from objects X and Y is a bilimit, then the square formed by the zero morphisms to X and Y, and the inclusions to their coproduct, is a bicartesian square.
|
CategoryTheory.IsPullback.of_isBilimit
theorem CategoryTheory.IsPullback.of_isBilimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
{b : CategoryTheory.Limits.BinaryBicone X Y}, b.IsBilimit → CategoryTheory.IsPullback b.fst b.snd 0 0
This theorem states that in a category `C` with zero object and zero morphisms, for any `BinaryBicone` `b` (consisting of two objects `X` and `Y`), if `b` is a bilimit in `C`, then the morphisms `b.fst` and `b.snd` form a pullback diagram in `C` with respect to the zero object and zero morphisms. In other words, if `b` is a bilimit, then `b.fst` and `b.snd` satisfy the universal property of the pullback, thus making them a pullback of 0 and 0.
More concisely: In a category with zero object and zero morphisms, if a binary bicone is a bilimit, then its first and second projections form a pullback diagram with the zero object and morphisms.
|
CategoryTheory.IsPushout.flip
theorem CategoryTheory.IsPushout.flip :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
{inr : Y ⟶ P}, CategoryTheory.IsPushout f g inl inr → CategoryTheory.IsPushout g f inr inl
This theorem states that for any category 'C', and any objects 'Z', 'X', 'Y', and 'P' in 'C', if we have morphisms 'f' from 'Z' to 'X', 'g' from 'Z' to 'Y', 'inl' from 'X' to 'P', and 'inr' from 'Y' to 'P', if the given setup forms a pushout diagram, then switching the roles of 'X' and 'Y', 'f' and 'g', and 'inl' and 'inr' will still yield a pushout diagram. In essence, a pushout in a category is invariant under flipping the input and output objects and morphisms.
More concisely: Given any pushout diagram in a category with objects Z, X, Y, and P, and morphisms f: Z -> X, g: Z -> Y, inl: X -> P, and inr: Y -> P, the resulting diagram obtained by interchanging X and Y, and f and g, and inl and inr, is also a pushout.
|
CategoryTheory.IsPushout.of_is_coproduct'
theorem CategoryTheory.IsPushout.of_is_coproduct' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {inl : X ⟶ P} {inr : Y ⟶ P},
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr) →
∀ (t : CategoryTheory.Limits.IsInitial Z), CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr
This theorem states that, given any Category 'C', and objects 'Z', 'X', 'Y', and 'P' in 'C', along with morphisms 'inl' from 'X' to 'P' and 'inr' from 'Y' to 'P', if the binary cofan formed by 'inl' and 'inr' is a colimit, and 'Z' is an initial object (meaning that the cocone induced by 'Z' on the empty diagram is a colimit), then the square formed by the morphisms from 'Z' to 'X' and 'Y', and 'inl' and 'inr' is a pushout square.
In simpler words, it provides a condition under which a certain diagram in a category is a pushout diagram, which plays a key role in the construction and analysis of categorical limits and colimits.
More concisely: Given any category 'C', objects 'Z', 'X', 'Y', and 'P' with 'inl' from 'X' to 'P' and 'inr' from 'Y' to 'P' as morphisms, if the binary coproduct 'P' formed by 'inl' and 'inr' is a colimit and 'Z' is an initial object, then the square formed by the morphisms from 'Z' to 'X' and 'Y', and 'inl' and 'inr' is a pushout square.
|
CategoryTheory.IsPullback.isLimit'
theorem CategoryTheory.IsPullback.isLimit' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
{g : Y ⟶ Z} (self : CategoryTheory.IsPullback fst snd f g),
Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯))
This theorem states that for any category `C` with objects `P`, `X`, `Y`, and `Z` and morphisms `fst` from `P` to `X`, `snd` from `P` to `Y`, `f` from `X` to `Z`, and `g` from `Y` to `Z`, if these morphisms and objects form a pullback, then there is a limit to the pullback cone made with `fst` and `snd`. In other words, the pullback cone has a limit in the category theory sense. This limit is a special kind of object that represents the "best" way to map into the cone from any other cone.
More concisely: Given a pullback square in a category with a limit-preserving category, the pullback cone has a limit.
|
CategoryTheory.IsPullback.of_isLimit'
theorem CategoryTheory.IsPullback.of_isLimit' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
{g : Y ⟶ Z} (w : CategoryTheory.CommSq fst snd f g),
CategoryTheory.Limits.IsLimit w.cone → CategoryTheory.IsPullback fst snd f g
The theorem `CategoryTheory.IsPullback.of_isLimit'` states that for any category `C`, and objects `P`, `X`, `Y`, `Z` in `C`, with morphisms `fst : P ⟶ X`, `snd : P ⟶ Y`, `f : X ⟶ Z`, `g : Y ⟶ Z` that form a commutative square `w` (i.e., a diagram where both paths from `P` to `Z` via `X` or `Y` are the same), if the cone formed by this commutative square is a limit, then we can say that the pullback of `f` and `g` along `fst` and `snd` exists. In categorical terms, this theorem provides a condition under which a pullback can be formed.
More concisely: If in a commutative square in a category with a limit cone, the cone is a limit, then the pullback of the two morphisms forming the square exists.
|
CategoryTheory.IsPullback.zero_bot
theorem CategoryTheory.IsPullback.zero_bot :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) 0 0 0
This theorem states that, for any category `C` (which has a zero object and zero morphisms) and any object `X` in `C`, the square with `0 : 0 ⟶ 0` on the bottom and the identity morphism on `X` on the top is a pullback square. In category theory, a pullback square provides a universal property for the limit of a diagram. In this case, the theorem says that the square featuring identity and zero morphism is such a pullback.
More concisely: For any category with a zero object and zero morphisms, the square with a zero morphism at the bottom and identity morphism at the top is a pullback square for every object.
|
CategoryTheory.IsPullback.of_vert_isIso
theorem CategoryTheory.IsPullback.of_vert_isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
{g : Y ⟶ Z} [inst_1 : CategoryTheory.IsIso snd] [inst_2 : CategoryTheory.IsIso f],
CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
This theorem states that in a category `C` with objects `P`, `X`, `Y`, and `Z`, given morphisms `fst : P ⟶ X`, `snd : P ⟶ Y`, `f : X ⟶ Z` and `g : Y ⟶ Z`, if `snd` and `f` are isomorphisms and the diagram commutes (i.e., `fst` followed by `f` equals `snd` followed by `g`), then the square formed by these morphisms is a pullback square. A pullback square is a special kind of diagram in category theory that represents the limit of a diagram.
More concisely: Given morphisms `fst : P ⟶ X`, `snd : P ⟶ Y`, `f : X ⟶ Z`, and `g : Y ⟶ Z` in a category `C` such that `snd` and `f` are isomorphisms and the diagram commutes (`fst ∘ f = snd ∘ g`), then `(fst, f)` is the pullback of `(snd, g)`.
|
CategoryTheory.BicartesianSq.of_has_biproduct₁
theorem CategoryTheory.BicartesianSq.of_has_biproduct₁ :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
[inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0
The theorem `CategoryTheory.BicartesianSq.of_has_biproduct₁` states that for any category `C` with a zero object and zero morphisms, and for any objects `X` and `Y` in `C` that have a binary biproduct, the diagram formed by the projections onto the first and second summands of the binary biproduct (denoted by `fst` and `snd` respectively) and the zero morphisms is a bicartesian square.
In simpler terms, this means that the diagram commutes, i.e., the different paths between any two objects in the diagram are equivalent in the categorical sense. In this case, the paths from `X ⊞ Y` (the binary biproduct of `X` and `Y`) to `X` and `Y`, and from there to the zero object `0` are equivalent.
More concisely: For any category with a zero object and zero morphisms and objects with a binary biproduct, the diagram formed by the projections and zero morphisms commutes.
|
CategoryTheory.IsPullback.map
theorem CategoryTheory.IsPullback.map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X}
{g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
[inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F],
CategoryTheory.IsPullback f g h i → CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
The theorem `CategoryTheory.IsPullback.map` states that given two categories `C` and `D`, and a functor `F` from `C` to `D`, if the cospan created by morphisms `h` from `X` to `Z` and `i` from `Y` to `Z` in `C` has preserved limits under the functor `F`, then if the square formed by morphisms `f` from `W` to `X`, `g` from `W` to `Y`, `h` from `X` to `Z`, and `i` from `Y` to `Z` in `C` is a pullback, the resulting square in `D` formed by the images of these morphisms under `F` is also a pullback.
In other words, this theorem is about the preservation of pullback squares under functors that preserve limits of specific types of diagrams (cospans in this case).
More concisely: If a functor preserves limits of cospans and a pullback square holds in a category, then the image of that square under the functor is also a pullback square in the target category.
|
CategoryTheory.IsPushout.of_isColimit'
theorem CategoryTheory.IsPushout.of_isColimit' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
{inr : Y ⟶ P} (w : CategoryTheory.CommSq f g inl inr),
CategoryTheory.Limits.IsColimit w.cocone → CategoryTheory.IsPushout f g inl inr
This theorem, `CategoryTheory.IsPushout.of_isColimit'`, states that for any category `C` and given objects `Z`, `X`, `Y`, `P` in `C`, together with morphisms `f : Z ⟶ X`, `g : Z ⟶ Y`, `inl : X ⟶ P`, and `inr : Y ⟶ P` such that a commutative square exists between them, if this configuration (as a cocone) is a colimit in the categorical sense, then it forms a pushout in the category `C`.
In other words, if you have a commutative square with the aforementioned properties and the cocone of this square is a colimit, then you can apply this theorem to assert that the given configuration is indeed a pushout in the category. This version of `of_isColimit` theorem is more conveniently used with the `apply` tactic in Lean.
More concisely: If in a commutative square in a category with a colimit at the object above, the cocone is the colimit, then the configuration forms a pushout.
|
CategoryTheory.IsPullback.of_isLimit
theorem CategoryTheory.IsPullback.of_isLimit :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
{c : CategoryTheory.Limits.PullbackCone f g},
CategoryTheory.Limits.IsLimit c → CategoryTheory.IsPullback c.fst c.snd f g
This theorem states that if `c` is a limiting pullback cone in a category `C` over objects `X`, `Y`, and `Z` with morphisms `f: X ⟶ Z` and `g: Y ⟶ Z`, then the pair of morphisms `(CategoryTheory.Limits.PullbackCone.fst c, CategoryTheory.Limits.PullbackCone.snd c)` forms a pullback for `f` and `g`. In other words, if the cone `c` is a limit of the cospan formed by `f` and `g`, then the first and second projections of this cone provide a pullback of `f` and `g`.
More concisely: If `c` is a limiting pullback cone in a category `C` over objects `X`, `Y`, and `Z` with morphisms `f: X ⟶ Z` and `g: Y ⟶ Z`, then the pair of morphisms `(fst c, snd c)` forms a pullback of `f` and `g`.
|
CategoryTheory.IsPushout.zero_bot
theorem CategoryTheory.IsPushout.zero_bot :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id X) 0 0 0
This theorem states that for any category `C` that has a zero object and zero morphisms, and for any object `X` in `C`, the square constructed with `0 : 0 ⟶ 0` at the bottom and the identity morphism on `X` at the top is a pushout square. In the context of category theory, a pushout is a kind of limit, which captures the idea of the "smallest" object that can be "pasted" onto two given morphisms in a way that commutes with them. In this specific case, the theorem is saying that the object we get by "pasting" along the zero morphism and the identity on `X` is in fact a pushout.
More concisely: In any category with a zero object and zero morphisms, the square formed by the zero morphism at the bottom and the identity morphism on an object X is a pushout square.
|
CategoryTheory.IsPushout.map
theorem CategoryTheory.IsPushout.map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X}
{g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
[inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F],
CategoryTheory.IsPushout f g h i → CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
The theorem `CategoryTheory.IsPushout.map` states that for any two categories `C` and `D`, a functor `F` from `C` to `D`, four objects `W`, `X`, `Y`, `Z` in `C`, morphisms `f: W ⟶ X`, `g: W ⟶ Y`, `h: X ⟶ Z`, and `i: Y ⟶ Z` in `C`, if `F` preserves the colimit of the span of `f` and `g`, and if `f`, `g`, `h`, `i` form a pushout in `C`, then the morphisms `F.map f`, `F.map g`, `F.map h`, and `F.map i` also form a pushout in `D`. In simpler terms, it says that under certain conditions, the pushout structure is preserved under the functor `F`.
More concisely: If functor `F` preserves colimits of spans and `(f, g, h, i)` is a pushout in category `C`, then `(F.map f, F.map g, F.map h, F.map i)` is a pushout in category `D`.
|
CategoryTheory.IsPushout.isColimit'
theorem CategoryTheory.IsPushout.isColimit' :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
{inr : Y ⟶ P} (self : CategoryTheory.IsPushout f g inl inr),
Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯))
This theorem states that for any Category `C` and objects `Z`, `X`, `Y`, `P` in `C`, given morphisms `f : Z ⟶ X`, `g : Z ⟶ Y`, `inl : X ⟶ P`, and `inr : Y ⟶ P`, if these form a pushout (as specified by the `CategoryTheory.IsPushout f g inl inr` condition), then there exists a colimit for the pushout cocone created by `inl` and `inr`. That is, in the language of category theory, the pushout cocone is a special kind of diagram for which a certain universal limiting condition is satisfied.
More concisely: Given any category `C` and objects `Z`, `X`, `Y`, `P`, morphisms `f : Z ⟶ X`, `g : Z ⟶ Y`, and `inl : X ⟶ P`, `inr : Y ⟶ P` forming a pushout, there exists a colimit for the pushout cocone `{inl, inr, Z �� Taylor, f, g}`.
|
CategoryTheory.IsPullback.of_horiz_isIso
theorem CategoryTheory.IsPullback.of_horiz_isIso :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
{g : Y ⟶ Z} [inst_1 : CategoryTheory.IsIso fst] [inst_2 : CategoryTheory.IsIso g],
CategoryTheory.CommSq fst snd f g → CategoryTheory.IsPullback fst snd f g
This theorem states that in any category `C`, given objects `P`, `X`, `Y`, and `Z`, and morphisms `fst: P -> X`, `snd: P -> Y`, `f: X -> Z`, and `g: Y -> Z`, if `fst` and `g` are isomorphisms and the diagram formed by these morphisms is a commutative square, then the square is a pullback square. In the language of category theory, a pullback square is a way of defining the product of two morphisms in a category, and commutative squares are diagrams in which all paths through the diagram result in the same morphism when composed.
More concisely: In any category, if the diagonal morphisms and two given morphisms form a commutative square and are isomorphisms, then the square is a pullback square.
|
CategoryTheory.IsPushout.zero_top
theorem CategoryTheory.IsPushout.zero_top :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
[inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
CategoryTheory.IsPushout 0 0 0 (CategoryTheory.CategoryStruct.id X)
The theorem `CategoryTheory.IsPushout.zero_top` states that in any category `C` (which is assumed to have a zero object and zero morphisms), for any object `X` in `C`, the square with `0 : 0 ⟶ 0` as the top morphism and the identity morphism on `X` as the bottom morphism is a pushout square. In the context of category theory, a pushout is a universal construction which encapsulates the idea of "gluing" of objects along a common part. In this case, the "gluing" is performed along the zero morphism and the identity morphism.
More concisely: In any category with a zero object, the square with the zero morphism as the top and the identity morphism as the bottom forms a pushout.
|
CategoryTheory.IsPullback.of_hasPullback
theorem CategoryTheory.IsPullback.of_hasPullback :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
[inst_1 : CategoryTheory.Limits.HasPullback f g],
CategoryTheory.IsPullback CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd f g
This theorem states that in the context of a category `C`, for any three objects `X`, `Y`, `Z` in `C` and two morphisms `f` from `X` to `Z` and `g` from `Y` to `Z`, if the pullback of `f` and `g` exists (i.e., `HasPullback f g` holds), then the pullback object along with the two projection morphisms (given by `pullback.fst` and `pullback.snd`) forms an "IsPullback" square. In other words, the pullback structure provided by `HasPullback f g` satisfies the universal property of the pullback.
More concisely: Given any morphisms `f: X -> Z` and `g: Y -> Z` in a category `C` with a pullback `(PB, p_X, p_Y)` at `Z`, the pullback `PB` is the unique object `B` and morphisms `p_X: X -> B` and `p_Y: Y -> B` such that for all objects `A` and morphisms `h: A -> X` and `k: A -> Y`, if `f . h = g . k`, then there exists a unique morphism `i: A -> B` with `h = p_X . i` and `k = p_Y . i`.
|