English
For a short exact sequence 0 → X1 → X2 → X3 → 0, the i-th homology functor yields a map H_i(G, X1) → H_i(G, X2) → H_i(G, X3). This defines a short complex of i-th homology groups.
Русский
Для короткой точной последовательности 0 → X1 → X2 → X3 → 0 гомология по i-й степени даёт отображения H_i(G, X1) → H_i(G, X2) → H_i(G, X3). Это образует короткий комплекс групп гомологии.
LaTeX
$$$mapShortComplex₂ X i: H_i(G, X_1) \to H_i(G, X_2) \to H_i(G, X_3)$$$
Lean4
/-- Given an exact sequence of `G`-representations `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0`, this expresses an
`n`-chain `x : Gⁿ →₀ X₁` such that `f ∘ x ∈ Bₙ(G, X₂)` as a cycle. Stated for readability of
`δ_apply`. -/
noncomputable abbrev cyclesMkOfCompEqD {i j : ℕ} {y : (Fin i → G) →₀ X.X₂} {x : (Fin j → G) →₀ X.X₁}
(hx : mapRange.linearMap X.f.hom.hom x = (inhomogeneousChains X.X₂).d i j y) : cycles X.X₁ j :=
cyclesMk j _ rfl x <| by
simpa using (map_chainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x (by simpa using hx) _
