English
The object mappingConeCompTriangleh(f,g) forms, together with the associated morphisms, a distinguished triangle in the triangulated structure of the HomotopyCategory.
Русский
Объект mappingConeCompTriangleh(f,g), вместе с сопутствующими морфизмами, образует выделенный треугольник в триангулированной структуре HomotopyCategory.
LaTeX
$$$\text{mappingConeCompTriangleh}(f,g) \in \text{distinguishedTriangles}$$$
Lean4
@[reassoc (attr := simp)]
theorem mappingConeCompTriangleh_comm₁ :
(mappingConeCompTriangleh f g).mor₂ ≫ (HomotopyCategory.quotient _ _).map (mappingConeCompHomotopyEquiv f g).hom =
(HomotopyCategory.quotient _ _).map (mappingCone.inr _) :=
by
rw [← cancel_mono (HomotopyCategory.isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).inv, assoc]
dsimp [mappingConeCompTriangleh]
rw [← Functor.map_comp, ← Functor.map_comp, ← Functor.map_comp, mappingConeCompHomotopyEquiv_hom_inv_id, comp_id,
mappingConeCompHomotopyEquiv_comm₁ f g, mappingConeCompTriangle_mor₂]
