English
The positive-degree homology isomorphism is defined by composing restrictionIsos with homology maps and isomorphisms coming from restrictionGEIso.
Русский
Определение изоморфизма гомологии в положительных степенях через композицию ограничений и изоморфизмов гомологии.
LaTeX
$$homologyIsoPos (n) (m) [has] : h.cochainComplex.homology m ≅ L.homology (n+1)$$
Lean4
/-- Given `h : ConnectData K L` and `n : ℕ`, the homology
of `h.cochainComplex` in degree `n + 1` identifies to the homology of `L` in degree `n + 1`. -/
noncomputable def homologyIsoPos (n : ℕ) (m : ℤ) [h.cochainComplex.HasHomology m] [L.HasHomology (n + 1)]
(hm : m = (n + 1 : ℕ)) : h.cochainComplex.homology m ≅ L.homology (n + 1) :=
have := hasHomology_of_iso h.restrictionGEIso.symm (n + 1)
(h.cochainComplex.restrictionHomologyIso (ComplexShape.embeddingUpIntGE 0) n (n + 1) (n + 2) (by simp) (by simp)
(i' := m - 1) (j' := m) (k' := m + 1) (by simp; cutsat) (by simp; cutsat) (by simp; cutsat) (by simp)
(by simp)).symm ≪≫
HomologicalComplex.homologyMapIso h.restrictionGEIso (n + 1)
