ofιUnop — Mathlib

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