English
For x ∈ cocycles₁ A, H1π A x = 0 iff x is in coboundaries.
Русский
Для x ∈ cocycles₁ A, H1π A x = 0 тогда и только тогда, когда x ∈ coboundaries₁ A.
LaTeX
$$theorem H1π_eq_zero_iff (x : cocycles₁ A) : H1π A x = 0 ↔ ⇑x ∈ coboundaries₁ A$$
Lean4
theorem H1π_eq_zero_iff (x : cocycles₁ A) : H1π A x = 0 ↔ ⇑x ∈ coboundaries₁ A :=
by
have h :=
leftHomologyπ_naturality'_assoc (isoShortComplexH1 A).inv (shortComplexH1 A).moduleCatLeftHomologyData
(leftHomologyData _) ((inhomogeneousCochains A).sc 1).leftHomologyIso.hom
simp only [H1π, isoCocycles₁, π, 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, coboundaries₁, shortComplexH1, cocycles₁]
