Pullback and pushout squares, and bicartesian 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 bicartesian squares, and show that the pullback and pushout squares for a biproduct are bicartesian.

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

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

Equations

• s.cone = CategoryTheory.Limits.PullbackCone.mk f g ⋯

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

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

Equations

• s.cocone = CategoryTheory.Limits.PushoutCocone.mk h i ⋯

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.CommSq.cocone_inl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i) : s.cocone.inl = h

@[simp]

theorem CategoryTheory.CommSq.cocone_inr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i) : s.cocone.inr = i

def CategoryTheory.CommSq.coneOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.CommSq f g h i) : p.cone.op ≅ ⋯.cocone

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

• p.coneOp = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl p.cone.op.pt) ⋯ ⋯

def CategoryTheory.CommSq.coconeOp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.CommSq f g h i) : p.cocone.op ≅ ⋯.cone

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

• p.coconeOp = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl p.cocone.op.pt) ⋯ ⋯

def CategoryTheory.CommSq.coneUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.CommSq f g h i) : p.cone.unop ≅ ⋯.cocone

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

• p.coneUnop = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl p.cone.unop.pt) ⋯ ⋯

def CategoryTheory.CommSq.coconeUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.CommSq f g h i) : p.cocone.unop ≅ ⋯.cone

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

• p.coconeUnop = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl p.cocone.unop.pt) ⋯ ⋯

structure CategoryTheory.IsPullback {C : Type u₁} [CategoryTheory.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 : Prop

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

• w : CategoryTheory.CategoryStruct.comp fst f = CategoryTheory.CategoryStruct.comp snd g
• isLimit' : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯))

  the pullback cone is a limit

structure CategoryTheory.IsPushout {C : Type u₁} [CategoryTheory.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 : Prop

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 cocartesian square.)

• w : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr
• isColimit' : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯))

  the pushout cocone is a colimit

structure CategoryTheory.BicartesianSq {C : Type u₁} [CategoryTheory.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 : Prop

A bicartesian 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.

• w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i
• isLimit' : Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g ⋯))
• isColimit' : Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯))

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₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) : CategoryTheory.Limits.PullbackCone f g

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

Equations

• h.cone = ⋯.cone

@[simp]

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

@[simp]

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

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

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

Equations

• h.isLimit = ⋯.some

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

API for PullbackCone.IsLimit.lift for IsPullback

Equations

• hP.lift h k w = CategoryTheory.Limits.PullbackCone.IsLimit.lift hP.isLimit h k w

@[simp]

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

@[simp]

theorem CategoryTheory.IsPullback.lift_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (hP.lift h k w) (CategoryTheory.CategoryStruct.comp fst h✝) = CategoryTheory.CategoryStruct.comp h h✝

@[simp]

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

@[simp]

theorem CategoryTheory.IsPullback.lift_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} (h : W ⟶ X) (k : W ⟶ Y) (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (hP.lift h k w) (CategoryTheory.CategoryStruct.comp snd h✝) = CategoryTheory.CategoryStruct.comp k h✝

theorem CategoryTheory.IsPullback.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (hP : CategoryTheory.IsPullback fst snd f g) {W : C} {k l : W ⟶ P} (h₀ : CategoryTheory.CategoryStruct.comp k fst = CategoryTheory.CategoryStruct.comp l fst) (h₁ : CategoryTheory.CategoryStruct.comp k snd = CategoryTheory.CategoryStruct.comp l snd) : k = l

theorem CategoryTheory.IsPullback.of_isLimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {c : CategoryTheory.Limits.PullbackCone f g} (h : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsPullback c.fst c.snd f g

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₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (w : CategoryTheory.CommSq fst snd f g) (h : CategoryTheory.Limits.IsLimit w.cone) : CategoryTheory.IsPullback fst snd f g

A variant of of_isLimit that is more useful with apply.

theorem CategoryTheory.IsPullback.of_isLimit_cone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} {c : CategoryTheory.Limits.Cone D} (hc : CategoryTheory.Limits.IsLimit c) : CategoryTheory.IsPullback (c.π.app CategoryTheory.Limits.WalkingCospan.left) (c.π.app CategoryTheory.Limits.WalkingCospan.right) (D.map CategoryTheory.Limits.WalkingCospan.Hom.inl) (D.map CategoryTheory.Limits.WalkingCospan.Hom.inr)

Variant of of_isLimit for an arbitrary cone on a diagram WalkingCospan ⥤ C.

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

theorem CategoryTheory.IsPullback.of_hasPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g) f g

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

theorem CategoryTheory.IsPullback.of_is_product {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {c : CategoryTheory.Limits.BinaryFan X Y} (h : CategoryTheory.Limits.IsLimit c) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback c.fst c.snd (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.from ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }))

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₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd)) (t : CategoryTheory.Limits.IsTerminal Z) : CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)

A variant of of_is_product that is more useful with apply.

theorem CategoryTheory.IsPullback.of_hasBinaryProduct' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from Y)

theorem CategoryTheory.IsPullback.of_hasBinaryProduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd 0 0

noncomputable def CategoryTheory.IsPullback.isoIsPullback {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.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

• CategoryTheory.IsPullback.isoIsPullback X Y h h' = h.isLimit.conePointUniqueUpToIso h'.isLimit

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom fst' = fst

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_fst_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom (CategoryTheory.CategoryStruct.comp fst' h✝) = CategoryTheory.CategoryStruct.comp fst h✝

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom snd' = snd

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_hom_snd_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').hom (CategoryTheory.CategoryStruct.comp snd' h✝) = CategoryTheory.CategoryStruct.comp snd h✝

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv fst = fst'

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_fst_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv (CategoryTheory.CategoryStruct.comp fst h✝) = CategoryTheory.CategoryStruct.comp fst' h✝

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv snd = snd'

@[simp]

theorem CategoryTheory.IsPullback.isoIsPullback_inv_snd_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g) {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPullback.isoIsPullback X Y h h').inv (CategoryTheory.CategoryStruct.comp snd h✝) = CategoryTheory.CategoryStruct.comp snd' h✝

noncomputable def CategoryTheory.IsPullback.isoPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] : P ≅ CategoryTheory.Limits.pullback f g

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

Equations

• h.isoPullback = (CategoryTheory.Limits.limit.isoLimitCone { cone := h.cone, isLimit := h.isLimit }).symm

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.Limits.pullback.fst f g) = fst

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h✝) = CategoryTheory.CategoryStruct.comp fst h✝

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.Limits.pullback.snd f g) = snd

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_hom_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.isoPullback.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h✝) = CategoryTheory.CategoryStruct.comp snd h✝

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.CategoryStruct.comp h.isoPullback.inv fst = CategoryTheory.Limits.pullback.fst f g

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_fst_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] {Z✝ : C} (h✝ : X ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.isoPullback.inv (CategoryTheory.CategoryStruct.comp fst h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h✝

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] : CategoryTheory.CategoryStruct.comp h.isoPullback.inv snd = CategoryTheory.Limits.pullback.snd f g

@[simp]

theorem CategoryTheory.IsPullback.isoPullback_inv_snd_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [CategoryTheory.Limits.HasPullback f g] {Z✝ : C} (h✝ : Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp h.isoPullback.inv (CategoryTheory.CategoryStruct.comp snd h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h✝

theorem CategoryTheory.IsPullback.of_iso_pullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.CommSq fst snd f g) [CategoryTheory.Limits.HasPullback f g] (i : P ≅ CategoryTheory.Limits.pullback f g) (w₁ : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.pullback.fst f g) = fst) (w₂ : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.pullback.snd f g) = snd) : CategoryTheory.IsPullback fst snd f g

theorem CategoryTheory.IsPullback.of_horiz_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.IsIso fst] [CategoryTheory.IsIso g] (sq : CategoryTheory.CommSq fst snd f g) : CategoryTheory.IsPullback fst snd f g

theorem CategoryTheory.IsPullback.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp fst e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom fst') (commsnd : CategoryTheory.CategoryStruct.comp snd e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom snd') (commf : CategoryTheory.CategoryStruct.comp f e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom f') (commg : CategoryTheory.CategoryStruct.comp g e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom g') : CategoryTheory.IsPullback fst' snd' f' g'

theorem CategoryTheory.IsPullback.isIso_fst_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {fst snd : P ⟶ X} {f : X ⟶ Y} [CategoryTheory.Mono f] (h : CategoryTheory.IsPullback fst snd f f) : CategoryTheory.IsIso fst

theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {fst snd : P ⟶ X} {f : X ⟶ Y} [CategoryTheory.Mono f] (h : CategoryTheory.IsPullback fst snd f f) : CategoryTheory.IsIso snd

def CategoryTheory.IsPushout.cocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) : CategoryTheory.Limits.PushoutCocone f g

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

Equations

• h.cocone = ⋯.cocone

@[simp]

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

@[simp]

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

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

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

Equations

• h.isColimit = ⋯.some

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

API for PushoutCocone.IsColimit.lift for IsPushout

Equations

• hP.desc h k w = CategoryTheory.Limits.PushoutCocone.IsColimit.desc hP.isColimit h k w

@[simp]

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

@[simp]

theorem CategoryTheory.IsPushout.inl_desc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inl (CategoryTheory.CategoryStruct.comp (hP.desc h k w) h✝) = CategoryTheory.CategoryStruct.comp h h✝

@[simp]

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

@[simp]

theorem CategoryTheory.IsPushout.inr_desc_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W) (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Z✝ : C} (h✝ : W ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inr (CategoryTheory.CategoryStruct.comp (hP.desc h k w) h✝) = CategoryTheory.CategoryStruct.comp k h✝

theorem CategoryTheory.IsPushout.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} {k l : P ⟶ W} (h₀ : CategoryTheory.CategoryStruct.comp inl k = CategoryTheory.CategoryStruct.comp inl l) (h₁ : CategoryTheory.CategoryStruct.comp inr k = CategoryTheory.CategoryStruct.comp inr l) : k = l

theorem CategoryTheory.IsPushout.of_isColimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {f : Z ⟶ X} {g : Z ⟶ Y} {c : CategoryTheory.Limits.PushoutCocone f g} (h : CategoryTheory.Limits.IsColimit c) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (w : CategoryTheory.CommSq f g inl inr) (h : CategoryTheory.Limits.IsColimit w.cocone) : CategoryTheory.IsPushout f g inl inr

A variant of of_isColimit that is more useful with apply.

theorem CategoryTheory.IsPushout.of_isColimit_cocone {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C} {c : CategoryTheory.Limits.Cocone D} (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.IsPushout (D.map CategoryTheory.Limits.WalkingSpan.Hom.fst) (D.map CategoryTheory.Limits.WalkingSpan.Hom.snd) (c.ι.app CategoryTheory.Limits.WalkingSpan.left) (c.ι.app CategoryTheory.Limits.WalkingSpan.right)

Variant of of_isColimit for an arbitrary cocone on a diagram WalkingSpan ⥤ C.

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

theorem CategoryTheory.IsPushout.of_hasPushout {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} (f : Z ⟶ X) (g : Z ⟶ Y) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.IsPushout f g (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.Limits.pushout.inr f g)

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

theorem CategoryTheory.IsPushout.of_is_coproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y} (h : CategoryTheory.Limits.IsColimit c) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left })) (t.to ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right })) c.inl c.inr

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₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)) (t : CategoryTheory.Limits.IsInitial Z) : CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr

A variant of of_is_coproduct that is more useful with apply.

theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasInitial C] : CategoryTheory.IsPushout (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y) CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr

theorem CategoryTheory.IsPushout.of_hasBinaryCoproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] (X Y : C) [CategoryTheory.Limits.HasBinaryCoproduct X Y] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr

noncomputable def CategoryTheory.IsPushout.isoIsPushout {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.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

• CategoryTheory.IsPushout.isoIsPushout X Y h h' = h.isColimit.coconePointUniqueUpToIso h'.isColimit

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') : CategoryTheory.CategoryStruct.comp inl (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inl'

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_hom_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inl (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom h✝) = CategoryTheory.CategoryStruct.comp inl' h✝

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') : CategoryTheory.CategoryStruct.comp inr (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom = inr'

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_hom_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') {Z✝ : C} (h✝ : P' ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inr (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').hom h✝) = CategoryTheory.CategoryStruct.comp inr' h✝

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') : CategoryTheory.CategoryStruct.comp inl' (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inl

@[simp]

theorem CategoryTheory.IsPushout.inl_isoIsPushout_inv_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') {Z✝ : C} (h✝ : P ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inl' (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv h✝) = CategoryTheory.CategoryStruct.comp inl h✝

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') : CategoryTheory.CategoryStruct.comp inr' (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv = inr

@[simp]

theorem CategoryTheory.IsPushout.inr_isoIsPushout_inv_assoc {C : Type u₁} [CategoryTheory.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 : CategoryTheory.IsPushout f g inl inr) (h' : CategoryTheory.IsPushout f g inl' inr') {Z✝ : C} (h✝ : P ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inr' (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsPushout.isoIsPushout X Y h h').inv h✝) = CategoryTheory.CategoryStruct.comp inr h✝

noncomputable def CategoryTheory.IsPushout.isoPushout {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] : P ≅ CategoryTheory.Limits.pushout f g

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

Equations

• h.isoPushout = (CategoryTheory.Limits.colimit.isoColimitCocone { cocone := h.cocone, isColimit := h.isColimit }).symm

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h.isoPushout.inv = inl

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] {Z✝ : C} (h✝ : P ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) (CategoryTheory.CategoryStruct.comp h.isoPushout.inv h✝) = CategoryTheory.CategoryStruct.comp inl h✝

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h.isoPushout.inv = inr

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] {Z✝ : C} (h✝ : P ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) (CategoryTheory.CategoryStruct.comp h.isoPushout.inv h✝) = CategoryTheory.CategoryStruct.comp inr h✝

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.CategoryStruct.comp inl h.isoPushout.hom = CategoryTheory.Limits.pushout.inl f g

@[simp]

theorem CategoryTheory.IsPushout.inl_isoPushout_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] {Z✝ : C} (h✝ : CategoryTheory.Limits.pushout f g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inl (CategoryTheory.CategoryStruct.comp h.isoPushout.hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) h✝

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] : CategoryTheory.CategoryStruct.comp inr h.isoPushout.hom = CategoryTheory.Limits.pushout.inr f g

@[simp]

theorem CategoryTheory.IsPushout.inr_isoPushout_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.IsPushout f g inl inr) [CategoryTheory.Limits.HasPushout f g] {Z✝ : C} (h✝ : CategoryTheory.Limits.pushout f g ⟶ Z✝) : CategoryTheory.CategoryStruct.comp inr (CategoryTheory.CategoryStruct.comp h.isoPushout.hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) h✝

theorem CategoryTheory.IsPushout.of_iso_pushout {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.CommSq f g inl inr) [CategoryTheory.Limits.HasPushout f g] (i : P ≅ CategoryTheory.Limits.pushout f g) (w₁ : CategoryTheory.CategoryStruct.comp inl i.hom = CategoryTheory.Limits.pushout.inl f g) (w₂ : CategoryTheory.CategoryStruct.comp inr i.hom = CategoryTheory.Limits.pushout.inr f g) : CategoryTheory.IsPushout f g inl inr

theorem CategoryTheory.IsPushout.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (h : CategoryTheory.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 : CategoryTheory.CategoryStruct.comp f e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom f') (commg : CategoryTheory.CategoryStruct.comp g e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom g') (comminl : CategoryTheory.CategoryStruct.comp inl e₄.hom = CategoryTheory.CategoryStruct.comp e₂.hom inl') (comminr : CategoryTheory.CategoryStruct.comp inr e₄.hom = CategoryTheory.CategoryStruct.comp e₃.hom inr') : CategoryTheory.IsPushout f' g' inl' inr'

theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {inl inr : X ⟶ P} {f : Y ⟶ X} [CategoryTheory.Epi f] (h : CategoryTheory.IsPushout f f inl inr) : CategoryTheory.IsIso inl

theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y : C} {inl inr : X ⟶ P} {f : Y ⟶ X} [CategoryTheory.Epi f] (h : CategoryTheory.IsPushout f f inl inr) : CategoryTheory.IsIso inr

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

theorem CategoryTheory.IsPullback.flip_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} : CategoryTheory.IsPullback fst snd f g ↔ CategoryTheory.IsPullback snd fst g f

@[simp]

theorem CategoryTheory.IsPullback.zero_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPullback 0 0 (CategoryTheory.CategoryStruct.id X) 0

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

@[simp]

theorem CategoryTheory.IsPullback.zero_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPullback 0 0 0 (CategoryTheory.CategoryStruct.id X)

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

@[simp]

theorem CategoryTheory.IsPullback.zero_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPullback 0 (CategoryTheory.CategoryStruct.id X) 0 0

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

@[simp]

theorem CategoryTheory.IsPullback.zero_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) 0 0 0

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) : CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁) (p : CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁) (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)) (p : CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁) (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) (e : CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁) : CategoryTheory.IsPullback h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔ CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁

theorem CategoryTheory.IsPullback.paste_horiz_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) (e : CategoryTheory.CategoryStruct.comp h₁₁ v₁₂ = CategoryTheory.CategoryStruct.comp v₁₁ h₂₁) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) ↔ CategoryTheory.IsPullback h₁₁ v₁₁ v₁₂ h₂₁

theorem CategoryTheory.IsPullback.of_right' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {h₁₃ : X₁₁ ⟶ X₁₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPullback h₁₃ v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)) (t : CategoryTheory.IsPullback h₁₂ v₁₂ v₁₃ h₂₂) : CategoryTheory.IsPullback (t.lift h₁₃ (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₃₁ : X₁₁ ⟶ X₃₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPullback h₁₁ v₃₁ (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁) (t : CategoryTheory.IsPullback h₂₁ v₂₁ v₂₂ h₃₁) : CategoryTheory.IsPullback h₁₁ (t.lift (CategoryTheory.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₃₂

theorem CategoryTheory.IsPullback.of_isBilimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.fst b.snd 0 0

@[simp]

theorem CategoryTheory.IsPullback.of_has_biproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0

theorem CategoryTheory.IsPullback.inl_snd' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.inl 0 b.snd 0

@[simp]

theorem CategoryTheory.IsPullback.inl_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0

The square

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

is a pullback square.

theorem CategoryTheory.IsPullback.inr_fst' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback b.inr 0 b.fst 0

@[simp]

theorem CategoryTheory.IsPullback.inr_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0

The square

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

is a pullback square.

theorem CategoryTheory.IsPullback.of_is_bilimit' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPullback 0 0 b.inl b.inr

theorem CategoryTheory.IsPullback.of_hasBinaryBiproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPullback 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr

instance CategoryTheory.IsPullback.hasPullback_biprod_fst_biprod_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.HasPullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr

Equations

• ⋯ = ⋯

def CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.pullback CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr ≅ 0

The pullback of biprod.inl and biprod.inr is the zero object.

Equations

• CategoryTheory.IsPullback.pullbackBiprodInlBiprodInr = CategoryTheory.Limits.limit.isoLimitCone { cone := ⋯.cone, isLimit := ⋯.isLimit }

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

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

theorem CategoryTheory.IsPullback.of_vert_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} [CategoryTheory.IsIso snd] [CategoryTheory.IsIso f] (sq : CategoryTheory.CommSq fst snd f g) : CategoryTheory.IsPullback fst snd f g

theorem CategoryTheory.IsPullback.of_id_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Z : C} {f : X ⟶ Z} : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)

theorem CategoryTheory.IsPullback.of_id_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Z : C} {f : X ⟶ Z} : CategoryTheory.IsPullback f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f

theorem CategoryTheory.IsPullback.id_vert {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Z : C} (f : X ⟶ Z) : CategoryTheory.IsPullback f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f

The following diagram is a pullback

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

theorem CategoryTheory.IsPullback.id_horiz {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Z : C} (f : X ⟶ Z) : CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)

The following diagram is a pullback

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

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

theorem CategoryTheory.IsPushout.flip_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} : CategoryTheory.IsPushout f g inl inr ↔ CategoryTheory.IsPushout g f inr inl

@[simp]

theorem CategoryTheory.IsPushout.zero_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPushout 0 (CategoryTheory.CategoryStruct.id X) 0 0

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

@[simp]

theorem CategoryTheory.IsPushout.zero_bot {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id X) 0 0 0

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

@[simp]

theorem CategoryTheory.IsPushout.zero_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPushout 0 0 (CategoryTheory.CategoryStruct.id X) 0

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

@[simp]

theorem CategoryTheory.IsPushout.zero_top {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X : C) : CategoryTheory.IsPushout 0 0 0 (CategoryTheory.CategoryStruct.id X)

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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁) : CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (t : CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂) : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁) (p : CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂)) (p : CategoryTheory.CategoryStruct.comp h₁₂ v₁₃ = CategoryTheory.CategoryStruct.comp v₁₂ h₂₂) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₂₁ : X₂₁ ⟶ X₃₁} {v₂₂ : X₂₂ ⟶ X₃₂} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : CategoryTheory.CategoryStruct.comp h₂₁ v₂₂ = CategoryTheory.CategoryStruct.comp v₂₁ h₃₁) : CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) (CategoryTheory.CategoryStruct.comp v₁₂ v₂₂) h₃₁ ↔ CategoryTheory.IsPushout h₂₁ v₂₁ v₂₂ h₃₁

theorem CategoryTheory.IsPushout.paste_horiz_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₂ : X₂₂ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) (e : CategoryTheory.CategoryStruct.comp h₁₂ v₁₃ = CategoryTheory.CategoryStruct.comp v₁₂ h₂₂) : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ (CategoryTheory.CategoryStruct.comp h₂₁ h₂₂) ↔ CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ h₂₂

theorem CategoryTheory.IsPushout.of_top' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₂₁ X₂₂ X₃₁ X₃₂ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₂₁ : X₂₁ ⟶ X₂₂} {h₃₁ : X₃₁ ⟶ X₃₂} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₂ ⟶ X₃₂} {v₂₁ : X₂₁ ⟶ X₃₁} (s : CategoryTheory.IsPushout h₁₁ (CategoryTheory.CategoryStruct.comp v₁₁ v₂₁) v₁₃ h₃₁) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : CategoryTheory.IsPushout h₂₁ v₂₁ (t.desc v₁₃ (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {X₁₁ X₁₂ X₁₃ X₂₁ X₂₂ X₂₃ : C} {h₁₁ : X₁₁ ⟶ X₁₂} {h₁₂ : X₁₂ ⟶ X₁₃} {h₂₁ : X₂₁ ⟶ X₂₂} {h₂₃ : X₂₁ ⟶ X₂₃} {v₁₁ : X₁₁ ⟶ X₂₁} {v₁₂ : X₁₂ ⟶ X₂₂} {v₁₃ : X₁₃ ⟶ X₂₃} (s : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.comp h₁₁ h₁₂) v₁₁ v₁₃ h₂₃) (t : CategoryTheory.IsPushout h₁₁ v₁₁ v₁₂ h₂₁) : CategoryTheory.IsPushout h₁₂ v₁₂ v₁₃ (t.desc (CategoryTheory.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₂₃

theorem CategoryTheory.IsPushout.of_isBilimit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout 0 0 b.inl b.inr

@[simp]

theorem CategoryTheory.IsPushout.of_has_biproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr

theorem CategoryTheory.IsPushout.inl_snd' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.inl 0 b.snd 0

theorem CategoryTheory.IsPushout.inl_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inl 0 CategoryTheory.Limits.biprod.snd 0

The square

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

is a pushout square.

theorem CategoryTheory.IsPushout.inr_fst' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.inr 0 b.fst 0

theorem CategoryTheory.IsPushout.inr_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.inr 0 CategoryTheory.Limits.biprod.fst 0

The square

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

is a pushout square.

theorem CategoryTheory.IsPushout.of_is_bilimit' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.IsPushout b.fst b.snd 0 0

theorem CategoryTheory.IsPushout.of_hasBinaryBiproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.IsPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0

instance CategoryTheory.IsPushout.hasPushout_biprod_fst_biprod_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.HasPushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd

Equations

• ⋯ = ⋯

def CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.Limits.pushout CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd ≅ 0

The pushout of biprod.fst and biprod.snd is the zero object.

Equations

• CategoryTheory.IsPushout.pushoutBiprodFstBiprodSnd = CategoryTheory.Limits.colimit.isoColimitCocone { cocone := ⋯.cocone, isColimit := ⋯.isColimit }

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

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

theorem CategoryTheory.IsPushout.of_horiz_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} [CategoryTheory.IsIso f] [CategoryTheory.IsIso inr] (sq : CategoryTheory.CommSq f g inl inr) : CategoryTheory.IsPushout f g inl inr

theorem CategoryTheory.IsPushout.of_vert_isIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} [CategoryTheory.IsIso g] [CategoryTheory.IsIso inl] (sq : CategoryTheory.CommSq f g inl inr) : CategoryTheory.IsPushout f g inl inr

theorem CategoryTheory.IsPushout.of_id_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} {f : Z ⟶ X} : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id Z) f f (CategoryTheory.CategoryStruct.id X)

theorem CategoryTheory.IsPushout.of_id_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} {f : Z ⟶ X} : CategoryTheory.IsPushout f (CategoryTheory.CategoryStruct.id Z) (CategoryTheory.CategoryStruct.id X) f

theorem CategoryTheory.IsPushout.id_vert {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (f : X ⟶ Z) : CategoryTheory.IsPushout f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Z) f

The following diagram is a pullback

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

theorem CategoryTheory.IsPushout.id_horiz {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (f : X ⟶ Z) : CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)

The following diagram is a pullback

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

noncomputable def CategoryTheory.IsPullback.isLimitFork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g g' : Y ⟶ Z} (H : CategoryTheory.IsPullback f f g g') : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)

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.

noncomputable def CategoryTheory.IsPushout.isLimitFork {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f f' : X ⟶ Y} {g : Y ⟶ Z} (H : CategoryTheory.IsPushout f f' g g) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ 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.

theorem CategoryTheory.BicartesianSq.of_isPullback_isPushout {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p₁ : CategoryTheory.IsPullback f g h i) (p₂ : CategoryTheory.IsPushout f g h i) : CategoryTheory.BicartesianSq f g h i

theorem CategoryTheory.BicartesianSq.flip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CategoryTheory.BicartesianSq f g h i) : CategoryTheory.BicartesianSq g f i h

theorem CategoryTheory.BicartesianSq.of_is_biproduct₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.BicartesianSq b.fst b.snd 0 0

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

is a bicartesian square.

theorem CategoryTheory.BicartesianSq.of_is_biproduct₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] {b : CategoryTheory.Limits.BinaryBicone X Y} (h : b.IsBilimit) : CategoryTheory.BicartesianSq 0 0 b.inl b.inr

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

is a bicartesian square.

@[simp]

theorem CategoryTheory.BicartesianSq.of_has_biproduct₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.BicartesianSq CategoryTheory.Limits.biprod.fst CategoryTheory.Limits.biprod.snd 0 0

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

is a bicartesian square.

@[simp]

theorem CategoryTheory.BicartesianSq.of_has_biproduct₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproduct X Y] : CategoryTheory.BicartesianSq 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr

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

is a bicartesian square.

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

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

theorem CategoryTheory.IsPullback.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F] (s : CategoryTheory.IsPullback f g h i) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F] (s : CategoryTheory.IsPushout f g h i) : CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F] (e : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i) (H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) : CategoryTheory.IsPullback f g h i

theorem CategoryTheory.IsPullback.of_map_of_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F] [F.Faithful] (H : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i)) : CategoryTheory.IsPullback f g h i

theorem CategoryTheory.IsPullback.map_iff {C : Type u₁} [CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan h i) F] [CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan h i) F] (e : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i) : CategoryTheory.IsPullback (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPullback f g h i

theorem CategoryTheory.IsPushout.of_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F] (e : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i) (H : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) : CategoryTheory.IsPushout f g h i

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

theorem CategoryTheory.IsPushout.map_iff {C : Type u₁} [CategoryTheory.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} [CategoryTheory.Category.{u_2, u_1} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) F] [CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span f g) F] (e : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i) : CategoryTheory.IsPushout (F.map f) (F.map g) (F.map h) (F.map i) ↔ CategoryTheory.IsPushout f g h i