Equalizers and coequalizers in C and Cᵒᵖ

We construct equalizers and coequalizers in the opposite categories.

instance CategoryTheory.Limits.hasEqualizers_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasCoequalizers C] : HasEqualizers Cᵒᵖ

instance CategoryTheory.Limits.hasCoequalizers_opposite {C : Type u₁} [Category.{v₁, u₁} C] [HasEqualizers C] : HasCoequalizers Cᵒᵖ

def CategoryTheory.Limits.parallelPairOpIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : parallelPair f.op g.op ≅ walkingParallelPairOpEquiv.functor.comp (parallelPair f g).op

The canonical isomorphism relating parallelPair f.op g.op and (parallelPair f g).op

@[simp]

theorem CategoryTheory.Limits.parallelPairOpIso_hom_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (parallelPairOpIso f g).hom.app WalkingParallelPair.zero = CategoryStruct.id ((parallelPair f.op g.op).obj WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.parallelPairOpIso_hom_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (parallelPairOpIso f g).hom.app WalkingParallelPair.one = CategoryStruct.id ((parallelPair f.op g.op).obj WalkingParallelPair.one)

@[simp]

theorem CategoryTheory.Limits.parallelPairOpIso_inv_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (parallelPairOpIso f g).inv.app WalkingParallelPair.zero = CategoryStruct.id ((walkingParallelPairOpEquiv.functor.comp (parallelPair f g).op).obj WalkingParallelPair.zero)

@[simp]

theorem CategoryTheory.Limits.parallelPairOpIso_inv_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (parallelPairOpIso f g).inv.app WalkingParallelPair.one = CategoryStruct.id ((walkingParallelPairOpEquiv.functor.comp (parallelPair f g).op).obj WalkingParallelPair.one)

def CategoryTheory.Limits.opParallelPairIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (parallelPair f g).op ≅ walkingParallelPairOpEquiv.inverse.comp (parallelPair f.op g.op)

The canonical isomorphism relating (parallelPair f g).op and parallelPair f.op g.op

@[simp]

theorem CategoryTheory.Limits.opParallelPairIso_hom_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (opParallelPairIso f g).hom.app (Opposite.op WalkingParallelPair.zero) = CategoryStruct.id ((parallelPair f g).op.obj (Opposite.op WalkingParallelPair.zero))

@[simp]

theorem CategoryTheory.Limits.opParallelPairIso_hom_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (opParallelPairIso f g).hom.app (Opposite.op WalkingParallelPair.one) = CategoryStruct.id ((parallelPair f g).op.obj (Opposite.op WalkingParallelPair.one))

@[simp]

theorem CategoryTheory.Limits.opParallelPairIso_inv_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (opParallelPairIso f g).inv.app (Opposite.op WalkingParallelPair.zero) = CategoryStruct.id ((walkingParallelPairOpEquiv.inverse.comp (parallelPair f.op g.op)).obj (Opposite.op WalkingParallelPair.zero))

@[simp]

theorem CategoryTheory.Limits.opParallelPairIso_inv_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y) : (opParallelPairIso f g).inv.app (Opposite.op WalkingParallelPair.one) = CategoryStruct.id ((walkingParallelPairOpEquiv.inverse.comp (parallelPair f.op g.op)).obj (Opposite.op WalkingParallelPair.one))

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

The obvious map Cofork f g → Fork f.unop g.unop

theorem CategoryTheory.Limits.Cofork.unop_π_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Cofork f g) : c.unop.π.app WalkingParallelPair.one = (c.ι.app WalkingParallelPair.zero).unop

theorem CategoryTheory.Limits.Cofork.unop_π_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Cofork f g) : c.unop.π.app WalkingParallelPair.zero = (c.ι.app WalkingParallelPair.one).unop

theorem CategoryTheory.Limits.Cofork.unop_ι {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Cofork f g) : c.unop.ι = c.π.unop

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

The obvious map Cofork f g → Fork f.op g.op

theorem CategoryTheory.Limits.Cofork.op_π_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Cofork f g) : c.op.π.app WalkingParallelPair.one = (c.ι.app WalkingParallelPair.zero).op

theorem CategoryTheory.Limits.Cofork.op_π_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Cofork f g) : c.op.π.app WalkingParallelPair.zero = (c.ι.app WalkingParallelPair.one).op

theorem CategoryTheory.Limits.Cofork.op_ι {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Cofork f g) : c.op.ι = c.π.op

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

The obvious map Fork f g → Cofork f.unop g.unop

theorem CategoryTheory.Limits.Fork.unop_ι_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Fork f g) : c.unop.ι.app WalkingParallelPair.one = (c.π.app WalkingParallelPair.zero).unop

theorem CategoryTheory.Limits.Fork.unop_ι_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Fork f g) : c.unop.ι.app WalkingParallelPair.zero = (c.π.app WalkingParallelPair.one).unop

theorem CategoryTheory.Limits.Fork.unop_π {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Fork f g) : c.unop.π = c.ι.unop

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

The obvious map Fork f g → Cofork f.op g.op

@[simp]

theorem CategoryTheory.Limits.Fork.op_ι_app {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) (X✝ : WalkingParallelPair) : c.op.ι.app X✝ = CategoryStruct.comp ((parallelPairOpIso f g).hom.app X✝) (c.π.app (Opposite.unop (walkingParallelPairOp.obj X✝))).op

@[simp]

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

theorem CategoryTheory.Limits.Fork.op_ι_app_one {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.op.ι.app WalkingParallelPair.one = (c.π.app WalkingParallelPair.zero).op

theorem CategoryTheory.Limits.Fork.op_ι_app_zero {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.op.ι.app WalkingParallelPair.zero = (c.π.app WalkingParallelPair.one).op

theorem CategoryTheory.Limits.Fork.op_π {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.op.π = c.ι.op

theorem CategoryTheory.Limits.Cofork.op_unop_π {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Cofork f g) : c.op.unop.π = c.π

theorem CategoryTheory.Limits.Cofork.unop_op_π {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Cofork f g) : c.unop.op.π = c.π

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

If c is a cofork, then c.op.unop is isomorphic to c.

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

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

theorem CategoryTheory.Limits.Fork.op_unop_ι {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f g : X ⟶ Y} (c : Fork f g) : c.op.unop.ι = c.ι

theorem CategoryTheory.Limits.Fork.unop_op_ι {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y} (c : Fork f g) : c.unop.op.ι = c.ι

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

If c is a fork, then c.op.unop is isomorphic to c.

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

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

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

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

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

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

def CategoryTheory.Limits.Cofork.ofπOpIsoOfι {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (w' : CategoryStruct.comp π'.op f.op = CategoryStruct.comp π'.op g.op) (h : π = π') : (ofπ π w).op ≅ Fork.ofι π'.op w'

The canonical isomorphism between (Cofork.ofπ π w).op and Fork.ofι π.op w'.

def CategoryTheory.Limits.Cofork.ofπUnopIsoOfι {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (w' : CategoryStruct.comp π'.unop f.unop = CategoryStruct.comp π'.unop g.unop) (h : π = π') : (ofπ π w).unop ≅ Fork.ofι π'.unop w'

The canonical isomorphism between (Cofork.ofπ π w).unop and Fork.ofι π.unop w'.

def CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (w' : CategoryStruct.comp π'.op f.op = CategoryStruct.comp π'.op g.op) (h : π = π') : IsColimit (ofπ π w) ≃ IsLimit (Fork.ofι π'.op w')

Cofork.ofπ π w is a colimit cocone if and only if Fork.ofι π.op w' in the opposite category is a limit cone.

def CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (π π' : Y ⟶ P) (w : CategoryStruct.comp f π = CategoryStruct.comp g π) (w' : CategoryStruct.comp π'.unop f.unop = CategoryStruct.comp π'.unop g.unop) (h : π = π') : IsColimit (ofπ π w) ≃ IsLimit (Fork.ofι π'.unop w')

Cofork.ofπ π w is a colimit cocone in Cᵒᵖ if and only if Fork.ofι π'.unop w' in C is a limit cone.

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

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

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

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

def CategoryTheory.Limits.Fork.ofιOpIsoOfπ {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (ι ι' : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (w' : CategoryStruct.comp f.op ι'.op = CategoryStruct.comp g.op ι'.op) (h : ι = ι') : (ofι ι w).op ≅ Cofork.ofπ ι'.op w'

The canonical isomorphism between (Fork.ofι ι w).op and Cofork.ofπ ι.op w'.

def CategoryTheory.Limits.Fork.ofιUnopIsoOfπ {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (ι ι' : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (w' : CategoryStruct.comp f.unop ι'.unop = CategoryStruct.comp g.unop ι'.unop) (h : ι = ι') : (ofι ι w).unop ≅ Cofork.ofπ ι'.unop w'

The canonical isomorphism between (Fork.ofι ι w).unop and Cofork.ofπ ι.unop w.unop.

def CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : C} {f g : X ⟶ Y} (ι ι' : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (w' : CategoryStruct.comp f.op ι'.op = CategoryStruct.comp g.op ι'.op) (h : ι = ι') : IsLimit (ofι ι w) ≃ IsColimit (Cofork.ofπ ι'.op w')

Fork.ofι ι w is a limit cone if and only if Cofork.ofπ ι'.op w' in the opposite category is a colimit cocone.

def CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop {C : Type u₁} [Category.{v₁, u₁} C] {X Y P : Cᵒᵖ} {f g : X ⟶ Y} (ι ι' : P ⟶ X) (w : CategoryStruct.comp ι f = CategoryStruct.comp ι g) (w' : CategoryStruct.comp f.unop ι'.unop = CategoryStruct.comp g.unop ι'.unop) (h : ι = ι') : IsLimit (ofι ι w) ≃ IsColimit (Cofork.ofπ ι'.unop w')

Fork.ofι ι w is a limit cone in Cᵒᵖ if and only if Cofork.ofπ ι.unop w.unop in C is a colimit cocone.

def CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkOpPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [HasPullback f f] [HasPushout f.op f.op] : IsColimit (ofπ f ⋯) ≃ IsLimit (Fork.ofι f.op ⋯)

Cofork.ofπ f pullback.condition is a colimit cocone if and only if Fork.ofι f.op pushout.condition in the opposite category is a limit cone.

def CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkUnopPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} [HasPullback f f] [HasPushout f.unop f.unop] : IsColimit (ofπ f ⋯) ≃ IsLimit (Fork.ofι f.unop ⋯)

Cofork.ofπ f pullback.condition is a colimit cocone in Cᵒᵖ if and only if Fork.ofι f.unop pushout.condition in C is a limit cone.

def CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkOpPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [HasPushout f f] [HasPullback f.op f.op] : IsLimit (ofι f ⋯) ≃ IsColimit (Cofork.ofπ f.op ⋯)

Fork.ofι f pushout.condition is a limit cone if and only if Cofork.ofπ f.op pullback.condition in the opposite category is a colimit cocone.

def CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkUnopPullback {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f : X ⟶ Y} [HasPushout f f] [HasPullback f.unop f.unop] : IsLimit (ofι f ⋯) ≃ IsColimit (Cofork.ofπ f.unop ⋯)

Fork.ofι f pushout.condition is a limit cone in Cᵒᵖ if and only if Cofork.ofπ f.op pullback.condition in C is a colimit cocone.