mem_distinguishedTriangles_iff' — Mathlib

English

There is an isomorphism connecting rotate of the inverse-triangle under triangleOpEquivalence with the rotated triangle in the opposite category.

Русский

Существует изоморфизм, связывающий вращение обратного треугольника с вращённым треугольником в противоположной категории.

LaTeX

$$$((triangleOpEquivalence C)^{-1}.obj T.rotate)^{\mathrm{unop}}.rotate \cong ((triangleOpEquivalence C)^{-1}.obj T)^{\mathrm{unop}}$$$

Lean4

theorem mem_distinguishedTriangles_iff' (T : Triangle Cᵒᵖ) :
    T ∈ distinguishedTriangles C ↔
      ∃ (T' : Triangle C) (_ : T' ∈ distTriang C),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T')) :=
  by
  rw [mem_distinguishedTriangles_iff]
  constructor
  · intro hT
    exact ⟨_, hT, ⟨(triangleOpEquivalence C).counitIso.symm.app T⟩⟩
  · rintro ⟨T', hT', ⟨e⟩⟩
    refine isomorphic_distinguished _ hT' _ ?_
    exact
      Iso.unop
        ((triangleOpEquivalence C).unitIso.app (Opposite.op T') ≪≫ (triangleOpEquivalence C).inverse.mapIso e.symm)

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