English
There is a canonical isomorphism of triangles between the rotated triangleh φ and the triangleh of inr φ: (triangleh φ).rotate ≅ (triangleh (inr φ)).
Русский
Существует каноническое изоморфное равенство треугольников между повёрнутым треугольникомh φ и треугольникомh над inr φ: (triangleh φ).rotate ≅ (triangleh (inr φ)).
LaTeX
$$$ (\\mathrm{triangleh}(\\phi)).\\mathrm{rotate} \\cong \\mathrm{triangleh}(\\mathrm{inr}(\\phi)) $$$
Lean4
/-- The canonical isomorphism of triangles `(triangleh φ).rotate ≅ (triangleh (inr φ))`. -/
noncomputable def rotateTrianglehIso : (triangleh φ).rotate ≅ (triangleh (inr φ)) :=
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
(((HomotopyCategory.quotient C (ComplexShape.up ℤ)).commShiftIso (1 : ℤ)).symm.app K ≪≫
HomotopyCategory.isoOfHomotopyEquiv (rotateHomotopyEquiv φ))
(by simp) (by simp)
(by
dsimp
rw [CategoryTheory.Functor.map_id, comp_id, assoc, ← Functor.map_comp_assoc, rotateHomotopyEquiv_comm₃,
Functor.map_neg, Preadditive.neg_comp, Functor.commShiftIso_hom_naturality, Preadditive.comp_neg,
Iso.inv_hom_id_app_assoc])
