English
For any 2-cycle x in A, H2π A x = 0 if and only if x is a boundary.
Русский
Для любого 2-цикла x в A, H2π A x = 0 тогда и только тогда, когда x является границей.
LaTeX
$$$H_2^{\\pi}(A)(x) = 0 \\iff x \\in \\partial_2 A.$$$
Lean4
theorem H2π_eq_zero_iff (x : cycles₂ A) : H2π A x = 0 ↔ x.1 ∈ boundaries₂ A :=
by
have h :=
leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
(leftHomologyData _) ((inhomogeneousChains A).sc 2).leftHomologyIso.hom
simp only [H2π, isoCycles₂, π, HomologicalComplex.homologyπ, homologyπ, cyclesMapIso'_inv, leftHomologyπ, ← h,
← leftHomologyMapIso'_inv, ModuleCat.hom_comp, LinearMap.coe_comp, Function.comp_apply,
map_eq_zero_iff _ ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]
simp [LinearMap.range_codRestrict, boundaries₂, shortComplexH2, cycles₂]
