The infinite dimensional real projective space

Content created by Fredrik Bakke.

Created on 2025-05-18.
Last modified on 2025-05-18.

module synthetic-homotopy-theory.infinite-real-projective-space where
Imports 
open import foundation.universe-levels

open import group-theory.symmetric-concrete-groups

open import univalent-combinatorics.standard-finite-types

Idea

The infinite dimensional real projective space ℝP∞ is the classifying space of the symmetric group on a two-element type.

Definitions

As the delooping of a two-element type

ℝP∞ : UU (lsuc lzero)
ℝP∞ = classifying-type-symmetric-Concrete-Group (Fin-Set 2)

point-ℝP∞ : ℝP∞
point-ℝP∞ = shape-symmetric-Concrete-Group (Fin-Set 2)

As the sequential colimit of the finite dimensional real projective spaces

The infinite dimensional real projective space ℝP∞ may be realized as a sequential colimit of finite dimensional real projective spaces, see Section IV [BR17].

  ℝP⁻¹ ──→ ℝP⁰ ──→ ℝP¹ ──→ ℝP² ──→ ⋯ ──→ ℝPⁿ ──→ ℝPⁿ⁺¹ ──→ ⋯ ──→ ℝP∞

This remains to be formalized.

References

[BR17]
Ulrik Buchholtz and Egbert Rijke. The real projective spaces in homotopy type theory. In 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 8. IEEE, [Piscataway], NJ, 2017.

See also

Recent changes