isHomological_of_localization — Mathlib

English

The homological kernel of a homological functor forms a triangulated substructure.

Русский

Гомологическое ядро гомологического функторa образует треугольную подструктуру.

LaTeX

$$$F.homologicalKernel.IsTriangulated$$$

Lean4

theorem isHomological_of_localization (L : C ⥤ D) [L.CommShift ℤ] [L.IsTriangulated] [L.mapArrow.EssSurj] (F : D ⥤ A)
    (G : C ⥤ A) (e : L ⋙ F ≅ G) [G.IsHomological] : F.IsHomological :=
  by
  have : F.PreservesZeroMorphisms :=
    preservesZeroMorphisms_of_map_zero_object (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)
  have : (L ⋙ F).IsHomological := IsHomological.of_iso e.symm
  refine IsHomological.mk' _ (fun T hT => ?_)
  rw [L.distTriang_iff] at hT
  obtain ⟨T₀, e, hT₀⟩ := hT
  exact ⟨L.mapTriangle.obj T₀, e, (L ⋙ F).map_distinguished_exact _ hT₀⟩

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