English
Given an exact sequence 0 → X1 → X2 → X3 → 0, one can construct an explicit cocycle in X1 from a cochain in X2 whose image under f equals a given cochain in X3; this yields an element of cocycles in X1.
Русский
Зная явное отображение коочейна, можно построить явный кокцикл в X1, соответствующий данным условиям; получаем элемент кокциколов в X1.
LaTeX
$$$\text{cocyclesMkOfCompEqD}:\; \text{the construction } x \mapsto \text{cocycles}(x)\in \mathrm{cocycles}(X_1, j)$$$
Lean4
/-- Given an exact sequence of `G`-representations `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0`, this expresses an
`n + 1`-cochain `x : Gⁿ⁺¹ → X₁` such that `f ∘ x ∈ Bⁿ⁺¹(G, X₂)` as a cocycle.
Stated for readability of `δ_apply`. -/
noncomputable abbrev cocyclesMkOfCompEqD {i j : ℕ} {y : (Fin i → G) → X.X₂} {x : (Fin j → G) → X.X₁}
(hx : X.f.hom ∘ x = (inhomogeneousCochains X.X₂).d i j y) : cocycles X.X₁ j :=
cocyclesMk x <| by
simpa using ((map_cochainsFunctor_shortExact hX).d_eq_zero_of_f_eq_d_apply i j y x (by simpa using hx) (j + 1))
