instIsTriangulatedHomologicalKernel

English

For a homological functor F, the kernel is itself triangulated.

Русский

У ядра гомологического функторa F самовая структура треугольной категории.

LaTeX

$$$F.\text{homologicalKernel IsTriangulated}$$$

Lean4

instance : F.homologicalKernel.IsTriangulated
    where
  exists_zero := ⟨0, isZero_zero C, fun n ↦ (shiftFunctor C n ⋙ F).map_isZero (isZero_zero C)⟩
  toIsStableUnderShift := ⟨fun a ↦ ⟨fun X hX b ↦ (hX (a + b)).of_iso (F.mapIso ((shiftFunctorAdd C a b).app X).symm)⟩⟩
  toIsTriangulatedClosed₂ :=
    ObjectProperty.IsTriangulatedClosed₂.mk'
      (fun T hT h₁ h₃ n ↦
        (F.map_distinguished_exact _ (Triangle.shift_distinguished T hT n)).isZero_of_both_zeros ((h₁ n).eq_of_src _ _)
          ((h₃ n).eq_of_tgt _ _))

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