ofιOp — Mathlib

Lean4
/-- A limit kernel fork gives a colimit cokernel cofork in the opposite category -/
def ofιOp {K X Y : C} (i : K ⟶ X) {f : X ⟶ Y} (w : i ≫ f = 0) (h : IsLimit (KernelFork.ofι i w)) :
    IsColimit (CokernelCofork.ofπ i.op (show f.op ≫ i.op = 0 by rw [← op_comp, w, op_zero])) :=
  CokernelCofork.IsColimit.ofπ _ _ (fun x hx => (h.lift (KernelFork.ofι x.unop (Quiver.Hom.op_inj hx))).op)
    (fun _ _ => Quiver.Hom.unop_inj (Fork.IsLimit.lift_ι h))
    (fun x hx b hb =>
      Quiver.Hom.unop_inj
        (Fork.IsLimit.hom_ext h (by simpa only [Quiver.Hom.unop_op, Fork.IsLimit.lift_ι] using Quiver.Hom.op_inj hb)))
Похожие утверждения