exact_map_iff — Mathlib

English

For a LeftHomologyData h and a functor F preserving zero morphisms and left-homology, the map (S.map F) is exact iff F.obj h.H is zero.

Русский

Для данных левой гомологии h и функтор F, сохраняющий нули и левую гомологию, отображение (S.map F) точное тогда и только тогда, когда F.obj h.H равно нулю.

LaTeX

$$$ (S.map F).Exact \\iff IsZero (F.obj\, h.H) $$$

Lean4

theorem exact_map_iff (h : S.LeftHomologyData) (F : C ⥤ D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F]
    [(S.map F).HasHomology] : (S.map F).Exact ↔ IsZero (F.obj h.H) :=
  (h.map F).exact_iff

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