Pullbacks and pushouts in C and Cᵒᵖ

We construct pullbacks and pushouts in the opposite categories.

instance CategoryTheory.Limits.hasPullbacks_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasPushouts C] : HasPullbacks Cᵒᵖ

instance CategoryTheory.Limits.hasPushouts_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasPullbacks C] : HasPushouts Cᵒᵖ

def CategoryTheory.Limits.spanOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : span f.op g.op ≅ walkingCospanOpEquiv.inverse.comp (cospan f g).op

The canonical isomorphism relating Span f.op g.op and (Cospan f g).op

Equations

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

@[simp]

theorem CategoryTheory.Limits.spanOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).inv

@[simp]

theorem CategoryTheory.Limits.spanOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom

def CategoryTheory.Limits.opCospan {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : (cospan f g).op ≅ walkingCospanOpEquiv.functor.comp (span f.op g.op)

The canonical isomorphism relating (Cospan f g).op and Span f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.opCospan_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingCospanᵒᵖ) : (opCospan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) (Opposite.unop X✝)).inv

@[simp]

theorem CategoryTheory.Limits.opCospan_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingCospanᵒᵖ) : (opCospan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) (Opposite.unop X✝)).hom

def CategoryTheory.Limits.cospanOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : cospan f.op g.op ≅ walkingSpanOpEquiv.inverse.comp (span f g).op

The canonical isomorphism relating Cospan f.op g.op and (Span f g).op

Equations

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

@[simp]

theorem CategoryTheory.Limits.cospanOp_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv

@[simp]

theorem CategoryTheory.Limits.cospanOp_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).hom

def CategoryTheory.Limits.opSpan {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : (span f g).op ≅ walkingSpanOpEquiv.functor.comp (cospan f.op g.op)

The canonical isomorphism relating (Span f g).op and Cospan f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.opSpan_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingSpanᵒᵖ) : (opSpan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) (Opposite.unop X✝)).inv

@[simp]

theorem CategoryTheory.Limits.opSpan_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingSpanᵒᵖ) : (opSpan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) (Opposite.unop X✝)).hom

def CategoryTheory.Limits.PushoutCocone.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : PullbackCone f.unop g.unop

The obvious map PushoutCocone f g → PullbackCone f.unop g.unop

Equations

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

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.unop_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.pt = Opposite.unop c.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.unop_π_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) (X✝ : WalkingCospan) : c.unop.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).unop (Option.rec (Iso.refl X) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl Y) (Iso.refl Z) val) X✝).inv.unop

theorem CategoryTheory.Limits.PushoutCocone.unop_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.fst = c.inl.unop

theorem CategoryTheory.Limits.PushoutCocone.unop_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.snd = c.inr.unop

def CategoryTheory.Limits.PushoutCocone.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : PullbackCone f.op g.op

The obvious map PushoutCocone f.op g.op → PullbackCone f g

Equations

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

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.op_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.pt = Opposite.op c.pt

@[simp]

theorem CategoryTheory.Limits.PushoutCocone.op_π_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) (X✝ : WalkingCospan) : c.op.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).op (Option.rec (Iso.refl (Opposite.op X)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv

theorem CategoryTheory.Limits.PushoutCocone.op_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.fst = c.inl.op

theorem CategoryTheory.Limits.PushoutCocone.op_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.snd = c.inr.op

def CategoryTheory.Limits.PullbackCone.unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutCocone f.unop g.unop

The obvious map PullbackCone f g → PushoutCocone f.unop g.unop

Equations

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

@[simp]

theorem CategoryTheory.Limits.PullbackCone.unop_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (X✝ : WalkingSpan) : c.unop.ι.app X✝ = CategoryStruct.comp (Option.rec (Iso.refl Z) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl X) (Iso.refl Y) val) X✝).hom.unop (c.π.app X✝).unop

@[simp]

theorem CategoryTheory.Limits.PullbackCone.unop_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.pt = Opposite.unop c.pt

theorem CategoryTheory.Limits.PullbackCone.unop_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inl = c.fst.unop

theorem CategoryTheory.Limits.PullbackCone.unop_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.inr = c.snd.unop

def CategoryTheory.Limits.PullbackCone.op {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutCocone f.op g.op

The obvious map PullbackCone f g → PushoutCocone f.op g.op

Equations

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

@[simp]

theorem CategoryTheory.Limits.PullbackCone.op_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) (X✝ : WalkingSpan) : c.op.ι.app X✝ = CategoryStruct.comp (Option.rec (Iso.refl (Opposite.op Z)) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom (c.π.app X✝).op

@[simp]

theorem CategoryTheory.Limits.PullbackCone.op_pt {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.pt = Opposite.op c.pt

theorem CategoryTheory.Limits.PullbackCone.op_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inl = c.fst.op

theorem CategoryTheory.Limits.PullbackCone.op_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.inr = c.snd.op

def CategoryTheory.Limits.PullbackCone.opUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.unop ≅ c

If c is a pullback cone, then c.op.unop is isomorphic to c.

Equations

• c.opUnop = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯

def CategoryTheory.Limits.PullbackCone.unopOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.unop.op ≅ c

If c is a pullback cone in Cᵒᵖ, then c.unop.op is isomorphic to c.

Equations

• c.unopOp = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯

def CategoryTheory.Limits.PushoutCocone.opUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.op.unop ≅ c

If c is a pushout cocone, then c.op.unop is isomorphic to c.

Equations

• c.opUnop = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯

def CategoryTheory.Limits.PushoutCocone.unopOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : c.unop.op ≅ c

If c is a pushout cocone in Cᵒᵖ, then c.unop.op is isomorphic to c.

Equations

• c.unopOp = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯

noncomputable def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : IsColimit c ≃ IsLimit c.op

A pushout cone is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.

Equations

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

noncomputable def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : IsColimit c ≃ IsLimit c.unop

A pushout cone is a colimit cocone in Cᵒᵖ if and only if the corresponding pullback cone in C is a limit cone.

Equations

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

def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : IsLimit c ≃ IsColimit c.op

A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.

Equations

• c.isLimitEquivIsColimitOp = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.opUnop).symm.trans c.op.isColimitEquivIsLimitUnop.symm

def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : IsLimit c ≃ IsColimit c.unop

A pullback cone is a limit cone in Cᵒᵖ if and only if the corresponding pushout cocone in C is a colimit cocone.

Equations

• c.isLimitEquivIsColimitUnop = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.unopOp).symm.trans c.unop.isColimitEquivIsLimitOp.symm

noncomputable def CategoryTheory.Limits.pullbackIsoUnopPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [h : HasPullback f g] [HasPushout f.op g.op] : pullback f g ≅ Opposite.unop (pushout f.op g.op)

The pullback of f and g in C is isomorphic to the pushout of f.op and g.op in Cᵒᵖ.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.fst f g) = (pushout.inl f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pushout.inl f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.snd f g) = (pushout.inr f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pushout.inr f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pushout.inl f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.fst f g).op h

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] : CategoryStruct.comp (pushout.inr f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.snd f g).op

@[simp]

theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.snd f g).op h

noncomputable def CategoryTheory.Limits.pushoutIsoUnopPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [h : HasPushout f g] [HasPullback f.op g.op] : pushout f g ≅ Opposite.unop (pullback f.op g.op)

The pushout of f and g in C is isomorphic to the pullback of f.op and g.op in Cᵒᵖ.

Equations

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

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushout.inl f g) (pushoutIsoUnopPullback f g).hom = (pullback.fst f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] {Z✝ : C} (h : Opposite.unop (pullback f.op g.op) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.fst f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushout.inr f g) (pushoutIsoUnopPullback f g).hom = (pullback.snd f.op g.op).unop

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] {Z✝ : C} (h : Opposite.unop (pullback f.op g.op) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.snd f.op g.op).unop h

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.fst f.op g.op) = (pushout.inl f g).op

@[simp]

theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : X ⟶ Y) [HasPushout f g] [HasPullback f.op g.op] : CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.snd f.op g.op) = (pushout.inr f g).op