composableArrows₅ — Mathlib

English

Definition of the pair of morphisms f_i, g_i forming the two-term exact sequence on i.

Русский

Определение пары морфизмов f_i, g_i образующей две стрелки точной последовательности на i.

LaTeX

$$composableArrows₂ S i$$

Lean4

/-- The (exact) sequence
`H_i(S.X₁) ⟶ H_i(S.X₂) ⟶ H_i(S.X₃) ⟶ H_j(S.X₁) ⟶ H_j(S.X₂) ⟶ H_j(S.X₃)` when `c.Rel i j`
and `S` is a short exact short complex of homological complexes in an abelian category. -/
@[simp]
noncomputable def composableArrows₅ (i j : ι) (hij : c.Rel i j) : ComposableArrows C 5 :=
  mk₅ (homologyMap S₁.f i) (homologyMap S₁.g i) (hS₁.δ i j hij) (homologyMap S₁.f j) (homologyMap S₁.g j)

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