invRotate_distinguished_triangle'

English

The inverse rotation of a distinguished triangle is still distinguished, via a sequence of shifts and rotations.

Русский

Обратное вращение выделенного треугольника также выделено, с помощью последовательности сдвигов и вращений.

LaTeX

$$$ T \\mapsto T^{-1}\\text{ rotated} \\in \\text{distinguishedTriangles}$$$

Lean4

theorem invRotate_distinguished_triangle' (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ)))
    (hT : T ∈ distinguishedTriangles C) : T.invRotate ∈ distinguishedTriangles C :=
  isomorphic_distinguished _
    (shift_distinguished_triangle _ (rotate_distinguished_triangle' _ (rotate_distinguished_triangle' _ hT)) _) _
    ((invRotateIsoRotateRotateShiftFunctorNegOne _).app T)

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