hasCokernel — Mathlib

English

If S has left homology and kernel of g exists, then the cokernel of kernel.lift g f zero exists (constructed via an iso of parallel pairs).

Русский

Если у S есть левая гомология и существует ядро g, то как минимум коканал ядра lift g f zero существует (строится через изоморфизм пар-параллельных стрелок).

LaTeX

$$$HasCokernel\big(\ker\ellift g f 0\big)$$$

Lean4

theorem hasCokernel [S.HasLeftHomology] [HasKernel S.g] : HasCokernel (kernel.lift S.g S.f S.zero) :=
  by
  let h := S.leftHomologyData
  haveI : HasColimit (parallelPair h.f' 0) := ⟨⟨⟨_, h.hπ'⟩⟩⟩
  let e : parallelPair (kernel.lift S.g S.f S.zero) 0 ≅ parallelPair h.f' 0 :=
    parallelPair.ext (Iso.refl _) (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi) (by cat_disch) (by simp)
  exact hasColimit_of_iso e

Похожие утверждения