covariantSequence_exact — Mathlib

English

Alternative formulation of covariant_sequence_exact₁'. The five-term exactness is established via ladder arguments and Ext-hom equivalences.

Русский

Альтернативная формулировка covariant_sequence_exact₁'. Доказано существование точности по лестничным аргументам и эквивалентностям Ext.

LaTeX

$$$(\\mathrm{covariantSequence\\_₁'})(X,hS)\\text{ is exact}$$$

Lean4

theorem covariantSequence_exact : (covariantSequence X hS n₀ n₁ h).Exact :=
  exact_of_δ₀ (covariant_sequence_exact₂' X hS n₀).exact_toComposableArrows
    (exact_of_δ₀ (covariant_sequence_exact₃' X hS n₀ n₁ h).exact_toComposableArrows
      (exact_of_δ₀ (covariant_sequence_exact₁' X hS n₀ n₁ h).exact_toComposableArrows
        (covariant_sequence_exact₂' X hS n₁).exact_toComposableArrows))

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