Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq

Pullback and pushout squares, and bi-Cartesian squares #

We provide another API for pullbacks and pushouts.

IsPullback fst snd f g is the proposition that

  P --fst--> X
  |          |
 snd         f
  |          |
  v          v
  Y ---g---> Z

is a pullback square.

(And similarly for IsPushout.)

We provide the glue to go back and forth to the usual IsLimit API for pullbacks, and prove IsPullback (pullback.fst f g) (pullback.snd f g) f g for the usual pullback f g provided by the HasLimit API.

We don't attempt to restate everything we know about pullbacks in this language, but do restate the pasting lemmas.

We define bi-Cartesian squares, and show that the pullback and pushout squares for a biproduct are bi-Cartesian.

def CategoryTheory.CommSq.cone {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :

The (not necessarily limiting) PullbackCone h i implicit in the statement that we have CommSq f g h i.

Equations
Instances For
    def CategoryTheory.CommSq.cocone {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :

    The (not necessarily limiting) PushoutCocone f g implicit in the statement that we have CommSq f g h i.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.CommSq.cone_fst {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :
      s.cone.fst = f
      @[simp]
      theorem CategoryTheory.CommSq.cone_snd {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :
      s.cone.snd = g
      @[simp]
      theorem CategoryTheory.CommSq.cocone_inl {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :
      @[simp]
      theorem CategoryTheory.CommSq.cocone_inr {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (s : CommSq f g h i) :
      def CategoryTheory.CommSq.coneOp {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CommSq f g h i) :

      The pushout cocone in the opposite category associated to the cone of a commutative square identifies to the cocone of the flipped commutative square in the opposite category

      Equations
      Instances For
        def CategoryTheory.CommSq.coconeOp {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CommSq f g h i) :

        The pullback cone in the opposite category associated to the cocone of a commutative square identifies to the cone of the flipped commutative square in the opposite category

        Equations
        Instances For
          def CategoryTheory.CommSq.coneUnop {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CommSq f g h i) :

          The pushout cocone obtained from the pullback cone associated to a commutative square in the opposite category identifies to the cocone associated to the flipped square.

          Equations
          Instances For
            def CategoryTheory.CommSq.coconeUnop {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : Cᵒᵖ} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : CommSq f g h i) :

            The pullback cone obtained from the pushout cone associated to a commutative square in the opposite category identifies to the cone associated to the flipped square.

            Equations
            Instances For
              structure CategoryTheory.IsPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} (fst : P X) (snd : P Y) (f : X Z) (g : Y Z) extends CategoryTheory.CommSq fst snd f g :

              The proposition that a square

                P --fst--> X
                |          |
               snd         f
                |          |
                v          v
                Y ---g---> Z
              
              

              is a pullback square. (Also known as a fibered product or Cartesian square.)

              Instances For
                structure CategoryTheory.IsPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} (f : Z X) (g : Z Y) (inl : X P) (inr : Y P) extends CategoryTheory.CommSq f g inl inr :

                The proposition that a square

                  Z ---f---> X
                  |          |
                  g         inl
                  |          |
                  v          v
                  Y --inr--> P
                
                

                is a pushout square. (Also known as a fiber coproduct or co-Cartesian square.)

                Instances For
                  structure CategoryTheory.BicartesianSq {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} (f : W X) (g : W Y) (h : X Z) (i : Y Z) extends CategoryTheory.IsPullback f g h i, CategoryTheory.IsPushout f g h i :

                  A bi-Cartesian square is a commutative square

                    W ---f---> X
                    |          |
                    g          h
                    |          |
                    v          v
                    Y ---i---> Z
                  
                  

                  that is both a pullback square and a pushout square.

                  Instances For

                    We begin by providing some glue between IsPullback and the IsLimit and HasLimit APIs. (And similarly for IsPushout.)

                    def CategoryTheory.IsPullback.cone {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :

                    The (limiting) PullbackCone f g implicit in the statement that we have an IsPullback fst snd f g.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.IsPullback.cone_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :
                      h.cone.fst = fst
                      @[simp]
                      theorem CategoryTheory.IsPullback.cone_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :
                      h.cone.snd = snd
                      noncomputable def CategoryTheory.IsPullback.isLimit {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :

                      The cone obtained from IsPullback fst snd f g is a limit cone.

                      Equations
                      Instances For
                        noncomputable def CategoryTheory.IsPullback.lift {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                        W P

                        API for PullbackCone.IsLimit.lift for IsPullback

                        Equations
                        Instances For
                          @[simp]
                          theorem CategoryTheory.IsPullback.lift_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                          CategoryStruct.comp (hP.lift h k w) fst = h
                          @[simp]
                          theorem CategoryTheory.IsPullback.lift_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : X Z✝) :
                          @[simp]
                          theorem CategoryTheory.IsPullback.lift_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) :
                          CategoryStruct.comp (hP.lift h k w) snd = k
                          @[simp]
                          theorem CategoryTheory.IsPullback.lift_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} (h : W X) (k : W Y) (w : CategoryStruct.comp h f = CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y Z✝) :
                          theorem CategoryTheory.IsPullback.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (hP : IsPullback fst snd f g) {W : C} {k l : W P} (h₀ : CategoryStruct.comp k fst = CategoryStruct.comp l fst) (h₁ : CategoryStruct.comp k snd = CategoryStruct.comp l snd) :
                          k = l
                          theorem CategoryTheory.IsPullback.of_isLimit {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X Z} {g : Y Z} {c : Limits.PullbackCone f g} (h : Limits.IsLimit c) :

                          If c is a limiting pullback cone, then we have an IsPullback c.fst c.snd f g.

                          theorem CategoryTheory.IsPullback.of_isLimit' {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :
                          IsPullback fst snd f g

                          A variant of of_isLimit that is more useful with apply.

                          theorem CategoryTheory.IsPullback.hasPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :

                          The pullback provided by HasPullback f g fits into an IsPullback.

                          If c is a limiting binary product cone, and we have a terminal object, then we have IsPullback c.fst c.snd 0 0 (where each 0 is the unique morphism to the terminal object).

                          theorem CategoryTheory.IsPullback.of_is_product' {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} (h : Limits.IsLimit (Limits.BinaryFan.mk fst snd)) (t : Limits.IsTerminal Z) :
                          IsPullback fst snd (t.from X) (t.from Y)

                          A variant of of_is_product that is more useful with apply.

                          noncomputable def CategoryTheory.IsPullback.isoIsPullback {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
                          P P'

                          Any object at the top left of a pullback square is isomorphic to the object at the top left of any other pullback square with the same cospan.

                          Equations
                          Instances For
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X Z✝) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y Z✝) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X Z✝) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) :
                            @[simp]
                            theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} {P' : C} {fst' : P' X} {snd' : P' Y} (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y Z✝) :
                            noncomputable def CategoryTheory.IsPullback.isoPullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :

                            Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_hom_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_hom_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : X Z✝) :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_hom_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_hom_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : Y Z✝) :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : X Z✝) :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] :
                              @[simp]
                              theorem CategoryTheory.IsPullback.isoPullback_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [Limits.HasPullback f g] {Z✝ : C} (h✝ : Y Z✝) :
                              theorem CategoryTheory.IsPullback.of_iso_pullback {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : CommSq fst snd f g) [Limits.HasPullback f g] (i : P Limits.pullback f g) (w₁ : CategoryStruct.comp i.hom (Limits.pullback.fst f g) = fst) (w₂ : CategoryStruct.comp i.hom (Limits.pullback.snd f g) = snd) :
                              IsPullback fst snd f g
                              theorem CategoryTheory.IsPullback.of_horiz_isIso_mono {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [IsIso fst] [Mono g] (sq : CommSq fst snd f g) :
                              IsPullback fst snd f g
                              theorem CategoryTheory.IsPullback.of_horiz_isIso {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [IsIso fst] [IsIso g] (sq : CommSq fst snd f g) :
                              IsPullback fst snd f g
                              theorem CategoryTheory.IsPullback.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) {P' X' Y' Z' : C} {fst' : P' X'} {snd' : P' Y'} {f' : X' Z'} {g' : Y' Z'} (e₁ : P P') (e₂ : X X') (e₃ : Y Y') (e₄ : Z Z') (commfst : CategoryStruct.comp fst e₂.hom = CategoryStruct.comp e₁.hom fst') (commsnd : CategoryStruct.comp snd e₃.hom = CategoryStruct.comp e₁.hom snd') (commf : CategoryStruct.comp f e₄.hom = CategoryStruct.comp e₂.hom f') (commg : CategoryStruct.comp g e₄.hom = CategoryStruct.comp e₃.hom g') :
                              IsPullback fst' snd' f' g'
                              theorem CategoryTheory.IsPullback.isIso_fst_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {P X Y : C} {fst snd : P X} {f : X Y} [Mono f] (h : IsPullback fst snd f f) :
                              IsIso fst
                              theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono {C : Type u₁} [Category.{v₁, u₁} C] {P X Y : C} {fst snd : P X} {f : X Y} [Mono f] (h : IsPullback fst snd f f) :
                              IsIso snd
                              theorem CategoryTheory.IsPullback.isIso_fst_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [IsIso g] :
                              IsIso fst
                              theorem CategoryTheory.IsPullback.isIso_snd_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) [IsIso f] :
                              IsIso snd
                              def CategoryTheory.IsPushout.cocone {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :

                              The (colimiting) PushoutCocone f g implicit in the statement that we have an IsPushout f g inl inr.

                              Equations
                              Instances For
                                @[simp]
                                theorem CategoryTheory.IsPushout.cocone_inl {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :
                                h.cocone.inl = inl
                                @[simp]
                                theorem CategoryTheory.IsPushout.cocone_inr {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :
                                h.cocone.inr = inr
                                noncomputable def CategoryTheory.IsPushout.isColimit {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :

                                The cocone obtained from IsPushout f g inl inr is a colimit cocone.

                                Equations
                                Instances For
                                  noncomputable def CategoryTheory.IsPushout.desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} (h : X W) (k : Y W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                                  P W

                                  API for PushoutCocone.IsColimit.lift for IsPushout

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.IsPushout.inl_desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} (h : X W) (k : Y W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                                    CategoryStruct.comp inl (hP.desc h k w) = h
                                    @[simp]
                                    theorem CategoryTheory.IsPushout.inl_desc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} (h : X W) (k : Y W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W Z✝) :
                                    @[simp]
                                    theorem CategoryTheory.IsPushout.inr_desc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} (h : X W) (k : Y W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) :
                                    CategoryStruct.comp inr (hP.desc h k w) = k
                                    @[simp]
                                    theorem CategoryTheory.IsPushout.inr_desc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} (h : X W) (k : Y W) (w : CategoryStruct.comp f h = CategoryStruct.comp g k) {Z✝ : C} (h✝ : W Z✝) :
                                    theorem CategoryTheory.IsPushout.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (hP : IsPushout f g inl inr) {W : C} {k l : P W} (h₀ : CategoryStruct.comp inl k = CategoryStruct.comp inl l) (h₁ : CategoryStruct.comp inr k = CategoryStruct.comp inr l) :
                                    k = l
                                    theorem CategoryTheory.IsPushout.of_isColimit {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y : C} {f : Z X} {g : Z Y} {c : Limits.PushoutCocone f g} (h : Limits.IsColimit c) :
                                    IsPushout f g c.inl c.inr

                                    If c is a colimiting pushout cocone, then we have an IsPushout f g c.inl c.inr.

                                    theorem CategoryTheory.IsPushout.of_isColimit' {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :
                                    IsPushout f g inl inr

                                    A variant of of_isColimit that is more useful with apply.

                                    theorem CategoryTheory.IsPushout.hasPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :

                                    The pushout provided by HasPushout f g fits into an IsPushout.

                                    If c is a colimiting binary coproduct cocone, and we have an initial object, then we have IsPushout 0 0 c.inl c.inr (where each 0 is the unique morphism from the initial object).

                                    theorem CategoryTheory.IsPushout.of_is_coproduct' {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {inl : X P} {inr : Y P} (h : Limits.IsColimit (Limits.BinaryCofan.mk inl inr)) (t : Limits.IsInitial Z) :
                                    IsPushout (t.to X) (t.to Y) inl inr

                                    A variant of of_is_coproduct that is more useful with apply.

                                    noncomputable def CategoryTheory.IsPushout.isoIsPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
                                    P P'

                                    Any object at the bottom right of a pushout square is isomorphic to the object at the bottom right of any other pushout square with the same span.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' Z✝) :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' Z✝) :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P Z✝) :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
                                      @[simp]
                                      theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z : C} (X Y : C) {P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} {P' : C} {inl' : X P'} {inr' : Y P'} (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') {Z✝ : C} (h✝ : P Z✝) :
                                      noncomputable def CategoryTheory.IsPushout.isoPushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :

                                      Any object at the top left of a pullback square is isomorphic to the pullback provided by the HasLimit API.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inl_isoPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inl_isoPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : P Z✝) :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inr_isoPushout_inv {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inr_isoPushout_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : P Z✝) :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inl_isoPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inl_isoPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : Limits.pushout f g Z✝) :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inr_isoPushout_hom {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] :
                                        @[simp]
                                        theorem CategoryTheory.IsPushout.inr_isoPushout_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [Limits.HasPushout f g] {Z✝ : C} (h✝ : Limits.pushout f g Z✝) :
                                        theorem CategoryTheory.IsPushout.of_iso_pushout {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : CommSq f g inl inr) [Limits.HasPushout f g] (i : P Limits.pushout f g) (w₁ : CategoryStruct.comp inl i.hom = Limits.pushout.inl f g) (w₂ : CategoryStruct.comp inr i.hom = Limits.pushout.inr f g) :
                                        IsPushout f g inl inr
                                        theorem CategoryTheory.IsPushout.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) {Z' X' Y' P' : C} {f' : Z' X'} {g' : Z' Y'} {inl' : X' P'} {inr' : Y' P'} (e₁ : Z Z') (e₂ : X X') (e₃ : Y Y') (e₄ : P P') (commf : CategoryStruct.comp f e₂.hom = CategoryStruct.comp e₁.hom f') (commg : CategoryStruct.comp g e₃.hom = CategoryStruct.comp e₁.hom g') (comminl : CategoryStruct.comp inl e₄.hom = CategoryStruct.comp e₂.hom inl') (comminr : CategoryStruct.comp inr e₄.hom = CategoryStruct.comp e₃.hom inr') :
                                        IsPushout f' g' inl' inr'
                                        theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {P X Y : C} {inl inr : X P} {f : Y X} [Epi f] (h : IsPushout f f inl inr) :
                                        IsIso inl
                                        theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi {C : Type u₁} [Category.{v₁, u₁} C] {P X Y : C} {inl inr : X P} {f : Y X} [Epi f] (h : IsPushout f f inl inr) :
                                        IsIso inr
                                        theorem CategoryTheory.IsPushout.isIso_inl_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [IsIso g] :
                                        IsIso inl
                                        theorem CategoryTheory.IsPushout.isIso_inr_of_isIso {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) [IsIso f] :
                                        IsIso inr
                                        theorem CategoryTheory.IsPullback.flip {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :
                                        IsPullback snd fst g f
                                        theorem CategoryTheory.IsPullback.flip_iff {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} :
                                        IsPullback fst snd f g IsPullback snd fst g f
                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the left and 𝟙 X on the right is a pullback square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pullback square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pullback square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pullback square.

                                        theorem CategoryTheory.IsPullback.paste_vert {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
                                        IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁

                                        Paste two pullback squares "vertically" to obtain another pullback square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        theorem CategoryTheory.IsPullback.paste_horiz {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
                                        IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)

                                        Paste two pullback squares "horizontally" to obtain another pullback square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        
                                        theorem CategoryTheory.IsPullback.of_bot {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁) (p : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁) (t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
                                        IsPullback h₁₁ v₁₁ v₁₂ h₂₁

                                        Given a pullback square assembled from a commuting square on the top and a pullback square on the bottom, the top square is a pullback square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        theorem CategoryTheory.IsPullback.of_right {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)) (p : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁) (t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
                                        IsPullback h₁₁ v₁₁ v₁₂ h₂₁

                                        Given a pullback square assembled from a commuting square on the left and a pullback square on the right, the left square is a pullback square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        
                                        theorem CategoryTheory.IsPullback.paste_vert_iff {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) (e : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁) :
                                        IsPullback h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁ IsPullback h₁₁ v₁₁ v₁₂ h₂₁
                                        theorem CategoryTheory.IsPullback.paste_horiz_iff {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) (e : CategoryStruct.comp h₁₁ v₁₂ = CategoryStruct.comp v₁₁ h₂₁) :
                                        IsPullback (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂) IsPullback h₁₁ v₁₁ v₁₂ h₂₁
                                        theorem CategoryTheory.IsPullback.of_right' {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {h₁₃ : X₁₁ X₁₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPullback h₁₃ v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)) (t : IsPullback h₁₂ v₁₂ v₁₃ h₂₂) :
                                        IsPullback (t.lift h₁₃ (CategoryStruct.comp v₁₁ h₂₁) ) v₁₁ v₁₂ h₂₁

                                        Variant of IsPullback.of_right where h₁₁ is induced from a morphism h₁₃ : X₁₁ ⟶ X₁₃, and the universal property of the right square.

                                        The objects fit in the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        
                                        theorem CategoryTheory.IsPullback.of_bot' {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₃₁ : X₁₁ X₃₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPullback h₁₁ v₃₁ (CategoryStruct.comp v₁₂ v₂₂) h₃₁) (t : IsPullback h₂₁ v₂₁ v₂₂ h₃₁) :
                                        IsPullback h₁₁ (t.lift (CategoryStruct.comp h₁₁ v₁₂) v₃₁ ) v₁₂ h₂₁

                                        Variant of IsPullback.of_bot, where v₁₁ is induced from a morphism v₃₁ : X₁₁ ⟶ X₃₁, and the universal property of the bottom square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        @[simp]

                                        The square

                                          X --inl--> X ⊞ Y
                                          |            |
                                          0           snd
                                          |            |
                                          v            v
                                          0 ---0-----> Y
                                        

                                        is a pullback square.

                                        @[simp]

                                        The square

                                          Y --inr--> X ⊞ Y
                                          |            |
                                          0           fst
                                          |            |
                                          v            v
                                          0 ---0-----> X
                                        

                                        is a pullback square.

                                        theorem CategoryTheory.IsPullback.op {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :
                                        IsPushout g.op f.op snd.op fst.op
                                        theorem CategoryTheory.IsPullback.unop {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : Cᵒᵖ} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} (h : IsPullback fst snd f g) :
                                        theorem CategoryTheory.IsPullback.of_vert_isIso_mono {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [IsIso snd] [Mono f] (sq : CommSq fst snd f g) :
                                        IsPullback fst snd f g
                                        theorem CategoryTheory.IsPullback.of_vert_isIso {C : Type u₁} [Category.{v₁, u₁} C] {P X Y Z : C} {fst : P X} {snd : P Y} {f : X Z} {g : Y Z} [IsIso snd] [IsIso f] (sq : CommSq fst snd f g) :
                                        IsPullback fst snd f g

                                        The following diagram is a pullback

                                        X --f--> Z
                                        |        |
                                        id       id
                                        v        v
                                        X --f--> Z
                                        

                                        The following diagram is a pullback

                                        X --id--> X
                                        |         |
                                        f         f
                                        v         v
                                        Z --id--> Z
                                        

                                        In a category, given a morphism f : A ⟶ B and an object X, this is the obvious pullback diagram:

                                        A ⨯ X ⟶ A
                                          |     |
                                          v     v
                                        B ⨯ X ⟶ B
                                        
                                        theorem CategoryTheory.IsPushout.flip {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :
                                        IsPushout g f inr inl
                                        theorem CategoryTheory.IsPushout.flip_iff {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} :
                                        IsPushout f g inl inr IsPushout g f inr inl
                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the right and 𝟙 X on the left is a pushout square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the bottom and 𝟙 X on the top is a pushout square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the right left 𝟙 X on the right is a pushout square.

                                        @[simp]

                                        The square with 0 : 0 ⟶ 0 on the top and 𝟙 X on the bottom is a pushout square.

                                        theorem CategoryTheory.IsPushout.paste_vert {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : IsPushout h₂₁ v₂₁ v₂₂ h₃₁) :
                                        IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁

                                        Paste two pushout squares "vertically" to obtain another pushout square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        theorem CategoryTheory.IsPushout.paste_horiz {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : IsPushout h₁₂ v₁₂ v₁₃ h₂₂) :
                                        IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)

                                        Paste two pushout squares "horizontally" to obtain another pushout square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        
                                        theorem CategoryTheory.IsPushout.of_top {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁) (p : CategoryStruct.comp h₂₁ v₂₂ = CategoryStruct.comp v₂₁ h₃₁) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
                                        IsPushout h₂₁ v₂₁ v₂₂ h₃₁

                                        Given a pushout square assembled from a pushout square on the top and a commuting square on the bottom, the bottom square is a pushout square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        theorem CategoryTheory.IsPushout.of_left {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂)) (p : CategoryStruct.comp h₁₂ v₁₃ = CategoryStruct.comp v₁₂ h₂₂) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
                                        IsPushout h₁₂ v₁₂ v₁₃ h₂₂

                                        Given a pushout square assembled from a pushout square on the left and a commuting square on the right, the right square is a pushout square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        
                                        theorem CategoryTheory.IsPushout.paste_vert_iff {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₂₁ : X₂₁ X₃₁} {v₂₂ : X₂₂ X₃₂} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : CategoryStruct.comp h₂₁ v₂₂ = CategoryStruct.comp v₂₁ h₃₁) :
                                        IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) (CategoryStruct.comp v₁₂ v₂₂) h₃₁ IsPushout h₂₁ v₂₁ v₂₂ h₃₁
                                        theorem CategoryTheory.IsPushout.paste_horiz_iff {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₂ : X₂₂ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : CategoryStruct.comp h₁₂ v₁₃ = CategoryStruct.comp v₁₂ h₂₂) :
                                        IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryStruct.comp h₂₁ h₂₂) IsPushout h₁₂ v₁₂ v₁₃ h₂₂
                                        theorem CategoryTheory.IsPushout.of_top' {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ X₁₂} {h₂₁ : X₂₁ X₂₂} {h₃₁ : X₃₁ X₃₂} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₂ X₃₂} {v₂₁ : X₂₁ X₃₁} (s : IsPushout h₁₁ (CategoryStruct.comp v₁₁ v₂₁) v₁₃ h₃₁) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
                                        IsPushout h₂₁ v₂₁ (t.desc v₁₃ (CategoryStruct.comp v₂₁ h₃₁) ) h₃₁

                                        Variant of IsPushout.of_top where v₂₂ is induced from a morphism v₁₃ : X₁₂ ⟶ X₃₂, and the universal property of the top square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂
                                        |            |
                                        v₁₁          v₁₂
                                        ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂
                                        |            |
                                        v₂₁          v₂₂
                                        ↓            ↓
                                        X₃₁ - h₃₁ -> X₃₂
                                        
                                        theorem CategoryTheory.IsPushout.of_left' {C : Type u₁} [Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ X₁₂} {h₁₂ : X₁₂ X₁₃} {h₂₁ : X₂₁ X₂₂} {h₂₃ : X₂₁ X₂₃} {v₁₁ : X₁₁ X₂₁} {v₁₂ : X₁₂ X₂₂} {v₁₃ : X₁₃ X₂₃} (s : IsPushout (CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ h₂₃) (t : IsPushout h₁₁ v₁₁ v₁₂ h₂₁) :
                                        IsPushout h₁₂ v₁₂ v₁₃ (t.desc (CategoryStruct.comp h₁₂ v₁₃) h₂₃ )

                                        Variant of IsPushout.of_right where h₂₂ is induced from a morphism h₂₃ : X₂₁ ⟶ X₂₃, and the universal property of the left square.

                                        The objects in the statement fit into the following diagram:

                                        X₁₁ - h₁₁ -> X₁₂ - h₁₂ -> X₁₃
                                        |            |            |
                                        v₁₁          v₁₂          v₁₃
                                        ↓            ↓            ↓
                                        X₂₁ - h₂₁ -> X₂₂ - h₂₂ -> X₂₃
                                        

                                        The square

                                          X --inl--> X ⊞ Y
                                          |            |
                                          0           snd
                                          |            |
                                          v            v
                                          0 ---0-----> Y
                                        

                                        is a pushout square.

                                        The square

                                          Y --inr--> X ⊞ Y
                                          |            |
                                          0           fst
                                          |            |
                                          v            v
                                          0 ---0-----> X
                                        

                                        is a pushout square.

                                        theorem CategoryTheory.IsPushout.op {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :
                                        IsPullback inr.op inl.op g.op f.op
                                        theorem CategoryTheory.IsPushout.unop {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : Cᵒᵖ} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} (h : IsPushout f g inl inr) :
                                        theorem CategoryTheory.IsPushout.of_horiz_isIso_epi {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [Epi f] [IsIso inr] (sq : CommSq f g inl inr) :
                                        IsPushout f g inl inr
                                        theorem CategoryTheory.IsPushout.of_horiz_isIso {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [IsIso f] [IsIso inr] (sq : CommSq f g inl inr) :
                                        IsPushout f g inl inr
                                        theorem CategoryTheory.IsPushout.of_vert_isIso_epi {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [Epi g] [IsIso inl] (sq : CommSq f g inl inr) :
                                        IsPushout f g inl inr
                                        theorem CategoryTheory.IsPushout.of_vert_isIso {C : Type u₁} [Category.{v₁, u₁} C] {Z X Y P : C} {f : Z X} {g : Z Y} {inl : X P} {inr : Y P} [IsIso g] [IsIso inl] (sq : CommSq f g inl inr) :
                                        IsPushout f g inl inr

                                        The following diagram is a pullback

                                        X --f--> Z
                                        |        |
                                        id       id
                                        v        v
                                        X --f--> Z
                                        

                                        The following diagram is a pullback

                                        X --id--> X
                                        |         |
                                        f         f
                                        v         v
                                        Z --id--> Z
                                        

                                        In a category, given a morphism f : A ⟶ B and an object X, this is the obvious pushout diagram:

                                        A ⟶ A ⨿ X
                                        |     |
                                        v     v
                                        B ⟶ B ⨿ X
                                        
                                        noncomputable def CategoryTheory.IsPullback.isLimitFork {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X Y} {g g' : Y Z} (H : IsPullback f f g g') :

                                        If f : X ⟶ Y, g g' : Y ⟶ Z forms a pullback square, then f is the equalizer of g and g'.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          noncomputable def CategoryTheory.IsPushout.isLimitFork {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f f' : X Y} {g : Y Z} (H : IsPushout f f' g g) :

                                          If f f' : X ⟶ Y, g : Y ⟶ Z forms a pushout square, then g is the coequalizer of f and f'.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p₁ : IsPullback f g h i) (p₂ : IsPushout f g h i) :
                                            theorem CategoryTheory.BicartesianSq.flip {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} (p : BicartesianSq f g h i) :
                                             X ⊞ Y --fst--> X
                                               |            |
                                              snd           0
                                               |            |
                                               v            v
                                               Y -----0---> 0
                                            

                                            is a bi-Cartesian square.

                                               0 -----0---> X
                                               |            |
                                               0           inl
                                               |            |
                                               v            v
                                               Y --inr--> X ⊞ Y
                                            

                                            is a bi-Cartesian square.

                                            @[simp]
                                             X ⊞ Y --fst--> X
                                               |            |
                                              snd           0
                                               |            |
                                               v            v
                                               Y -----0---> 0
                                            

                                            is a bi-Cartesian square.

                                            @[simp]
                                               0 -----0---> X
                                               |            |
                                               0           inl
                                               |            |
                                               v            v
                                               Y --inr--> X ⊞ Y
                                            

                                            is a bi-Cartesian square.

                                            theorem CategoryTheory.Functor.map_isPullback {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.PreservesLimit (Limits.cospan h i) F] (s : IsPullback f g h i) :
                                            IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
                                            theorem CategoryTheory.Functor.map_isPushout {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.PreservesColimit (Limits.span f g) F] (s : IsPushout f g h i) :
                                            IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
                                            theorem CategoryTheory.IsPullback.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.PreservesLimit (Limits.cospan h i) F] (s : IsPullback f g h i) :
                                            IsPullback (F.map f) (F.map g) (F.map h) (F.map i)

                                            Alias of CategoryTheory.Functor.map_isPullback.

                                            theorem CategoryTheory.IsPushout.map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.PreservesColimit (Limits.span f g) F] (s : IsPushout f g h i) :
                                            IsPushout (F.map f) (F.map g) (F.map h) (F.map i)

                                            Alias of CategoryTheory.Functor.map_isPushout.

                                            theorem CategoryTheory.IsPullback.of_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.ReflectsLimit (Limits.cospan h i) F] (e : CategoryStruct.comp f h = CategoryStruct.comp g i) (H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) :
                                            IsPullback f g h i
                                            theorem CategoryTheory.IsPullback.of_map_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.ReflectsLimit (Limits.cospan h i) F] [F.Faithful] (H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) :
                                            IsPullback f g h i
                                            theorem CategoryTheory.IsPullback.map_iff {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [Limits.PreservesLimit (Limits.cospan h i) F] [Limits.ReflectsLimit (Limits.cospan h i) F] (e : CategoryStruct.comp f h = CategoryStruct.comp g i) :
                                            IsPullback (F.map f) (F.map g) (F.map h) (F.map i) IsPullback f g h i
                                            theorem CategoryTheory.IsPushout.of_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.ReflectsColimit (Limits.span f g) F] (e : CategoryStruct.comp f h = CategoryStruct.comp g i) (H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) :
                                            IsPushout f g h i
                                            theorem CategoryTheory.IsPushout.of_map_of_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} [Limits.ReflectsColimit (Limits.span f g) F] [F.Faithful] (H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) :
                                            IsPushout f g h i
                                            theorem CategoryTheory.IsPushout.map_iff {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} {f : W X} {g : W Y} {h : X Z} {i : Y Z} {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [Limits.PreservesColimit (Limits.span f g) F] [Limits.ReflectsColimit (Limits.span f g) F] (e : CategoryStruct.comp f h = CategoryStruct.comp g i) :
                                            IsPushout (F.map f) (F.map g) (F.map h) (F.map i) IsPushout f g h i