rotateHomotopyEquiv_comm₂ — Mathlib

English

A higher-order commutation showing the compatibility of rotateHomotopyEquiv with the mapping cone in the homotopy category.

Русский

Высокий уровень согласованности поворота rotateHomotopyEquiv с отображающим конусом в гомотопической категории.

LaTeX

$$$rotateHomotopyEquiv_comm₂ : (HomotopyCategory.quotient).map( triangle φ ).mor_3 \\circ (rotateHomotopyEquiv φ).hom = (HomotopyCategory.quotient).map( inr (inr φ) )$$$

Lean4

@[reassoc (attr := simp)]
theorem rotateHomotopyEquiv_comm₂ :
    (HomotopyCategory.quotient _ _).map (triangle φ).mor₃ ≫
        (HomotopyCategory.quotient _ _).map (rotateHomotopyEquiv φ).hom =
      (HomotopyCategory.quotient _ _).map (inr (inr φ)) :=
  by simpa only [Functor.map_comp] using HomotopyCategory.eq_of_homotopy _ _ (rotateHomotopyEquivComm₂Homotopy φ)

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