Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullbacks

Pullbacks #

We define a category WalkingCospan (resp. WalkingSpan), which is the index category for the given data for a pullback (resp. pushout) diagram. Convenience methods cospan f g and span f g construct functors from the walking (co)span, hitting the given morphisms.

We define pullback f g and pushout f g as limits and colimits of such functors.

References #

@[inline, reducible]

The type of objects for the diagram indexing a pullback, defined as a special case of WidePullbackShape.

Equations
Instances For
    @[match_pattern, inline, reducible]

    The central point of the walking cospan.

    Equations
    Instances For
      @[inline, reducible]

      The type of objects for the diagram indexing a pushout, defined as a special case of WidePushoutShape.

      Equations
      Instances For
        @[match_pattern, inline, reducible]

        The central point of the walking span.

        Equations
        Instances For
          @[inline, reducible]

          The type of arrows for the diagram indexing a pullback.

          Equations
          Instances For
            @[match_pattern, inline, reducible]

            The identity arrows of the walking cospan.

            Equations
            Instances For
              @[inline, reducible]

              The type of arrows for the diagram indexing a pushout.

              Equations
              Instances For
                @[match_pattern, inline, reducible]

                The identity arrows of the walking span.

                Equations
                Instances For

                  To construct an isomorphism of cones over the walking cospan, it suffices to construct an isomorphism of the cone points and check it commutes with the legs to left and right.

                  Equations
                  Instances For

                    To construct an isomorphism of cocones over the walking span, it suffices to construct an isomorphism of the cocone points and check it commutes with the legs from left and right.

                    Equations
                    Instances For

                      cospan f g is the functor from the walking cospan hitting f and g.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        span f g is the functor from the walking span hitting f and g.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          A functor applied to a cospan is a cospan.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For

                            A functor applied to a span is a span.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              def CategoryTheory.Limits.cospanExt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :

                              Construct an isomorphism of cospans from components.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_hom_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_hom_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_hom_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_inv_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_inv_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                @[simp]
                                theorem CategoryTheory.Limits.cospanExt_inv_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Z} {g : Y Z} {f' : X' Z'} {g' : Y' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom) (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                def CategoryTheory.Limits.spanExt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :

                                Construct an isomorphism of spans from components.

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_app_one {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_hom_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_hom_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_hom_app_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_inv_app_left {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_inv_app_right {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[simp]
                                  theorem CategoryTheory.Limits.spanExt_inv_app_zero {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {X' : C} {Y' : C} {Z' : C} (iX : X X') (iY : Y Y') (iZ : Z Z') {f : X Y} {g : X Z} {f' : X' Y'} {g' : X' Z'} (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom) (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom) :
                                  @[inline, reducible]
                                  abbrev CategoryTheory.Limits.PullbackCone {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :
                                  Type (max u v)

                                  A pullback cone is just a cone on the cospan formed by two morphisms f : X ⟶ Z and g : Y ⟶ Z.

                                  Equations
                                  Instances For
                                    @[inline, reducible]
                                    abbrev CategoryTheory.Limits.PullbackCone.fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (t : CategoryTheory.Limits.PullbackCone f g) :
                                    t.pt X

                                    The first projection of a pullback cone.

                                    Equations
                                    Instances For
                                      @[inline, reducible]
                                      abbrev CategoryTheory.Limits.PullbackCone.snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (t : CategoryTheory.Limits.PullbackCone f g) :
                                      t.pt Y

                                      The second projection of a pullback cone.

                                      Equations
                                      Instances For

                                        This is a slightly more convenient method to verify that a pullback cone is a limit cone. It only asks for a proof of facts that carry any mathematical content

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem CategoryTheory.Limits.PullbackCone.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g) :
                                          def CategoryTheory.Limits.PullbackCone.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {W : C} (fst : W X) (snd : W Y) (eq : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g) :

                                          A pullback cone on f and g is determined by morphisms fst : W ⟶ X and snd : W ⟶ Y such that fst ≫ f = snd ≫ g.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            To construct an isomorphism of pullback cones, it suffices to construct an isomorphism of the cone points and check it commutes with fst and snd.

                                            Equations
                                            Instances For

                                              If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that h ≫ f = k ≫ g, then we get l : W ⟶ t.pt, which satisfies l ≫ fst t = h and l ≫ snd t = k, see IsLimit.lift_fst and IsLimit.lift_snd.

                                              Equations
                                              Instances For

                                                If t is a limit pullback cone over f and g and h : W ⟶ X and k : W ⟶ Y are such that h ≫ f = k ≫ g, then we have l : W ⟶ t.pt satisfying l ≫ fst t = h and l ≫ snd t = k.

                                                Equations
                                                Instances For

                                                  This is a more convenient formulation to show that a PullbackCone constructed using PullbackCone.mk is a limit cone.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For

                                                    Flipping a pullback cone twice gives an isomorphic cone.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For

                                                      The flip of a pullback square is a pullback square.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For

                                                        A square is a pullback square if its flip is.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For

                                                          The pullback cone (𝟙 X, 𝟙 X) for the pair (f, f) is a limit if f is a mono. The converse is shown in mono_of_pullback_is_id.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For

                                                            f is a mono if the pullback cone (𝟙 X, 𝟙 X) is a limit for the pair (f, f). The converse is given in PullbackCone.is_id_of_mono.

                                                            Suppose f and g are two morphisms with a common codomain and s is a limit cone over the diagram formed by f and g. Suppose f and g both factor through a monomorphism h via x and y, respectively. Then s is also a limit cone over the diagram formed by x and y.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For

                                                              If W is the pullback of f, g, it is also the pullback of f ≫ i, g ≫ i for any mono i.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[inline, reducible]
                                                                abbrev CategoryTheory.Limits.PushoutCocone {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :
                                                                Type (max u v)

                                                                A pushout cocone is just a cocone on the span formed by two morphisms f : X ⟶ Y and g : X ⟶ Z.

                                                                Equations
                                                                Instances For
                                                                  @[inline, reducible]
                                                                  abbrev CategoryTheory.Limits.PushoutCocone.inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (t : CategoryTheory.Limits.PushoutCocone f g) :
                                                                  Y t.pt

                                                                  The first inclusion of a pushout cocone.

                                                                  Equations
                                                                  Instances For
                                                                    @[inline, reducible]
                                                                    abbrev CategoryTheory.Limits.PushoutCocone.inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (t : CategoryTheory.Limits.PushoutCocone f g) :
                                                                    Z t.pt

                                                                    The second inclusion of a pushout cocone.

                                                                    Equations
                                                                    Instances For

                                                                      This is a slightly more convenient method to verify that a pushout cocone is a colimit cocone. It only asks for a proof of facts that carry any mathematical content

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem CategoryTheory.Limits.PushoutCocone.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr) :
                                                                        def CategoryTheory.Limits.PushoutCocone.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} {W : C} (inl : Y W) (inr : Z W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr) :

                                                                        A pushout cocone on f and g is determined by morphisms inl : Y ⟶ W and inr : Z ⟶ W such that f ≫ inl = g ↠ inr.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For

                                                                          If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.pt ⟶ W such that inl t ≫ l = h and inr t ≫ l = k, see IsColimit.inl_desc and IsColimit.inr_desc

                                                                          Equations
                                                                          Instances For

                                                                            If t is a colimit pushout cocone over f and g and h : Y ⟶ W and k : Z ⟶ W are morphisms satisfying f ≫ h = g ≫ k, then we have a factorization l : t.pt ⟶ W such that inl t ≫ l = h and inr t ≫ l = k.

                                                                            Equations
                                                                            Instances For

                                                                              To construct an isomorphism of pushout cocones, it suffices to construct an isomorphism of the cocone points and check it commutes with inl and inr.

                                                                              Equations
                                                                              Instances For

                                                                                This is a more convenient formulation to show that a PushoutCocone constructed using PushoutCocone.mk is a colimit cocone.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  Flipping a pushout cocone twice gives an isomorphic cocone.

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    The flip of a pushout square is a pushout square.

                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      A square is a pushout square if its flip is.

                                                                                      Equations
                                                                                      • One or more equations did not get rendered due to their size.
                                                                                      Instances For

                                                                                        The pushout cocone (𝟙 X, 𝟙 X) for the pair (f, f) is a colimit if f is an epi. The converse is shown in epi_of_isColimit_mk_id_id.

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For

                                                                                          f is an epi if the pushout cocone (𝟙 X, 𝟙 X) is a colimit for the pair (f, f). The converse is given in PushoutCocone.isColimitMkIdId.

                                                                                          Suppose f and g are two morphisms with a common domain and s is a colimit cocone over the diagram formed by f and g. Suppose f and g both factor through an epimorphism h via x and y, respectively. Then s is also a colimit cocone over the diagram formed by x and y.

                                                                                          Equations
                                                                                          • One or more equations did not get rendered due to their size.
                                                                                          Instances For

                                                                                            If W is the pushout of f, g, it is also the pushout of h ≫ f, h ≫ g for any epi h.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For

                                                                                              This is a helper construction that can be useful when verifying that a category has all pullbacks. Given F : WalkingCospan ⥤ C, which is really the same as cospan (F.map inl) (F.map inr), and a pullback cone on F.map inl and F.map inr, we get a cone on F.

                                                                                              If you're thinking about using this, have a look at hasPullbacks_of_hasLimit_cospan, which you may find to be an easier way of achieving your goal.

                                                                                              Equations
                                                                                              Instances For

                                                                                                This is a helper construction that can be useful when verifying that a category has all pushout. Given F : WalkingSpan ⥤ C, which is really the same as span (F.map fst) (F.map snd), and a pushout cocone on F.map fst and F.map snd, we get a cocone on F.

                                                                                                If you're thinking about using this, have a look at hasPushouts_of_hasColimit_span, which you may find to be an easier way of achieving your goal.

                                                                                                Equations
                                                                                                Instances For
                                                                                                  @[inline, reducible]
                                                                                                  abbrev CategoryTheory.Limits.HasPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) :

                                                                                                  HasPullback f g represents a particular choice of limiting cone for the pair of morphisms f : X ⟶ Z and g : Y ⟶ Z.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    @[inline, reducible]
                                                                                                    abbrev CategoryTheory.Limits.HasPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :

                                                                                                    HasPushout f g represents a particular choice of colimiting cocone for the pair of morphisms f : X ⟶ Y and g : X ⟶ Z.

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      @[inline, reducible]
                                                                                                      abbrev CategoryTheory.Limits.pullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                      C

                                                                                                      pullback f g computes the pullback of a pair of morphisms with the same target.

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        @[inline, reducible]
                                                                                                        abbrev CategoryTheory.Limits.pushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                        C

                                                                                                        pushout f g computes the pushout of a pair of morphisms with the same source.

                                                                                                        Equations
                                                                                                        Instances For
                                                                                                          @[inline, reducible]

                                                                                                          The first projection of the pullback of f and g.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[inline, reducible]

                                                                                                            The second projection of the pullback of f and g.

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              @[inline, reducible]

                                                                                                              The first inclusion into the pushout of f and g.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[inline, reducible]

                                                                                                                The second inclusion into the pushout of f and g.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[inline, reducible]

                                                                                                                  A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism pullback.lift : W ⟶ pullback f g.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[inline, reducible]

                                                                                                                    A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism pushout.desc : pushout f g ⟶ W.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      def CategoryTheory.Limits.pullback.lift' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback f g] (h : W X) (k : W Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) :
                                                                                                                      { l : W CategoryTheory.Limits.pullback f g // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.fst = h CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd = k }

                                                                                                                      A pair of morphisms h : W ⟶ X and k : W ⟶ Y satisfying h ≫ f = k ≫ g induces a morphism l : W ⟶ pullback f g such that l ≫ pullback.fst = h and l ≫ pullback.snd = k.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def CategoryTheory.Limits.pullback.desc' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout f g] (h : Y W) (k : Z W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) :
                                                                                                                        { l : CategoryTheory.Limits.pushout f g W // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl l = h CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr l = k }

                                                                                                                        A pair of morphisms h : Y ⟶ W and k : Z ⟶ W satisfying f ≫ h = g ≫ k induces a morphism l : pushout f g ⟶ W such that pushout.inl ≫ l = h and pushout.inr ≫ l = k.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          theorem CategoryTheory.Limits.pullback.condition_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z✝} {g : Y Z✝} [CategoryTheory.Limits.HasPullback f g] {Z : C} (h : Z✝ Z) :
                                                                                                                          theorem CategoryTheory.Limits.pullback.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd g
                                                                                                                          theorem CategoryTheory.Limits.pushout.condition {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                          CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.pushout.inl = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.pushout.inr
                                                                                                                          @[inline, reducible]
                                                                                                                          abbrev CategoryTheory.Limits.pullback.map {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {S : C} {T : C} (f₁ : W S) (f₂ : X S) [CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) :

                                                                                                                          Given such a diagram, then there is a natural morphism W ×ₛ X ⟶ Y ×ₜ Z.

                                                                                                                          W ⟶ Y ↘ ↘ S ⟶ T ↗ ↗ X ⟶ Z

                                                                                                                          Equations
                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                          Instances For
                                                                                                                            @[inline, reducible]

                                                                                                                            The canonical map X ×ₛ Y ⟶ X ×ₜ Y given S ⟶ T.

                                                                                                                            Equations
                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                            Instances For
                                                                                                                              @[inline, reducible]
                                                                                                                              abbrev CategoryTheory.Limits.pushout.map {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {S : C} {T : C} (f₁ : S W) (f₂ : S X) [CategoryTheory.Limits.HasPushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [CategoryTheory.Limits.HasPushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂) :

                                                                                                                              Given such a diagram, then there is a natural morphism W ⨿ₛ X ⟶ Y ⨿ₜ Z.

                                                                                                                              W ⟶ Y
                                                                                                                              

                                                                                                                              ↗ ↗ S ⟶ T ↘ ↘ X ⟶ Z

                                                                                                                              Equations
                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                              Instances For
                                                                                                                                @[inline, reducible]

                                                                                                                                The canonical map X ⨿ₛ Y ⟶ X ⨿ₜ Y given S ⟶ T.

                                                                                                                                Equations
                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                Instances For
                                                                                                                                  theorem CategoryTheory.Limits.pullback.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback f g] {W : C} {k : W CategoryTheory.Limits.pullback f g} {l : W CategoryTheory.Limits.pullback f g} (h₀ : CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.fst) (h₁ : CategoryTheory.CategoryStruct.comp k CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.pullback.snd) :
                                                                                                                                  k = l

                                                                                                                                  Two morphisms into a pullback are equal if their compositions with the pullback morphisms are equal

                                                                                                                                  def CategoryTheory.Limits.pullbackIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd )

                                                                                                                                  The pullback cone built from the pullback projections is a pullback.

                                                                                                                                  Equations
                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                  Instances For
                                                                                                                                    instance CategoryTheory.Limits.pullback.fst_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Mono g] :
                                                                                                                                    CategoryTheory.Mono CategoryTheory.Limits.pullback.fst

                                                                                                                                    The pullback of a monomorphism is a monomorphism

                                                                                                                                    Equations
                                                                                                                                    • =
                                                                                                                                    instance CategoryTheory.Limits.pullback.snd_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Mono f] :
                                                                                                                                    CategoryTheory.Mono CategoryTheory.Limits.pullback.snd

                                                                                                                                    The pullback of a monomorphism is a monomorphism

                                                                                                                                    Equations
                                                                                                                                    • =
                                                                                                                                    instance CategoryTheory.Limits.mono_pullback_to_prod {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasBinaryProduct X Y] :
                                                                                                                                    CategoryTheory.Mono (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd)

                                                                                                                                    The map X ×[Z] Y ⟶ X × Y is mono.

                                                                                                                                    Equations
                                                                                                                                    • =
                                                                                                                                    theorem CategoryTheory.Limits.pushout.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout f g] {W : C} {k : CategoryTheory.Limits.pushout f g W} {l : CategoryTheory.Limits.pushout f g W} (h₀ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl k = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl l) (h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr k = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr l) :
                                                                                                                                    k = l

                                                                                                                                    Two morphisms out of a pushout are equal if their compositions with the pushout morphisms are equal

                                                                                                                                    def CategoryTheory.Limits.pushoutIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr )

                                                                                                                                    The pushout cocone built from the pushout coprojections is a pushout.

                                                                                                                                    Equations
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      instance CategoryTheory.Limits.pushout.inl_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Epi g] :
                                                                                                                                      CategoryTheory.Epi CategoryTheory.Limits.pushout.inl

                                                                                                                                      The pushout of an epimorphism is an epimorphism

                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      instance CategoryTheory.Limits.pushout.inr_of_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Epi f] :
                                                                                                                                      CategoryTheory.Epi CategoryTheory.Limits.pushout.inr

                                                                                                                                      The pushout of an epimorphism is an epimorphism

                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      instance CategoryTheory.Limits.epi_coprod_to_pushout {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasBinaryCoproduct Y Z] :
                                                                                                                                      CategoryTheory.Epi (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr)

                                                                                                                                      The map X ⨿ Y ⟶ X ⨿[Z] Y is epi.

                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      instance CategoryTheory.Limits.pullback.map_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {S : C} {T : C} (f₁ : W S) (f₂ : X S) [CategoryTheory.Limits.HasPullback f₁ f₂] (g₁ : Y T) (g₂ : Z T) [CategoryTheory.Limits.HasPullback g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₃ = CategoryTheory.CategoryStruct.comp i₁ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₃ = CategoryTheory.CategoryStruct.comp i₂ g₂) [CategoryTheory.IsIso i₁] [CategoryTheory.IsIso i₂] [CategoryTheory.IsIso i₃] :
                                                                                                                                      CategoryTheory.IsIso (CategoryTheory.Limits.pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                                                                                                                                      Equations
                                                                                                                                      • =
                                                                                                                                      @[simp]
                                                                                                                                      theorem CategoryTheory.Limits.pullback.congrHom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Z} {f₂ : X Z} {g₁ : Y Z} {g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPullback f₁ g₁] [CategoryTheory.Limits.HasPullback f₂ g₂] :
                                                                                                                                      def CategoryTheory.Limits.pullback.congrHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Z} {f₂ : X Z} {g₁ : Y Z} {g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPullback f₁ g₁] [CategoryTheory.Limits.HasPullback f₂ g₂] :

                                                                                                                                      If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pullback f₁ g₁ ≅ pullback f₂ g₂

                                                                                                                                      Equations
                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                      Instances For
                                                                                                                                        @[simp]
                                                                                                                                        theorem CategoryTheory.Limits.pullback.congrHom_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Z} {f₂ : X Z} {g₁ : Y Z} {g₂ : Y Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPullback f₁ g₁] [CategoryTheory.Limits.HasPullback f₂ g₂] :
                                                                                                                                        instance CategoryTheory.Limits.pushout.map_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} {S : C} {T : C} (f₁ : S W) (f₂ : S X) [CategoryTheory.Limits.HasPushout f₁ f₂] (g₁ : T Y) (g₂ : T Z) [CategoryTheory.Limits.HasPushout g₁ g₂] (i₁ : W Y) (i₂ : X Z) (i₃ : S T) (eq₁ : CategoryTheory.CategoryStruct.comp f₁ i₁ = CategoryTheory.CategoryStruct.comp i₃ g₁) (eq₂ : CategoryTheory.CategoryStruct.comp f₂ i₂ = CategoryTheory.CategoryStruct.comp i₃ g₂) [CategoryTheory.IsIso i₁] [CategoryTheory.IsIso i₂] [CategoryTheory.IsIso i₃] :
                                                                                                                                        CategoryTheory.IsIso (CategoryTheory.Limits.pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)
                                                                                                                                        Equations
                                                                                                                                        • =
                                                                                                                                        @[simp]
                                                                                                                                        theorem CategoryTheory.Limits.pushout.congrHom_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Y} {f₂ : X Y} {g₁ : X Z} {g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPushout f₁ g₁] [CategoryTheory.Limits.HasPushout f₂ g₂] :
                                                                                                                                        def CategoryTheory.Limits.pushout.congrHom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Y} {f₂ : X Y} {g₁ : X Z} {g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPushout f₁ g₁] [CategoryTheory.Limits.HasPushout f₂ g₂] :

                                                                                                                                        If f₁ = f₂ and g₁ = g₂, we may construct a canonical isomorphism pushout f₁ g₁ ≅ pullback f₂ g₂

                                                                                                                                        Equations
                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem CategoryTheory.Limits.pushout.congrHom_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f₁ : X Y} {f₂ : X Y} {g₁ : X Z} {g₂ : X Z} (h₁ : f₁ = f₂) (h₂ : g₁ = g₂) [CategoryTheory.Limits.HasPushout f₁ g₁] [CategoryTheory.Limits.HasPushout f₂ g₂] :

                                                                                                                                          The comparison morphism for the pullback of f,g. This is an isomorphism iff G preserves the pullback of f,g; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

                                                                                                                                          Equations
                                                                                                                                          Instances For
                                                                                                                                            @[simp]
                                                                                                                                            theorem CategoryTheory.Limits.pullbackComparison_comp_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj X Z) :
                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.fst) h
                                                                                                                                            @[simp]
                                                                                                                                            theorem CategoryTheory.Limits.pullbackComparison_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) CategoryTheory.Limits.pullback.fst = G.map CategoryTheory.Limits.pullback.fst
                                                                                                                                            @[simp]
                                                                                                                                            theorem CategoryTheory.Limits.pullbackComparison_comp_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] {Z : D} (h : G.obj Y Z) :
                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp (G.map CategoryTheory.Limits.pullback.snd) h
                                                                                                                                            @[simp]
                                                                                                                                            theorem CategoryTheory.Limits.pullbackComparison_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (G.map f) (G.map g)] :
                                                                                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g) CategoryTheory.Limits.pullback.snd = G.map CategoryTheory.Limits.pullback.snd

                                                                                                                                            The comparison morphism for the pushout of f,g. This is an isomorphism iff G preserves the pushout of f,g; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[simp]
                                                                                                                                              theorem CategoryTheory.Limits.inl_comp_pushoutComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inl
                                                                                                                                              @[simp]
                                                                                                                                              theorem CategoryTheory.Limits.inr_comp_pushoutComparison {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} {Z : C} (G : CategoryTheory.Functor C D) (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout (G.map f) (G.map g)] :
                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutComparison G f g) = G.map CategoryTheory.Limits.pushout.inr

                                                                                                                                              Making this a global instance would make the typeclass search go in an infinite loop.

                                                                                                                                              The isomorphism X ×[Z] Y ≅ Y ×[Z] X.

                                                                                                                                              Equations
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] {Z : C} (h : Y Z) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] {Z : C} (h : X Z) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).hom CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pullback.fst
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] {Z : C} (h : X Z) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) [CategoryTheory.Limits.HasPullback f g] {Z : C} (h : Y Z) :
                                                                                                                                                @[simp]
                                                                                                                                                theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                                CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f g).inv CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pullback.fst

                                                                                                                                                Making this a global instance would make the typeclass search go in an infinite loop.

                                                                                                                                                The isomorphism Y ⨿[X] Z ≅ Z ⨿[X] Y.

                                                                                                                                                Equations
                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                Instances For
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                                  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inr
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                                  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutSymmetry f g).hom = CategoryTheory.Limits.pushout.inl
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                                  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inr
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                                  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutSymmetry f g).inv = CategoryTheory.Limits.pushout.inl
                                                                                                                                                  noncomputable def CategoryTheory.Limits.pullbackIsPullbackOfCompMono {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X W) (g : Y W) (i : W Z) [CategoryTheory.Mono i] [CategoryTheory.Limits.HasPullback f g] :
                                                                                                                                                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd )

                                                                                                                                                  The pullback of f, g is also the pullback of f ≫ i, g ≫ i for any mono i.

                                                                                                                                                  Equations
                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                  Instances For

                                                                                                                                                    Verify that the constructed limit cone is indeed a limit.

                                                                                                                                                    Equations
                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                    Instances For
                                                                                                                                                      instance CategoryTheory.Limits.pullback_snd_iso_of_left_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.IsIso f] :
                                                                                                                                                      CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
                                                                                                                                                      Equations
                                                                                                                                                      • =
                                                                                                                                                      instance CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Z : C} (i : Z W) [CategoryTheory.Mono i] (f : X Z) :
                                                                                                                                                      CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
                                                                                                                                                      Equations
                                                                                                                                                      • =

                                                                                                                                                      Verify that the constructed limit cone is indeed a limit.

                                                                                                                                                      Equations
                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                      Instances For
                                                                                                                                                        instance CategoryTheory.Limits.pullback_snd_iso_of_right_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.IsIso g] :
                                                                                                                                                        CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
                                                                                                                                                        Equations
                                                                                                                                                        • =
                                                                                                                                                        instance CategoryTheory.Limits.pullback_snd_iso_of_left_factors_mono {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Z : C} (i : Z W) [CategoryTheory.Mono i] (f : X Z) :
                                                                                                                                                        CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
                                                                                                                                                        Equations
                                                                                                                                                        • =
                                                                                                                                                        noncomputable def CategoryTheory.Limits.pushoutIsPushoutOfEpiComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : W X) [CategoryTheory.Epi h] [CategoryTheory.Limits.HasPushout f g] :
                                                                                                                                                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr )

                                                                                                                                                        The pushout of f, g is also the pullback of h ≫ f, h ≫ g for any epi h.

                                                                                                                                                        Equations
                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                        Instances For

                                                                                                                                                          Verify that the constructed cocone is indeed a colimit.

                                                                                                                                                          Equations
                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                          Instances For
                                                                                                                                                            instance CategoryTheory.Limits.pushout_inr_iso_of_left_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.IsIso f] :
                                                                                                                                                            CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
                                                                                                                                                            Equations
                                                                                                                                                            • =
                                                                                                                                                            instance CategoryTheory.Limits.pushout_inr_iso_of_right_factors_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} (h : W X) [CategoryTheory.Epi h] (f : X Y) :
                                                                                                                                                            CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
                                                                                                                                                            Equations
                                                                                                                                                            • =

                                                                                                                                                            Verify that the constructed cocone is indeed a colimit.

                                                                                                                                                            Equations
                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                            Instances For
                                                                                                                                                              instance CategoryTheory.Limits.pushout_inl_iso_of_right_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) [CategoryTheory.IsIso g] :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              instance CategoryTheory.Limits.pushout_inl_iso_of_left_factors_epi {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} (h : W X) [CategoryTheory.Epi h] (f : X Y) :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Mono f] :
                                                                                                                                                              CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.snd
                                                                                                                                                              instance CategoryTheory.Limits.fst_iso_of_mono_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Mono f] :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pullback.fst
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              instance CategoryTheory.Limits.snd_iso_of_mono_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Mono f] :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pullback.snd
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Epi f] :
                                                                                                                                                              CategoryTheory.Limits.pushout.inl = CategoryTheory.Limits.pushout.inr
                                                                                                                                                              instance CategoryTheory.Limits.inl_iso_of_epi_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Epi f] :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pushout.inl
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              instance CategoryTheory.Limits.inr_iso_of_epi_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) [CategoryTheory.Epi f] :
                                                                                                                                                              CategoryTheory.IsIso CategoryTheory.Limits.pushout.inr
                                                                                                                                                              Equations
                                                                                                                                                              • =
                                                                                                                                                              def CategoryTheory.Limits.bigSquareIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂)) (H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ f₁ h₁)) :

                                                                                                                                                              Given

                                                                                                                                                              X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

                                                                                                                                                              Then the big square is a pullback if both the small squares are.

                                                                                                                                                              Equations
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                def CategoryTheory.Limits.bigSquareIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₂ i₃ h₂)) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁)) :

                                                                                                                                                                Given

                                                                                                                                                                X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

                                                                                                                                                                Then the big square is a pushout if both the small squares are.

                                                                                                                                                                Equations
                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                Instances For
                                                                                                                                                                  def CategoryTheory.Limits.leftSquareIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₂ f₂ h₂)) (H' : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk i₁ (CategoryTheory.CategoryStruct.comp f₁ f₂) )) :

                                                                                                                                                                  Given

                                                                                                                                                                  X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

                                                                                                                                                                  Then the left square is a pullback if the right square and the big square are.

                                                                                                                                                                  Equations
                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                  Instances For
                                                                                                                                                                    def CategoryTheory.Limits.rightSquareIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} {Y₃ : C} (f₁ : X₁ X₂) (f₂ : X₂ X₃) (g₁ : Y₁ Y₂) (g₂ : Y₂ Y₃) (i₁ : X₁ Y₁) (i₂ : X₂ Y₂) (i₃ : X₃ Y₃) (h₁ : CategoryTheory.CategoryStruct.comp i₁ g₁ = CategoryTheory.CategoryStruct.comp f₁ i₂) (h₂ : CategoryTheory.CategoryStruct.comp i₂ g₂ = CategoryTheory.CategoryStruct.comp f₂ i₃) (H : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk g₁ i₂ h₁)) (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp g₁ g₂) i₃ )) :

                                                                                                                                                                    Given

                                                                                                                                                                    X₁ - f₁ -> X₂ - f₂ -> X₃ | | | i₁ i₂ i₃ ∨ ∨ ∨ Y₁ - g₁ -> Y₂ - g₂ -> Y₃

                                                                                                                                                                    Then the right square is a pushout if the left square and the big square are.

                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For

                                                                                                                                                                      The canonical isomorphism W ×[X] (X ×[Z] Y) ≅ W ×[Z] Y

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : W Z) :
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : Y Z) :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').hom CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : W Z) :
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pullback.fst
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : Y Z) :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z✝) (g : Y Z✝) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] {Z : C} (h : X Z) :
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) (f' : W X) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback f' CategoryTheory.Limits.pullback.fst] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f' f) g] :
                                                                                                                                                                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f'

                                                                                                                                                                        The canonical isomorphism (Y ⨿[X] Z) ⨿[Z] W ≅ Y ×[X] W

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z✝) (g' : Z✝ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' Z) :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (g' : Z W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (g' : Z W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom = CategoryTheory.Limits.pushout.inr
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z✝) (g' : Z✝ W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] {Z : C} (h : CategoryTheory.Limits.pushout CategoryTheory.Limits.pushout.inr g' Z) :
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (g' : Z W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').inv = CategoryTheory.Limits.pushout.inr
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (g' : Z W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.Limits.pushout.inl
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (g' : Z W) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPushout CategoryTheory.Limits.pushout.inr g'] [CategoryTheory.Limits.HasPushout f (CategoryTheory.CategoryStruct.comp g g')] :
                                                                                                                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) = CategoryTheory.CategoryStruct.comp g' CategoryTheory.Limits.pushout.inr
                                                                                                                                                                          def CategoryTheory.Limits.pullbackPullbackLeftIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] :
                                                                                                                                                                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) CategoryTheory.Limits.pullback.snd ) )

                                                                                                                                                                          (X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            def CategoryTheory.Limits.pullbackAssocIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] :
                                                                                                                                                                            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) CategoryTheory.Limits.pullback.snd ) )

                                                                                                                                                                            (X₁ ×[Y₁] X₂) ×[Y₂] X₃ is the pullback X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

                                                                                                                                                                            Equations
                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                            Instances For
                                                                                                                                                                              theorem CategoryTheory.Limits.hasPullback_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] :
                                                                                                                                                                              CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)
                                                                                                                                                                              def CategoryTheory.Limits.pullbackPullbackRightIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ) CategoryTheory.Limits.pullback.snd )

                                                                                                                                                                              X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[X₂] (X₂ ×[Y₂] X₃).

                                                                                                                                                                              Equations
                                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                                              Instances For
                                                                                                                                                                                def CategoryTheory.Limits.pullbackAssocSymmIsPullback {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Limits.pullback.lift CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) ) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) )

                                                                                                                                                                                X₁ ×[Y₁] (X₂ ×[Y₂] X₃) is the pullback (X₁ ×[Y₁] X₂) ×[Y₂] X₃.

                                                                                                                                                                                Equations
                                                                                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                                                                                Instances For
                                                                                                                                                                                  theorem CategoryTheory.Limits.hasPullback_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄
                                                                                                                                                                                  noncomputable def CategoryTheory.Limits.pullbackAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                  CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄ CategoryTheory.Limits.pullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)

                                                                                                                                                                                  The canonical isomorphism (X₁ ×[Y₁] X₂) ×[Y₂] X₃ ≅ X₁ ×[Y₁] (X₂ ×[Y₂] X₃).

                                                                                                                                                                                  Equations
                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                  Instances For
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₁ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst) = CategoryTheory.Limits.pullback.fst
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₁ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom CategoryTheory.Limits.pullback.fst = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.fst
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₂ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₃ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd) = CategoryTheory.Limits.pullback.snd
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₂ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst h)
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst CategoryTheory.Limits.pullback.snd) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.fst
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] {Z : C} (h : X₃ Z) :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd h)
                                                                                                                                                                                    @[simp]
                                                                                                                                                                                    theorem CategoryTheory.Limits.pullbackAssoc_inv_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₁) (f₃ : X₂ Y₂) (f₄ : X₃ Y₂) [CategoryTheory.Limits.HasPullback f₁ f₂] [CategoryTheory.Limits.HasPullback f₃ f₄] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd f₃) f₄] [CategoryTheory.Limits.HasPullback f₁ (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst f₂)] :
                                                                                                                                                                                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv CategoryTheory.Limits.pullback.snd = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.snd CategoryTheory.Limits.pullback.snd
                                                                                                                                                                                    def CategoryTheory.Limits.pushoutPushoutLeftIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] :
                                                                                                                                                                                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl) CategoryTheory.Limits.pushout.inr ) )

                                                                                                                                                                                    (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).

                                                                                                                                                                                    Equations
                                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                                    Instances For
                                                                                                                                                                                      def CategoryTheory.Limits.pushoutAssocIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] :
                                                                                                                                                                                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl) (CategoryTheory.Limits.pushout.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl) CategoryTheory.Limits.pushout.inr ) )

                                                                                                                                                                                      (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ is the pushout X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).

                                                                                                                                                                                      Equations
                                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                                      Instances For
                                                                                                                                                                                        theorem CategoryTheory.Limits.hasPushout_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] :
                                                                                                                                                                                        CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)
                                                                                                                                                                                        def CategoryTheory.Limits.pushoutPushoutRightIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.desc CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr) ) CategoryTheory.Limits.pushout.inr )

                                                                                                                                                                                        X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃).

                                                                                                                                                                                        Equations
                                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          def CategoryTheory.Limits.pushoutAssocSymmIsPushout {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (CategoryTheory.Limits.pushout.desc CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr) ) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inr) )

                                                                                                                                                                                          X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃) is the pushout (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃.

                                                                                                                                                                                          Equations
                                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                                          Instances For
                                                                                                                                                                                            theorem CategoryTheory.Limits.hasPushout_assoc_symm {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                            CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄
                                                                                                                                                                                            noncomputable def CategoryTheory.Limits.pushoutAssoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                            CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)

                                                                                                                                                                                            The canonical isomorphism (X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃ ≅ X₁ ⨿[Z₁] (X₂ ⨿[Z₂] X₃).

                                                                                                                                                                                            Equations
                                                                                                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                                                                                                            Instances For
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.Limits.pushout.inl
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inr
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.Limits.pushout.inr
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl CategoryTheory.Limits.pushout.inl
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄ Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv h)) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl h)
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).inv) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inl
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_pushoutAssoc_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] {Z : C} (h : CategoryTheory.Limits.pushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl) Z) :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr h)
                                                                                                                                                                                              @[simp]
                                                                                                                                                                                              theorem CategoryTheory.Limits.inr_pushoutAssoc_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} {X₃ : C} {Z₁ : C} {Z₂ : C} (g₁ : Z₁ X₁) (g₂ : Z₁ X₂) (g₃ : Z₂ X₂) (g₄ : Z₂ X₃) [CategoryTheory.Limits.HasPushout g₁ g₂] [CategoryTheory.Limits.HasPushout g₃ g₄] [CategoryTheory.Limits.HasPushout (CategoryTheory.CategoryStruct.comp g₃ CategoryTheory.Limits.pushout.inr) g₄] [CategoryTheory.Limits.HasPushout g₁ (CategoryTheory.CategoryStruct.comp g₂ CategoryTheory.Limits.pushout.inl)] :
                                                                                                                                                                                              CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutAssoc g₁ g₂ g₃ g₄).hom = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr CategoryTheory.Limits.pushout.inr
                                                                                                                                                                                              @[inline, reducible]

                                                                                                                                                                                              HasPullbacks represents a choice of pullback for every pair of morphisms

                                                                                                                                                                                              See

                                                                                                                                                                                              Equations
                                                                                                                                                                                              Instances For
                                                                                                                                                                                                @[inline, reducible]

                                                                                                                                                                                                HasPushouts represents a choice of pushout for every pair of morphisms

                                                                                                                                                                                                Equations
                                                                                                                                                                                                Instances For

                                                                                                                                                                                                  If C has all limits of diagrams cospan f g, then it has all pullbacks

                                                                                                                                                                                                  If C has all colimits of diagrams span f g, then it has all pushouts

                                                                                                                                                                                                  Having wide pullback at any universe level implies having binary pullbacks.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • =

                                                                                                                                                                                                  Having wide pushout at any universe level implies having binary pushouts.

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • =
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem CategoryTheory.Limits.baseChange_obj_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} (f : X Y) (g : CategoryTheory.Over Y) :
                                                                                                                                                                                                  ((CategoryTheory.Limits.baseChange f).obj g).hom = CategoryTheory.Limits.pullback.snd

                                                                                                                                                                                                  Given a morphism f : X ⟶ Y, we can take morphisms over Y to morphisms over X via pullbacks. This is right adjoint to over.map (TODO)

                                                                                                                                                                                                  Equations
                                                                                                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                                                                                                  Instances For