preservesLeftHomology_of_zero_g — Mathlib

English

If S.f = 0 and the cokernel diagram is preserved by F, then F preserves the left homology of S.

Русский

Если S.f = 0 и диаграмма cokernel сохраняется F, тогда F сохраняет левую гомологию S.

LaTeX

$$$S.f = 0 \Rightarrow F.PreservesLeftHomologyOf S$$$

Lean4

/-- If a short complex `S` is such that `S.g = 0` and that the cokernel of `S.f` is preserved
by a functor `F`, then `F` preserves the left homology of `S`. -/
theorem preservesLeftHomology_of_zero_g (hg : S.g = 0) [PreservesColimit (parallelPair S.f 0) F] :
    F.PreservesLeftHomologyOf S :=
  ⟨fun h =>
    { g := by
        rw [hg]
        infer_instance
      f' := by
        have := h.isIso_i hg
        let e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
          parallelPair.ext (Iso.refl _) (asIso h.i) (by simp) (by simp)
        exact Limits.preservesColimit_of_iso_diagram F e.symm }⟩

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