trianglehRotateIsoTrianglehOfDegreewiseSplit

English

There is an isomorphism between the rotated triangle of a degreewise split cochain complex and the triangle built from the degreewise split data.

Русский

Существует изоморфизм между повёрнутым треугольником разложенного по степеням коцеп complex и треугольником, построенным из данных разложения по степеням.

LaTeX

$$$\text{trianglehRotateIsoTrianglehOfDegreewiseSplit}\; S\; \sigma :\; \text{triangleh}(S,\sigma) \cong \text{trianglehOfDegreewiseSplit}(S,\sigma)$$$

Lean4

/-- The triangle `(triangleh φ).rotate` is isomorphic to a triangle attached to a
degreewise split short exact sequence of cochain complexes. -/
noncomputable def trianglehRotateIsoTrianglehOfDegreewiseSplit :
    (triangleh φ).rotate ≅ trianglehOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ) :=
  (HomotopyCategory.quotient _ _).mapTriangleRotateIso.app _ ≪≫
    (HomotopyCategory.quotient _ _).mapTriangle.mapIso (triangleRotateIsoTriangleOfDegreewiseSplit φ)

Похожие утверждения