Iterated loop spaces
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-03-10.
Last modified on 2025-02-27.
module synthetic-homotopy-theory.iterated-loop-spaces where
Imports
open import elementary-number-theory.natural-numbers open import foundation.iterating-functions open import foundation.universe-levels open import structured-types.h-spaces open import structured-types.pointed-types open import synthetic-homotopy-theory.loop-spaces
Idea
The
iterated loop space¶
ΩⁿA
of a pointed type A
is obtained by
iteratively applying the
loop space operation Ω
to A
.
Definitions
Iterated loop spaces
module _ {l : Level} where iterated-loop-space : ℕ → Pointed-Type l → Pointed-Type l iterated-loop-space n = iterate n Ω type-iterated-loop-space : ℕ → Pointed-Type l → UU l type-iterated-loop-space n A = type-Pointed-Type (iterated-loop-space n A) point-iterated-loop-space : (n : ℕ) (A : Pointed-Type l) → type-iterated-loop-space n A point-iterated-loop-space n A = point-Pointed-Type (iterated-loop-space n A)
Iterated loop spaces of H-spaces
module _ {l : Level} where iterated-loop-space-H-Space : ℕ → H-Space l → H-Space l iterated-loop-space-H-Space zero-ℕ X = X iterated-loop-space-H-Space (succ-ℕ n) X = Ω-H-Space (iterated-loop-space n (pointed-type-H-Space X))
See also
External links
- Loop space on Wikidata
- Function iteration on Wikidata
Recent changes
- 2025-02-27. Egbert Rijke and Fredrik Bakke. Cleaning up for homotopy groups (#836).
- 2024-03-23. Egbert Rijke. Deloopings and Eilenberg-Mac Lane spaces (#1079).
- 2023-10-22. Egbert Rijke and Fredrik Bakke. Refactor synthetic homotopy theory (#654).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497).