hasKernel — Mathlib

English

For φ, with τ2 iso and τ1 epi, the map opcyclesMap' φ h1 h2 is an isomorphism (under right homology data).

Русский

Для φ с τ2 изоморфизмом и τ1 эпиморфизмом карта opcyclesMap' φ h1 h2 является изоморфизмом (при наявности правой гомологии).

LaTeX

$$$\\text{IsIso}(\\mathrm{opcyclesMap}'\\ φ\\ h_1\\ h_2)$$$

Lean4

theorem hasKernel [S.HasRightHomology] [HasCokernel S.f] : HasKernel (cokernel.desc S.f S.g S.zero) :=
  by
  let h := S.rightHomologyData
  haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩
  let e : parallelPair (cokernel.desc S.f S.g S.zero) 0 ≅ parallelPair h.g' 0 :=
    parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) h.hp) (Iso.refl _)
      (coequalizer.hom_ext (by simp)) (by simp)
  exact hasLimit_of_iso e.symm

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