homologySequence_epi_shift_map_mor₂_iff

English

A family of connecting morphisms δ indexed by shifts forms a coherent long exact sequence.

Русский

Семейство соединяющих морфизмов δ, индексируемых сдвигами, образует непрерывную длинную точную последовательность.

LaTeX

$$$\{\delta_T^n\}_{n\in \mathbb Z}$ define a long exact sequence after applying F$$

Lean4

theorem homologySequence_epi_shift_map_mor₂_iff : Epi ((F.shift n₀).map T.mor₂) ↔ F.homologySequenceδ T n₀ n₁ h = 0 :=
  (F.homologySequence_exact₃ T hT n₀ n₁ h).epi_f_iff

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