composableArrows₃ — Mathlib

English

Given an exact sequence of homological complexes 0 → X₁ ⟶ X₂ ⟶ X₃ → 0, the induced sequence at i, X₁.opcycles i → X₂.opcycles i ⟶ X₃.opcycles i → 0, is exact at X₂.opcycles i.

Русский

Для точной последовательности 0 → X₁ ⟶ X₂ ⟶ X₃ → 0 гомологических комплексов, соответствующая последовательность на уровне i: X₁.opcycles i → X₂.opcycles i ⟶ X₃.opcycles i → 0, точна на X₂.opcycles i.

LaTeX

$$$(\text{ShortComplex.mk}(opcyclesMap\,f\,i,\; opcyclesMap\,g\,i,\; \text{by rw...})).Exact$$$

Lean4

/-- The diagram `K.homology i ⟶ K.opcycles i ⟶ K.cycles j ⟶ K.homology j`. -/
@[simp]
noncomputable def composableArrows₃ [K.HasHomology i] [K.HasHomology j] : ComposableArrows C 3 :=
  ComposableArrows.mk₃ (K.homologyι i) (K.opcyclesToCycles i j) (K.homologyπ j)

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