mapShortComplex₃ — Mathlib

English

From a short exact sequence 0 → X1 → X2 → X3 → 0, there is a short complex H_i(G, X2) → H_i(G, X3) → H_j(G, X1) obtained by applying the i-th homology functor to the sequence with indices rotated appropriately.

Русский

Из короткой точной последовательности 0 → X1 → X2 → X3 → 0 получается короткий комплекс H_i(G, X2) → H_i(G, X3) → H_j(G, X1), полученный применением i-й гомологии к переставленной последовательности.

LaTeX

$$$mapShortComplex₃ hX hij$$$

Lean4

/-- The short complex `Hᵢ(G, X₂) ⟶ Hᵢ(G, X₃) ⟶ Hⱼ(G, X₁)` associated to an exact sequence of
representations `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`. -/
noncomputable abbrev mapShortComplex₃ {i j : ℕ} (hij : j + 1 = i) :=
  (snakeInput (map_chainsFunctor_shortExact hX) _ _ hij).L₁'

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