English
Let F: C → A be a functor that preserves zero morphisms. If for every distinguished triangle T in C there exists a distinguished triangle T′ isomorphic to T such that the image under F of the short complex associated to T′ is exact, then F is a homological functor.
Русский
Пусть F: C → A — гомологичный-функтор в смысле сохранения нулевых морфизмов. Если для каждого выделенного треугольника T в C существует выделенный треугольник T′, изоморфный T, и изоморешение e: T ≅ T′, так что образ под F соответствующего краткого комплекса T′ является точным, то F — гомологичный функтор.
LaTeX
$$$\text{Let }F: C \to A\text{ preserve zero morphisms and }\forall T\in \operatorname{distTriang}(C),\ \exists T'\ \text{with }T'\cong T\text{ such that }(\text{shortComplexOfDistTriangle }T'\,(\text{isomorphic_distinguished }\,\text{_}h_T\,\_e^{\text{symm}})).map F\text{ is Exact}.\ \Longrightarrow\ F\text{ is Homological}$$$
Lean4
theorem mk' [F.PreservesZeroMorphisms]
(hF :
∀ (T : Pretriangulated.Triangle C) (hT : T ∈ distTriang C),
∃ (T' : Pretriangulated.Triangle C) (e : T ≅ T'),
((shortComplexOfDistTriangle T' (isomorphic_distinguished _ hT _ e.symm)).map F).Exact) :
F.IsHomological where
exact T
hT := by
obtain ⟨T', e, h'⟩ := hF T hT
exact (ShortComplex.exact_iff_of_iso (F.mapShortComplex.mapIso ((shortComplexOfDistTriangleIsoOfIso e hT)))).2 h'
