mappingConeCompHomotopyEquiv_comm₁

English

There is a homotopy equivalence between mappingCone g and mappingCone (mappingConeCompTriangle f g).mor1 that respects the cone-structure, yielding a compatible identification of cones.

Русский

Существует гомотопическая эквивалентность между mappingCone g и mappingCone (mappingConeCompTriangle f g).mor1, которая согласуется с конусной структурой и обеспечивает совместное узнавание конусов.

LaTeX

$$$\text{HomotopyEquiv}(\mathrm{mappingCone}(g), \mathrm{mappingCone}(\mathrm{mappingConeCompTriangle}(f,g).mor_1))$$$

Lean4

@[reassoc]
theorem mappingConeCompHomotopyEquiv_comm₁ :
    inr (map f (f ≫ g) (𝟙 X₁) g (by rw [id_comp])) ≫ (mappingConeCompHomotopyEquiv f g).inv =
      (mappingConeCompTriangle f g).mor₂ :=
  by simp [map, mappingConeCompHomotopyEquiv, MappingConeCompHomotopyEquiv.inv]

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