English
In degree one, δ maps a boundary described by z and y to the boundary described by x in H_1 via the chains iso identifications, factoring through chains Iso at X1 and X3.
Русский
На степени единицы δ переводит границу, заданную z и y, в границу, заданную x в H_1 через цепные изоморфизмы X1 и X3.
LaTeX
$$$\delta hX 2 1 rfl (H2\pi X.X_3 z) = H1\pi X.X_1 ⟨x, mem\_cycles₁\_of\_comp\_eq\_d\_₂₁ hX hx⟩$$$
Lean4
theorem δ₁_apply (z : cycles₂ X.X₃) (y : G × G →₀ X.X₂)
(hy : mapRange.linearMap X.g.hom.hom y = z.1)
-- Let `x` be a 1-chain for `X₁` such that `f ∘ x = d(y)`.
(x : G →₀ X.X₁) (hx : mapRange.linearMap X.f.hom.hom x = d₂₁ X.X₂ y) :
-- Then `x` is a 1-cycle and `δ z = x` in `H₁(X₁)`.
δ hX 2 1 rfl (H2π X.X₃ z) = H1π X.X₁ ⟨x, mem_cycles₁_of_comp_eq_d₂₁ hX hx⟩ := by
simpa only [H2π, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply, H1π, ← cyclesMk₂_eq X.X₃,
← cyclesMk₁_eq X.X₁] using
δ_apply hX (i := 2) (j := 1) 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])
