distinguished_cocone_triangle — Mathlib

English

The square involving F.mapTriangle.op, triangleOpEquivalence functors and F.op.mapTriangle is 2-commutative when F commutes with shifts.

Русский

Квадрат, содержащий F.mapTriangle.op, треугольниковые эквивалентности и F.op.mapTriangle, является 2-совместимым, когда F сохраняет сдвиги.

LaTeX

$$$CatCommSq(F.mapTriangle.op, (triangleOpEquivalence C).functor, (triangleOpEquivalence D).functor, F.op.mapTriangle)$$$

Lean4

theorem distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    ∃ (Z : Cᵒᵖ) (g : Y ⟶ Z) (h : Z ⟶ X⟦(1 : ℤ)⟧), Triangle.mk f g h ∈ distinguishedTriangles C :=
  by
  obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle₁ f.unop
  refine
    ⟨_, g.op, (opShiftFunctorEquivalence C 1).counitIso.inv.app (Opposite.op Z) ≫ (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op,
      ?_⟩
  simp only [mem_distinguishedTriangles_iff]
  refine Pretriangulated.isomorphic_distinguished _ H _ ?_
  exact
    Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
      (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))

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