English
The triangle obtained by rotating a degreewise split short complex is canonically isomorphic to the triangle attached to the split data via a specified iso.
Русский
Треугольник, полученный путём поворота короткой последовательности со структурой разложения по степеням, канонически изоморфен треугольнику, прикрепленному к данным разложения через заданный изоморфизм.
LaTeX
$$$\mathrm{triangleRotateIsoTriangleOfDegreewiseSplit}\; S\; \sigma :\; \mathrm{triangleRotateShortComplex}(S,\sigma) \cong \mathrm{trianglehOfDegreewiseSplit}(S,\sigma)$$$
Lean4
/-- A cochain of degree `n : ℤ` between to cochain complexes `F` and `G` consists
of a family of morphisms `F.X p ⟶ G.X q` whenever `p + n = q`, i.e. for all
triplets in `HomComplex.Triplet n`. -/
def Cochain :=
∀ (T : Triplet n), F.X T.p ⟶ G.X T.q
