English
For h connecting K and L, and natural n, there is an isomorphism between the homology of the cochain complex h.cochainComplex in degree m and the homology of L in degree n+1, provided m matches (n+1).
Русский
Для связующего h между K и L существует изоморфизм гомологии коцепного комплекса h.cochainComplex в степени m и гомологии L в степени n+1 при условии m = (n+1).
LaTeX
$$homologyIsoPos (n) (m) [h.cochainComplex.HasHomology m] [L.HasHomology (n+1)] (hm : m = (n+1)) : h.cochainComplex.homology m ≅ L.homology (n+1)$$
Lean4
/-- Given `h : ConnectData K L` where `K : ChainComplex C ℕ` and `L : CochainComplex C ℕ`,
this is the cochain complex indexed by `ℤ` obtained by connecting `K` and `L`:
`... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ...`. -/
@[simps]
def cochainComplex : CochainComplex C ℤ where
X := X K L
d := h.d
shape := h.shape
