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

@[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✝ = (match X✝ with | none => Iso.refl (Opposite.op Z) | some WalkingPair.left => Iso.refl (Opposite.op X) | some WalkingPair.right => Iso.refl (Opposite.op Y)).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✝ = (match X✝ with | none => Iso.refl (Opposite.op Z) | some WalkingPair.left => Iso.refl (Opposite.op X) | some WalkingPair.right => Iso.refl (Opposite.op Y)).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

@[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✝ = (match Opposite.unop X✝ with | none => Iso.refl (Opposite.op Z) | some WalkingPair.left => Iso.refl (Opposite.op X) | some WalkingPair.right => Iso.refl (Opposite.op Y)).hom

@[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✝ = (match Opposite.unop X✝ with | none => Iso.refl (Opposite.op Z) | some WalkingPair.left => Iso.refl (Opposite.op X) | some WalkingPair.right => Iso.refl (Opposite.op Y)).inv

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

@[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✝ = (match X✝ with | none => Iso.refl (Opposite.op X) | some WalkingPair.left => Iso.refl (Opposite.op Y) | some WalkingPair.right => Iso.refl (Opposite.op Z)).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✝ = (match X✝ with | none => Iso.refl (Opposite.op X) | some WalkingPair.left => Iso.refl (Opposite.op Y) | some WalkingPair.right => Iso.refl (Opposite.op Z)).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

@[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✝ = (match Opposite.unop X✝ with | none => Iso.refl (Opposite.op X) | some WalkingPair.left => Iso.refl (Opposite.op Y) | some WalkingPair.right => Iso.refl (Opposite.op Z)).hom

@[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✝ = (match Opposite.unop X✝ with | none => Iso.refl (Opposite.op X) | some WalkingPair.left => Iso.refl (Opposite.op Y) | some WalkingPair.right => Iso.refl (Opposite.op Z)).inv

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

@[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 (match X✝ with | none => Iso.refl X | some WalkingPair.left => Iso.refl Y | some WalkingPair.right => Iso.refl Z).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

@[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 (match X✝ with | none => Iso.refl (Opposite.op X) | some WalkingPair.left => Iso.refl (Opposite.op Y) | some WalkingPair.right => Iso.refl (Opposite.op Z)).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

@[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 (match X✝ with | none => Iso.refl Z | some WalkingPair.left => Iso.refl X | some WalkingPair.right => Iso.refl Y).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

@[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

@[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 (match X✝ with | none => Iso.refl (Opposite.op Z) | some WalkingPair.left => Iso.refl (Opposite.op X) | some WalkingPair.right => Iso.refl (Opposite.op Y)).hom (c.π.app X✝).op

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.opUnopIso {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.

def CategoryTheory.Limits.PullbackCone.unopOpIso {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.

def CategoryTheory.Limits.PushoutCocone.opUnopIso {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.

def CategoryTheory.Limits.PushoutCocone.unopOpIso {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.

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.

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.

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.

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.

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ᵒᵖ.

@[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.pullbackIsoOpPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z) [h : HasPullback f g] [HasPushout f.unop g.unop] : pullback f g ≅ Opposite.op (pushout f.unop g.unop)

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoOpPushout_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.unop g.unop] {Z✝ : Cᵒᵖ} (h : X ⟶ Z✝) : CategoryStruct.comp (pullbackIsoOpPushout f g).inv (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pushout.inl f.unop g.unop).op h

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoOpPushout_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.unop g.unop] {Z✝ : Cᵒᵖ} (h : Y ⟶ Z✝) : CategoryStruct.comp (pullbackIsoOpPushout f g).inv (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pushout.inr f.unop g.unop).op h

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoOpPushout_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.unop g.unop] {Z✝ : C} (h : Opposite.unop (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f.unop g.unop) (CategoryStruct.comp (pullbackIsoOpPushout f g).hom.unop h) = CategoryStruct.comp (pullback.fst f g).unop h

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pullbackIsoOpPushout_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.unop g.unop] {Z✝ : C} (h : Opposite.unop (pullback f g) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f.unop g.unop) (CategoryStruct.comp (pullbackIsoOpPushout f g).hom.unop h) = CategoryStruct.comp (pullback.snd f g).unop 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ᵒᵖ.

@[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

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pushoutIsoOpPullback_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.unop g.unop] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f.unop g.unop) ⟶ Z✝) : CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushoutIsoOpPullback f g).hom h) = CategoryStruct.comp (pullback.fst f.unop g.unop).op h

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.pushoutIsoOpPullback_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.unop g.unop] {Z✝ : Cᵒᵖ} (h : Opposite.op (pullback f.unop g.unop) ⟶ Z✝) : CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushoutIsoOpPullback f g).hom h) = CategoryStruct.comp (pullback.snd f.unop g.unop).op h

@[simp]

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

@[simp]

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

def CategoryTheory.CommSq.coneOp {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : 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

def CategoryTheory.CommSq.coconeOp {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : 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

def CategoryTheory.CommSq.coneUnop {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : 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.

def CategoryTheory.CommSq.coconeUnop {C : Type u_1} [Category.{v_1, u_1} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : 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.