ofπOp — Mathlib

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