homologySequence_mono_shift_map_mor₁_iff

English

The δ morphisms provide exactness in a family of triangles after shifting.

Русский

Mорфизм δ обеспечивает точность в семействе треугольников после сдвигов.

LaTeX

$$$\forall T \in \operatorname{distTriang}(C),\ \forall n_0,n_1,\ h\,\text{ with } n_0+1=n_1,\ (F.shift n_0).shifted δ = 0$$$

Lean4

theorem homologySequence_mono_shift_map_mor₁_iff : Mono ((F.shift n₁).map T.mor₁) ↔ F.homologySequenceδ T n₀ n₁ h = 0 :=
  (F.homologySequence_exact₁ T hT n₀ n₁ h).mono_g_iff

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