English
The (n+1)-dimensional loop space is homeomorphic to the loop space of n-dimensional loops with base point const.
Русский
Пространство петлей размерности n+1 гомеоморфно пространству петлей размерности n с базовой точкой const.
LaTeX
$$loopHomeo(i) : Ω^N X x ≃ₜ Ω(Ω^{j//j≠i} X x) const$$
Lean4
/-- The `n+1`-dimensional loops are in bijection with the loops in the space of
`n`-dimensional loops with base point `const`.
We allow an arbitrary indexing type `N` in place of `Fin n` here. -/
@[simps]
def loopHomeo (i : N) : Ω^ N X x ≃ₜ Ω (Ω^ { j // j ≠ i } X x) const
where
toFun := toLoop i
invFun := fromLoop i
left_inv p := by ext; exact congr_arg p (by dsimp; exact Equiv.apply_symm_apply _ _)
right_inv := to_from i
continuous_toFun := continuous_toLoop i
continuous_invFun := continuous_fromLoop i
