composableArrows₂ — Mathlib

English

Under the standard hypotheses, a compatibility equation holds tying lifted cycles through δ to lifted cycles on the other side of the short exact sequence.

Русский

При стандартных гипотезах выполняется совместимость через δ между поднятыми циклами и поднятыми циклами на другой стороне короткого точного ряда.

LaTeX

$$x_3 ≫ hS.δ i j hij = x_1 ≫ S.X₁.homologyπ j$$

Lean4

/-- The (exact) sequence `S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i` -/
@[simp]
noncomputable def composableArrows₂ (i : ι) : ComposableArrows C 2 :=
  mk₂ (homologyMap S.f i) (homologyMap S.g i)

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