English
In the degree zero specialization, the connecting morphism δ sends the cycle z to the chain x in H_0, matching the basepoint identifications via the H1 and H0 projections.
Русский
В нулевой степени переходное отображение δ отправляет цикл z в касательную цепь x в H_0, совпадая с идентификациями базовых точек через проекции H1 и H0.
LaTeX
$$$\delta hX 1 0 rfl (H1\pi X.X_3 z) = H0\pi X.X_1 x$$$
Lean4
theorem δ₀_apply (z : cycles₁ X.X₃) (y : G →₀ X.X₂)
(hy : mapRange.linearMap X.g.hom.hom y = z.1)
-- Let `x : X₁` be such that `f(x) = d(y)`.
(x : X.X₁) (hx : X.f.hom x = d₁₀ X.X₂ y) :
-- Then `δ z = x` in `H₀(X₁)`.
δ hX 1 0 rfl (H1π X.X₃ z) = H0π X.X₁ x := by
simpa only [H1π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H0π, ← cyclesMk₀_eq X.X₁,
← cyclesMk₁_eq X.X₃] using
δ_apply hX (i := 1) (j := 0) rfl ((chainsIso₁ X.X₃).inv z.1) (by simp) ((chainsIso₁ X.X₂).inv y)
(Finsupp.ext fun _ => by simp [chainsIso₁, ← hy]) ((chainsIso₀ X.X₁).inv x)
(Finsupp.ext fun _ => by simp [chainsIso₀, ← hx])
