leftHomotopyClassEquivRightHomotopyClass

English

If X is cofibrant and Y is fibrant, then the functor sending a left-homotopy class to the corresponding right-homotopy class is an equivalence LH(X,Y) ≃ RH(X,Y).

Русский

Если X кофибрива, а Y фибривант, то отображение левого гомотопического класса в соответствующий правый класс образует эквиваленцию LH(X,Y) ≃ RH(X,Y).

LaTeX

$$$\mathrm{LeftHo}(X,Y) \cong \mathrm{RightHo}(X,Y)$$$

Lean4

/-- Left homotopy classes of maps `X ⟶ Y` identify to right homotopy classes
when `X` is cofibrant and `Y` is fibrant. -/
def leftHomotopyClassEquivRightHomotopyClass : LeftHomotopyClass X Y ≃ RightHomotopyClass X Y
    where
  toFun :=
    Quot.lift (fun f ↦ .mk f)
      (fun _ _ h ↦ by
        dsimp
        rw [RightHomotopyClass.mk_eq_mk_iff]
        exact h.rightHomotopyRel)
  invFun :=
    Quot.lift (fun f ↦ .mk f)
      (fun _ _ h ↦ by
        dsimp
        rw [LeftHomotopyClass.mk_eq_mk_iff]
        exact h.leftHomotopyRel)
  left_inv := by rintro ⟨f⟩; rfl
  right_inv := by rintro ⟨f⟩; rfl

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