distinguishedTriangles — Mathlib

English

A triangulated F induces a triangulated F.op, with the appropriate transfer of distinguished triangles.

Русский

Триангулёванный функтор F индуцирует триангулёванный F.op с корректной передачей выделенных треугольников.

LaTeX

$$$F^{op}.IsTriangulated \Rightarrow F.IsTriangulated$$$

Lean4

/-- A triangle in `Cᵒᵖ` shall be distinguished iff it corresponds to a distinguished
triangle in `C` via the equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ`. -/
def distinguishedTriangles : Set (Triangle Cᵒᵖ) := fun T =>
  ((triangleOpEquivalence C).inverse.obj T).unop ∈ distTriang C

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