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✝ = (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.spanUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z) : span f.unop g.unop ≅ walkingCospanOpEquiv.inverse.comp (cospan f g).leftOp

The canonical isomorphism relating span f.unop g.unop and (cospan f g).leftOp

Equations

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

@[simp]

theorem CategoryTheory.Limits.spanUnop_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanUnop f g).inv.app X✝ = (match X✝ with | none => Iso.refl (Opposite.unop Z) | some WalkingPair.left => Iso.refl (Opposite.unop X) | some WalkingPair.right => Iso.refl (Opposite.unop Y)).inv

@[simp]

theorem CategoryTheory.Limits.spanUnop_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z) (X✝ : WalkingSpan) : (spanUnop f g).hom.app X✝ = (match X✝ with | none => Iso.refl (Opposite.unop Z) | some WalkingPair.left => Iso.refl (Opposite.unop X) | some WalkingPair.right => Iso.refl (Opposite.unop 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

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✝ = (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

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

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_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

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

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

The canonical isomorphism relating cospan f.unop g.unop and (span f g).leftOp

Equations

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

@[simp]

theorem CategoryTheory.Limits.cospanUnop_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanUnop f g).hom.app X✝ = (match X✝ with | none => Iso.refl (Opposite.unop X) | some WalkingPair.left => Iso.refl (Opposite.unop Y) | some WalkingPair.right => Iso.refl (Opposite.unop Z)).hom

@[simp]

theorem CategoryTheory.Limits.cospanUnop_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z) (X✝ : WalkingCospan) : (cospanUnop f g).inv.app X✝ = (match X✝ with | none => Iso.refl (Opposite.unop X) | some WalkingPair.left => Iso.refl (Opposite.unop Y) | some WalkingPair.right => Iso.refl (Opposite.unop Z)).inv

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✝ = (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

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

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_π_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

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

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_π_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

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

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 (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

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 (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

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

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

• c.unopOpIso = 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.opUnopIso).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.unopOpIso).symm.trans c.unop.isColimitEquivIsLimitOp.symm

@[simp]

theorem CategoryTheory.Limits.hasPushout_op_iff_hasPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : HasPushout f.op g.op ↔ HasPullback f g

@[simp]

theorem CategoryTheory.Limits.hasPushout_unop_iff_hasPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Z) (g : Y ⟶ Z) : HasPushout f.unop g.unop ↔ HasPullback f g

instance CategoryTheory.Limits.instHasPushoutOppositeOpOfHasPullback {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

instance CategoryTheory.Limits.instHasPushoutUnopOfHasPullbackOpposite {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

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] : 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] : 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] {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] : 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] {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] : 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] {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] : 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] {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] : 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.

Equations

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

@[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] : 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] {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] : 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] {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] : 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] {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] : 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] {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

@[simp]

theorem CategoryTheory.Limits.hasPullback_op_iff_hasPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : HasPullback f.op g.op ↔ HasPushout f g

@[simp]

theorem CategoryTheory.Limits.hasPullback_unop_iff_hasPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z) : HasPullback f.unop g.unop ↔ HasPushout f g

instance CategoryTheory.Limits.instHasPullbackOppositeOpOfHasPushout {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : HasPullback f.op g.op

instance CategoryTheory.Limits.instHasPullbackUnopOfHasPushoutOpposite {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g] : HasPullback f.unop g.unop

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] : 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] : 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] {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] : 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] {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] : 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] : 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] : 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.

Equations

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

@[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] : 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] {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] : 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] {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] : 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] : CategoryStruct.comp (pushoutIsoOpPullback f g).inv.unop (pullback.snd f.unop g.unop) = (pushout.inr f g).unop

theorem CategoryTheory.Limits.op_pullbackMap {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z S T : C} (f₁ : W ⟶ S) (f₂ : X ⟶ S) [HasPullback f₁ f₂] (g₁ : Y ⟶ T) (g₂ : Z ⟶ T) [HasPullback g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : CategoryStruct.comp f₁ i₃ = CategoryStruct.comp i₁ g₁) (eq₂ : CategoryStruct.comp f₂ i₃ = CategoryStruct.comp i₂ g₂) : (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op = CategoryStruct.comp (pushoutIsoOpPullback g₁.op g₂.op).inv (CategoryStruct.comp (pushout.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (pushoutIsoOpPullback f₁.op f₂.op).hom)

theorem CategoryTheory.Limits.op_pushoutMap {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z S T : C} (f₁ : S ⟶ W) (f₂ : S ⟶ X) [HasPushout f₁ f₂] (g₁ : T ⟶ Y) (g₂ : T ⟶ Z) [HasPushout g₁ g₂] (i₁ : W ⟶ Y) (i₂ : X ⟶ Z) (i₃ : S ⟶ T) (eq₁ : CategoryStruct.comp f₁ i₁ = CategoryStruct.comp i₃ g₁) (eq₂ : CategoryStruct.comp f₂ i₂ = CategoryStruct.comp i₃ g₂) : (pushout.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂).op = CategoryStruct.comp (pullbackIsoOpPushout g₁.op g₂.op).inv (CategoryStruct.comp (pullback.map g₁.op g₂.op f₁.op f₂.op i₁.op i₂.op i₃.op ⋯ ⋯) (pullbackIsoOpPushout f₁.op f₂.op).hom)

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

Equations

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

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

Equations

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

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.

Equations

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

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.

Equations

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