Fundamental groups of real projective spaces in every dimension

The fundamental group of real projective space has three dimension ranges:

• RP⁰ is a point, so its fundamental group has one element;
• RP¹ is a circle, so its fundamental group is infinite cyclic;
• RPⁿ has a two-element fundamental group for 2 ≤ n.

The three group isomorphisms are constructed in the imported dimension-specific modules. This file records their common cardinality consequence. Recall that Nat.card is zero on an infinite type, so the value zero in dimension one expresses infinitude, not an empty fundamental group.

Main result

• TauCeti.RealProjectiveSpace.card_fundamentalGroup: the cardinality trichotomy 1, 0, 2 in dimensions 0, 1, ≥ 2, respectively.

Roadmap

This assembles the π₁(RPⁿ) application in Stage 4, item 13 of TauCetiRoadmap/UniversalCovers/README.md. The dimension-zero input is TauCeti.RealProjectiveSpace.Zero.fundamentalGroupMulEquiv; the circle case is TauCeti.RealProjectiveSpace.Line.fundamentalGroupMulEquiv; and the higher-dimensional input is TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv.

References

• A. Hatcher, Algebraic Topology, Section 1.1 and Corollary 1.15.

theorem TauCeti.RealProjectiveSpace.card_fundamentalGroup (n : ℕ) (x : RealProjectiveSpace n) : Nat.card (FundamentalGroup (RealProjectiveSpace n) x) = match n, x with | 0, x => 1 | 1, x => 0 | n.succ.succ, x => 2

The cardinality trichotomy for fundamental groups of real projective spaces.

The values are 1 in dimension zero, 0 in dimension one because that fundamental group is infinite, and 2 in every dimension at least two.