mapShortComplex₁ — Mathlib

English

Given a short exact sequence 0 → X1 → X2 → X3 → 0, the associated first horizontal segment of the homology long exact sequence is a short complex H_i(G, X3) → H_j(G, X1) → H_j(G, X2).

Русский

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

LaTeX

$$$mapShortComplex1: H_i(G, X_3) \to H_j(G, X_1) \to H_j(G, X_2)$$$

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₂'

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