The fundamental group of zero-dimensional real projective space

Real projective zero-space is a single point: the unit sphere in ℝ¹ consists of two antipodal points, and the antipodal quotient identifies them. The sibling modules compute the fundamental group of RP¹ and of RPⁿ for 2 ≤ n; this file supplies the remaining boundary case.

The instance TauCeti.RealProjectiveSpace.instUniqueZero gives uniqueness directly. Mathlib's generic contractibility instance for a nonempty subsingleton space makes RP⁰ contractible and hence simply connected. It follows that the fundamental group at its unique point is the trivial group.

Main declarations

• TauCeti.RealProjectiveSpace.Zero.fundamentalGroupMulEquiv: the fundamental group of RP⁰ is the trivial group PUnit.
• TauCeti.RealProjectiveSpace.Zero.card_fundamentalGroup: the fundamental group has one element.

Roadmap

This closes the n = 0 boundary case of π₁(RPⁿ) in Stage 4, item 13 of TauCetiRoadmap/UniversalCovers/README.md. The n = 1 case is TauCeti.RealProjectiveSpace.Line.fundamentalGroupMulEquiv, while TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv covers 2 ≤ n.

References

• A. Hatcher, Algebraic Topology, Section 1.1.

noncomputable def TauCeti.RealProjectiveSpace.Zero.fundamentalGroupMulEquiv (x : RealProjectiveSpace 0) : FundamentalGroup (RealProjectiveSpace 0) x ≃* PUnit.{u_1 + 1}

The fundamental group of RP⁰ is trivial. At its unique basepoint it is isomorphic to the one-element group PUnit.

Equations

• TauCeti.RealProjectiveSpace.Zero.fundamentalGroupMulEquiv x = MulEquiv.ofUnique

theorem TauCeti.RealProjectiveSpace.Zero.card_fundamentalGroup (x : RealProjectiveSpace 0) : Nat.card (FundamentalGroup (RealProjectiveSpace 0) x) = 1

The fundamental group of RP⁰ has exactly one element.