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 #

@[reducible, inline]

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

Equations
Instances For
    @[reducible, match_pattern, inline]

    The central point of the walking cospan.

    Equations
    Instances For
      @[reducible, inline]

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

      Equations
      Instances For
        @[reducible, match_pattern, inline]

        The central point of the walking span.

        Equations
        Instances For
          @[reducible, inline]

          The type of arrows for the diagram indexing a pullback.

          Equations
          Instances For
            @[reducible, match_pattern, inline]

            The identity arrows of the walking cospan.

            Equations
            Instances For
              @[reducible, inline]

              The type of arrows for the diagram indexing a pushout.

              Equations
              Instances For
                @[reducible, match_pattern, inline]

                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
                            def CategoryTheory.Limits.spanCompIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) :

                            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) :
                                  @[reducible, inline]
                                  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
                                    @[reducible, inline]
                                    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
                                      @[reducible, inline]
                                      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
                                        def CategoryTheory.Limits.PullbackCone.isLimitAux {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) (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt t.pt) (fac_left : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp (lift s) t.fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp (lift s) t.snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt t.pt), (∀ (j : CategoryTheory.Limits.WalkingCospan), CategoryTheory.CategoryStruct.comp m (t.app j) = s.app j)m = lift s) :

                                        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
                                        • t.isLimitAux lift fac_left fac_right uniq = { lift := lift, fac := , uniq := uniq }
                                        Instances For
                                          def CategoryTheory.Limits.PullbackCone.isLimitAux' {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) (create : (s : CategoryTheory.Limits.PullbackCone f g) → { l : s.pt t.pt // CategoryTheory.CategoryStruct.comp l t.fst = s.fst CategoryTheory.CategoryStruct.comp l t.snd = s.snd ∀ {m : s.pt t.pt}, CategoryTheory.CategoryStruct.comp m t.fst = s.fstCategoryTheory.CategoryStruct.comp m t.snd = s.sndm = l }) :

                                          This is another 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, and allows access to the same s for all parts.

                                          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
                                              @[simp]
                                              theorem CategoryTheory.Limits.PullbackCone.mk_fst {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) :
                                              @[simp]
                                              theorem CategoryTheory.Limits.PullbackCone.mk_snd {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) :

                                              To check whether a morphism is equalized by the maps of a pullback cone, it suffices to check it for fst t and snd t

                                              def CategoryTheory.Limits.PullbackCone.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} {s : CategoryTheory.Limits.PullbackCone f g} {t : CategoryTheory.Limits.PullbackCone f g} (i : s.pt t.pt) (w₁ : s.fst = CategoryTheory.CategoryStruct.comp i.hom t.fst) (w₂ : s.snd = CategoryTheory.CategoryStruct.comp i.hom t.snd) :
                                              s t

                                              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
                                                    def CategoryTheory.Limits.PullbackCone.IsLimit.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) (lift : (s : CategoryTheory.Limits.PullbackCone f g) → s.pt W) (fac_left : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.PullbackCone f g), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.PullbackCone f g) (m : s.pt W), CategoryTheory.CategoryStruct.comp m fst = s.fstCategoryTheory.CategoryStruct.comp m snd = s.sndm = lift s) :

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

                                                    Equations
                                                    Instances For

                                                      The pullback cone obtained by flipping fst and snd.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem CategoryTheory.Limits.PullbackCone.flip_pt {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.flip.pt = t.pt
                                                        @[simp]
                                                        theorem CategoryTheory.Limits.PullbackCone.flip_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.flip.fst = t.snd
                                                        @[simp]
                                                        theorem CategoryTheory.Limits.PullbackCone.flip_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.flip.snd = t.fst
                                                        def CategoryTheory.Limits.PullbackCone.flipFlipIso {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.flip.flip t

                                                        Flipping a pullback cone twice gives an isomorphic cone.

                                                        Equations
                                                        Instances For

                                                          The flip of a pullback square is a pullback square.

                                                          Equations
                                                          Instances For

                                                            A square is a pullback square if its flip is.

                                                            Equations
                                                            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
                                                              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
                                                                    @[reducible, inline]
                                                                    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
                                                                      @[reducible, inline]
                                                                      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
                                                                        @[reducible, inline]
                                                                        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
                                                                          def CategoryTheory.Limits.PushoutCocone.isColimitAux {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) (desc : (s : CategoryTheory.Limits.PushoutCocone f g) → t.pt s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp t.inl (desc s) = s.inl) (fac_right : ∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp t.inr (desc s) = s.inr) (uniq : ∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : t.pt s.pt), (∀ (j : CategoryTheory.Limits.WalkingSpan), CategoryTheory.CategoryStruct.comp (t.app j) m = s.app j)m = desc s) :

                                                                          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
                                                                          • t.isColimitAux desc fac_left fac_right uniq = { desc := desc, fac := , uniq := uniq }
                                                                          Instances For

                                                                            This is another 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, and allows access to the same s for all parts.

                                                                            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
                                                                                @[simp]
                                                                                theorem CategoryTheory.Limits.PushoutCocone.mk_inl {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) :
                                                                                @[simp]
                                                                                theorem CategoryTheory.Limits.PushoutCocone.mk_inr {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) :

                                                                                To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check it for inl t and inr t

                                                                                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
                                                                                    def CategoryTheory.Limits.PushoutCocone.ext {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} {s : CategoryTheory.Limits.PushoutCocone f g} {t : CategoryTheory.Limits.PushoutCocone f g} (i : s.pt t.pt) (w₁ : CategoryTheory.CategoryStruct.comp s.inl i.hom = t.inl) (w₂ : CategoryTheory.CategoryStruct.comp s.inr i.hom = t.inr) :
                                                                                    s t

                                                                                    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
                                                                                      def CategoryTheory.Limits.PushoutCocone.IsColimit.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) (desc : (s : CategoryTheory.Limits.PushoutCocone f g) → W s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : CategoryTheory.Limits.PushoutCocone f g), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : CategoryTheory.Limits.PushoutCocone f g) (m : W s.pt), CategoryTheory.CategoryStruct.comp inl m = s.inlCategoryTheory.CategoryStruct.comp inr m = s.inrm = desc s) :

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

                                                                                      Equations
                                                                                      Instances For

                                                                                        The pushout cocone obtained by flipping inl and inr.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.Limits.PushoutCocone.flip_pt {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) :
                                                                                          t.flip.pt = t.pt
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.Limits.PushoutCocone.flip_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) :
                                                                                          t.flip.inl = t.inr
                                                                                          @[simp]
                                                                                          theorem CategoryTheory.Limits.PushoutCocone.flip_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) :
                                                                                          t.flip.inr = t.inl
                                                                                          def CategoryTheory.Limits.PushoutCocone.flipFlipIso {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) :
                                                                                          t.flip.flip t

                                                                                          Flipping a pushout cocone twice gives an isomorphic cocone.

                                                                                          Equations
                                                                                          Instances For

                                                                                            The flip of a pushout square is a pushout square.

                                                                                            Equations
                                                                                            Instances For

                                                                                              A square is a pushout square if its flip is.

                                                                                              Equations
                                                                                              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
                                                                                                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.

                                                                                                  def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} (f : X Y) (g : X Z) (h : X W) [CategoryTheory.Epi h] (x : W Y) (y : W Z) (hhx : CategoryTheory.CategoryStruct.comp h x = f) (hhy : CategoryTheory.CategoryStruct.comp h y = g) (s : CategoryTheory.Limits.PushoutCocone f g) (hs : CategoryTheory.Limits.IsColimit s) :
                                                                                                  let_fun reassoc₁ := ; let_fun reassoc₂ := ; CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk s.inl s.inr )

                                                                                                  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
                                                                                                          @[reducible, inline]
                                                                                                          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
                                                                                                            @[reducible, inline]
                                                                                                            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
                                                                                                              @[reducible, inline]
                                                                                                              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
                                                                                                                @[reducible, inline]
                                                                                                                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
                                                                                                                  @[reducible, inline]

                                                                                                                  The first projection of the pullback of f and g.

                                                                                                                  Equations
                                                                                                                  Instances For
                                                                                                                    @[reducible, inline]

                                                                                                                    The second projection of the pullback of f and g.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      @[reducible, inline]

                                                                                                                      The first inclusion into the pushout of f and g.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        @[reducible, inline]

                                                                                                                        The second inclusion into the pushout of f and g.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[reducible, inline]

                                                                                                                          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
                                                                                                                            @[reducible, inline]

                                                                                                                            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
                                                                                                                                  @[reducible, inline]
                                                                                                                                  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
                                                                                                                                    @[reducible, inline]

                                                                                                                                    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
                                                                                                                                      @[reducible, inline]
                                                                                                                                      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
                                                                                                                                        @[reducible, inline]

                                                                                                                                        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