English
For x in cycles₁ A, H1π A x = 0 if and only if x lies in boundaries₁ A.
Русский
Для элемента x из cycles₁ A: H1π A x = 0 тогда и только тогда, когда x лежит в границах boundaries₁ A.
LaTeX
$$H1π_eq_zero_iff (x : cycles₁ A) : H1π A x = 0 ↔ x.1 ∈ boundaries₁ A$$
Lean4
theorem H1π_eq_zero_iff (x : cycles₁ A) : H1π A x = 0 ↔ x.1 ∈ boundaries₁ A :=
by
have h :=
leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
(leftHomologyData _) ((inhomogeneousChains A).sc 1).leftHomologyIso.hom
simp only [H1π, 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₁, shortComplexH1, cycles₁]
