English
The connecting morphism δ applied to a boundary built from z and y matches the boundary of x, i.e., δ maps a chosen boundary corresponding to z, y to the boundary of x with hx, under the compatibility hx.
Русский
Переходное отображение δ, применённое к границе, построенной из z и y, совпадает с границей x при совместимости hx.
LaTeX
$$$\delta hX i j hij(\pi X.X_3 i (\text{cyclesMk } i j (\, \cdots \nobreak\\ z \, (\cdots) )) ) = \pi X.X_1 j (\text{cyclesMkOfCompEqD } hX hx)$$$
Lean4
theorem δ_apply {i j : ℕ}
(hij : j + 1 = i)
-- Let `0 ⟶ X₁ ⟶f X₂ ⟶g X₃ ⟶ 0` be a short exact sequence of `G`-representations.
-- Let `z` be an `j + 1`-cycle for `X₃`
(z : (Fin i → G) →₀ X.X₃)
(hz : (inhomogeneousChains X.X₃).d i j z = 0)
-- Let `y` be an `j + 1`-chain for `X₂` such that `g ∘ y = z`
(y : (Fin i → G) →₀ X.X₂)
(hy : (chainsMap (MonoidHom.id G) X.g).f i y = z)
-- Let `x` be an `j`-chain for `X₁` such that `f ∘ x = d(y)`
(x : (Fin j → G) →₀ X.X₁)
-- Then `x` is an `j`-cycle and `δ z = x` in `Hⱼ(X₁)`.
(hx : mapRange.linearMap X.f.hom.hom x = (inhomogeneousChains X.X₂).d i j y) :
δ hX i j hij (π X.X₃ i <| cyclesMk i j (by simp [← hij]) z (by simpa using hz)) =
π X.X₁ j (cyclesMkOfCompEqD hX hx) :=
by exact (map_chainsFunctor_shortExact hX).δ_apply i j hij z hz y hy x (by simpa using hx) _ rfl
