map_of_preservesLeftHomologyOf — Mathlib

English

If S is exact and F preserves zero morphisms and preserves left-homology of S (and hasHomology for S.map F), then (S.map F).Exact.

Русский

Если S точен и F сохраняет нулевые морфизмы, сохраняет левую гомологию S, и у S.map F есть гомология, то (S.map F).Exact.

LaTeX

$$$ (S.map F).Exact $$$

Lean4

theorem map_of_preservesLeftHomologyOf (h : S.Exact) (F : C ⥤ D) [F.PreservesZeroMorphisms]
    [F.PreservesLeftHomologyOf S] [(S.map F).HasHomology] : (S.map F).Exact :=
  by
  have := h.hasHomology
  rw [S.leftHomologyData.exact_iff, IsZero.iff_id_eq_zero] at h
  rw [S.leftHomologyData.exact_map_iff F, IsZero.iff_id_eq_zero, ← F.map_id, h, F.map_zero]

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