English
Describes the explicit formula for δ on a cocycle z and a cocycle y with hy, expressing δ(z) in terms of cocycles Mk and the boundary maps.
Русский
Дано явное формулы δ на кокцикла z и y c условиями hy, выражающее δ(z) через cocycles Mk и граничные отображения.
LaTeX
$$$\delta\_\text{apply}(hX,i,j,hij,z,hz,y,hy,x,hx) = \cdots$$$
Lean4
theorem δ_apply {i j : ℕ}
(hij : i + 1 = j)
-- Let `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0` be a short exact sequence of `G`-representations.
-- Let `z` be an `i`-cocycle for `X₃`
(z : (Fin i → G) → X.X₃)
(hz : (inhomogeneousCochains X.X₃).d i j z = 0)
-- Let `y` be an `i`-cochain for `X₂` such that `g ∘ y = z`
(y : (Fin i → G) → X.X₂)
(hy : (cochainsMap (MonoidHom.id G) X.g).f i y = z)
-- Let `x` be an `i + 1`-cochain for `X₁` such that `f ∘ x = d(y)`
(x : (Fin j → G) → X.X₁) (hx : X.f.hom ∘ x = (inhomogeneousCochains X.X₂).d i j y) :
-- Then `x` is an `i + 1`-cocycle and `δ z = x` in `Hⁱ⁺¹(X₁)`.
δ hX i j hij (π X.X₃ i <| cocyclesMk z (by subst hij; simpa using hz)) = π X.X₁ j (cocyclesMkOfCompEqD hX hx) := by
exact (map_cochainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x (by simpa using hx) (j + 1) (by simp)
