The fundamental group of the real projective line is ℤ

For n = 1, real projective space RP¹ is homeomorphic to the circle Circle via TauCeti.RealProjectiveSpace.Line.homeomorphCircle.

Transporting the circle computation π₁(Circle, z) ≃* Multiplicative ℤ (Circle.fundamentalGroupMulEquiv) across RP¹ ≃ₜ Circle gives

π₁(RP¹, x) ≃* Multiplicative ℤ

at any basepoint x : RealProjectiveSpace 1.

For 2 ≤ n, the fundamental group computation is developed in the sibling module TauCeti.AlgebraicTopology.UniversalCover.RealProjective.FundamentalGroup.Basic, yielding π₁(RPⁿ) ≅ ℤˣ conditional on the simple-connectivity instance for Sⁿ.

Main declarations

• TauCeti.RealProjectiveSpace.Line.fundamentalGroupMulEquiv: π₁(RP¹, x) ≃* Multiplicative ℤ at any basepoint.
• TauCeti.RealProjectiveSpace.Line.nontrivial_fundamentalGroup: π₁(RP¹, x) is nontrivial.
• TauCeti.RealProjectiveSpace.Line.infinite_fundamentalGroup: π₁(RP¹, x) is infinite.
• TauCeti.RealProjectiveSpace.Line.card_fundamentalGroup: Nat.card (π₁(RP¹, x)) = 0, expressing infinitude under the Nat.card convention.
• TauCeti.RealProjectiveSpace.Line.not_simplyConnectedSpace: RP¹ is not simply connected.
• TauCeti.RealProjectiveSpace.Line.not_contractibleSpace: RP¹ is not contractible.

References

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, π₁(RPⁿ), by closing its n = 1 case.

noncomputable def TauCeti.RealProjectiveSpace.Line.fundamentalGroupMulEquiv (x : RealProjectiveSpace 1) : FundamentalGroup (RealProjectiveSpace 1) x ≃* Multiplicative ℤ

The fundamental group of the real projective line is infinite cyclic. The isomorphism is obtained by transporting the complex-circle computation across homeomorphCircle.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.RealProjectiveSpace.Line.fundamentalGroupMulEquiv_def (x : RealProjectiveSpace 1) : fundamentalGroupMulEquiv x = (FundamentalGroup.homeomorphMulEquiv homeomorphCircle x).trans (homeomorphCircle x).fundamentalGroupMulEquiv

fundamentalGroupMulEquiv factors as transport along homeomorphCircle : RP¹ ≃ₜ Circle, followed by the circle fundamental-group computation Circle.fundamentalGroupMulEquiv at the image basepoint.

theorem TauCeti.RealProjectiveSpace.Line.nontrivial_fundamentalGroup (x : RealProjectiveSpace 1) : Nontrivial (FundamentalGroup (RealProjectiveSpace 1) x)

The fundamental group of RP¹ at any basepoint is nontrivial.

theorem TauCeti.RealProjectiveSpace.Line.infinite_fundamentalGroup (x : RealProjectiveSpace 1) : Infinite (FundamentalGroup (RealProjectiveSpace 1) x)

The fundamental group of RP¹ at any basepoint is infinite.

@[simp]

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

The fundamental group of RP¹ has Nat.card zero because it is infinite.

theorem TauCeti.RealProjectiveSpace.Line.not_simplyConnectedSpace : ¬SimplyConnectedSpace (RealProjectiveSpace 1)

The real projective line is not simply connected.

theorem TauCeti.RealProjectiveSpace.Line.not_contractibleSpace : ¬ContractibleSpace (RealProjectiveSpace 1)

The real projective line is not contractible.