kernelOpUnop — Mathlib

Lean4
/-- The kernel of `f.op` is the opposite of `cokernel f`. -/
@[simps]
def kernelOpUnop : (kernel f.op).unop ≅ cokernel f
    where
  hom := (kernel.lift f.op (cokernel.π f).op <| by simp [← op_comp]).unop
  inv :=
    cokernel.desc f (kernel.ι f.op).unop <|
      by
      rw [← f.unop_op, ← unop_comp, f.unop_op]
      simp
  hom_inv_id := by
    rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]
    congr 1
    ext
    simp [← op_comp]
  inv_hom_id := by
    ext
    simp [← unop_comp]
      -- TODO: Generalize (this will work whenever f has a kernel)
      -- (The abelian case is probably sufficient for most applications.)
Похожие утверждения