rotate_distinguished_triangle — Mathlib

English

A reformulation of the previous statement in terms of opposite morphisms and their unop compositions, maintaining the same completion criteria for c.

Русский

Переформулировка предыдущего утверждения через противоположные морфизмы и их объединение через unop, с тем же условием дополнения c.

LaTeX

$$$\exists c:\, T_1.obj_3 \to T_2.obj_3,\; T_1.mor_2 \\circ c = b \\circ T_2.mor_2 \land \\; T_1.mor_3 \\circ a⟨1⟩' = c \\circ T_2.mor_3$$$

Lean4

theorem rotate_distinguished_triangle (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C :=
  by
  simp only [mem_distinguishedTriangles_iff,
    Pretriangulated.rotate_distinguished_triangle ((triangleOpEquivalence C).inverse.obj (T.rotate)).unop]
  exact distinguished_iff_of_iso (rotateTriangleOpEquivalenceInverseObjRotateUnopIso T).symm

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