homologySequenceComposableArrows₅_exact

English

Definition of a five-term exact object built from F-shifted morphisms and δ.

Русский

Определение пятёрочного точного объекта, собираемого из сдвинутых морфизмов F и δ.

LaTeX

$$$\text{HomologyComposableArrows}_5 := \text{mk}_{5} ( (F.shift n_0).map T.mor_1 ) ( (F.shift n_0).map T.mor_2 ) ( F.homologySequenceδ T n_0 n_1 h ) ( (F.shift n_1).map T.mor_1 ) ( (F.shift n_1).map T.mor_2 )$$$

Lean4

theorem homologySequenceComposableArrows₅_exact : (F.homologySequenceComposableArrows₅ T n₀ n₁ h).Exact :=
  exact_of_δ₀ (F.homologySequence_exact₂ T hT n₀).exact_toComposableArrows
    (exact_of_δ₀ (F.homologySequence_exact₃ T hT n₀ n₁ h).exact_toComposableArrows
      (exact_of_δ₀ (F.homologySequence_exact₁ T hT n₀ n₁ h).exact_toComposableArrows
        (F.homologySequence_exact₂ T hT n₁).exact_toComposableArrows))

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