op_distinguished — Mathlib

English

Let C be a (classical) category with enough structure to form distinguished triangles. If T is a distinguished triangle in C, then its image under the triangle-opposite equivalence is a distinguished triangle in the opposite category Cᵒᵖ.

Русский

Пусть C — категория с достаточной структурой для существования выделенных треугольников. Если T является выделенным треугольником в C, то образ T под эквивалентностью противоположной категории Cᵒᵖ является выделенным треугольником в Cᵒᵖ.

LaTeX

$$$((\\triangleOpEquivalence C).functor.obj (Opposite.op\\,T)) \\in distTriang\\; C^{\\mathrm{op}}$$$

Lean4

theorem op_distinguished (T : Triangle C) (hT : T ∈ distTriang C) :
    ((triangleOpEquivalence C).functor.obj (Opposite.op T)) ∈ distTriang Cᵒᵖ :=
  by
  rw [mem_distTriang_op_iff']
  exact ⟨T, hT, ⟨Iso.refl _⟩⟩

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