mem_mapTriangle_essImage_of_distinguished

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⟩⟩

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