English
For a given iso e: F1 ≅ F2, there is a canonical iso between F1.mapTriangle and F2.mapTriangle compatible with commShift.
Русский
Для данного изоморфизма e: F1 ≅ F2 существует каноническое изоморфление между F1.mapTriangle и F2.mapTriangle, совместимое с commShift.
LaTeX
$$mapTriangleIso e$$
Lean4
theorem mem_mapTriangle_essImage_of_distinguished [F.IsTriangulated] [F.mapArrow.EssSurj] (T : Triangle D)
(hT : T ∈ distTriang D) : ∃ (T' : Triangle C) (_ : T' ∈ distTriang C), Nonempty (F.mapTriangle.obj T' ≅ T) :=
by
obtain ⟨X, Y, f, e₁, e₂, w⟩ :
∃ (X Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁) (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁ :=
by
let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩
obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f
exact ⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩