leftHomotopyRel_iff_rightHomotopyRel

English

For any morphisms f,g in a category with suitable model structure, LeftHomotopyRel f g is equivalent to RightHomotopyRel f g.

Русский

Для любых морфизмов f,g в категории с подходящей модельной структурой, левое отношение гомотопии эквивалентно правому отношению гомотопии.

LaTeX

$$LeftHomotopyRel f g ↔ RightHomotopyRel f g$$

Lean4

theorem leftHomotopyRel_iff_rightHomotopyRel {X Y : C} (f g : X ⟶ Y) [IsCofibrant X] [IsFibrant Y] :
    LeftHomotopyRel f g ↔ RightHomotopyRel f g :=
  ⟨fun h ↦ h.rightHomotopyRel, fun h ↦ h.leftHomotopyRel⟩

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