English
Given two distinguished triangles T1 and T2 with morphisms a,b forming a commutative square fac, there exists a linking morphism c: T1.obj3 → T2.obj3 such that the two compatibility equations hold: T1.mor2 ≫ c = b ≫ T2.mor2 and T1.mor3 ≫ a⟦1⟧' = c ≫ T2.mor3.
Русский
Для двух выделенных треугольников T1 и T2 с морфизмами, образующими равнобедренный квадрат fac, существует связующий морфизм c: T1.obj3 → T2.obj3, удовлетворяющий двум совместимостям: T1.mor2 ≫ c = b ≫ T2.mor2 и T1.mor3 ≫ a⟦1⟧' = c ≫ T2.mor3.
LaTeX
$$$\\exists c: T_1.obj_3 \\to T_2.obj_3,\\; T_1.mor_2 \\circ c = b \\circ T_2.mor_2 \\;\\land\\; T_1.mor_3 \\circ a\\langle 1 \\rangle' = c \\circ T_2.mor_3$$$
Lean4
/-- If `φ : K ⟶ L` is a morphism of cochain complexes in `C` and `G : C ⥤ D` is an
additive functor, then the image by `G` of the triangle `triangle φ` identifies to
the triangle associated to the image of `φ` by `G`. -/
noncomputable def mapTriangleIso :
(G.mapHomologicalComplex (ComplexShape.up ℤ)).mapTriangle.obj (triangle φ) ≅
triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ) :=
by
refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (mapHomologicalComplexIso φ G) ?_ ?_ ?_
· dsimp
simp only [comp_id, id_comp]
· dsimp
rw [map_inr, id_comp]
· dsimp
simp only [CategoryTheory.Functor.map_id, comp_id, map_δ]
