rotate_distinguished_triangle' — Mathlib

English

As in 15346, the functorial mapping respects the triangle structure, yielding an isomorphism between mapped triangles.

Русский

Снова: отображение функториально сохраняет структуру треугольника, образуя изоморфизм между отображаемыми треугольниками.

LaTeX

$$$ (\\mathrm{mapTriangleIso} \\phi G) : \\; (\\mathrm{G.mapHomologicalComplex} (up \\mathbb{Z}))\\,\\mapsto \\; \\text{triangle} \\; (G.map(\\phi)) $$$

Lean4

theorem rotate_distinguished_triangle' (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT : T ∈ distinguishedTriangles C) : T.rotate ∈ distinguishedTriangles C :=
  by
  obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
  exact ⟨_, _, _, ⟨(rotate _).mapIso e ≪≫ CochainComplex.mappingCone.rotateTrianglehIso φ⟩⟩

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