Documentation

TauCeti.AlgebraicTopology.UniversalCover.RealProjective.FundamentalGroup.Basic

The fundamental group of real projective space #

For 2 ≤ n, real projective n-space RPⁿ has fundamental group isomorphic to ℤˣ via the two-sheeted antipodal quotient mk n.

The antipodal cover is a regular covering map with deck group ℤˣ, and the covering sphere Sⁿ is simply connected for 2 ≤ n by TauCeti.simplyConnectedSpace_sphere_euclideanSpace. The regular-cover comparison TauCeti.Deck.IsRegular.fundamentalGroupDeckEquiv therefore identifies the fundamental group of RPⁿ at any basepoint with the deck group itself (the opposite drops out because the deck group is commutative), yielding

FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ.

As consequences, RPⁿ (for 2 ≤ n) has a fundamental group of order 2, a nontrivial fundamental group, is not simply connected, not contractible, and not homeomorphic to ℝ.

Main declarations #

References #

This is the deck-to-fundamental-group part of the computation of π₁(RPⁿ). It consumes TauCeti.RealProjectiveSpace.isQuotientCoveringMap_mk and TauCeti.RealProjectiveSpace.deckMulEquiv from TauCeti.AlgebraicTopology.UniversalCover.RealProjective.Deck, the simple connectivity of the covering sphere from TauCeti.AlgebraicTopology.Sphere.SimplyConnected, and the regular-cover comparison TauCeti.Deck.IsRegular.fundamentalGroupEquiv. The equivalence construction and monodromy proof pattern are adapted from TauCeti.AlgebraicTopology.UniversalCover.Circle.FundamentalGroup for the antipodal cover.

source
noncomputable def TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv (n : ℕ) (hn : 2 ≤ n) {x : RealProjectiveSpace n} (e : ↑(mk n ⁻¹' {x})) :
FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ

The fundamental group of real projective space RPⁿ (for 2 ≤ n) is isomorphic to ℤˣ, for any basepoint x with a chosen lift e in the sphere: FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv_apply_eq_iff (n : ℕ) (hn : 2 ≤ n) {x : RealProjectiveSpace n} (e : ↑(mk n ⁻¹' {x})) (γ : FundamentalGroup (RealProjectiveSpace n) x) (u : ℤˣ) :
    (fundamentalGroupMulEquiv n hn e) γ = u ↔ ↑(⋯.monodromy γ e) = u • ↑e

    Characterization of the element of ℤˣ assigned by fundamentalGroupMulEquiv: a loop class γ maps to u : ℤˣ exactly when its monodromy translate of the chosen lift e is u • (e : sphere _ 1).

    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.monodromy_fundamentalGroupMulEquiv_symm (n : ℕ) (hn : 2 ≤ n) {x : RealProjectiveSpace n} (e : ↑(mk n ⁻¹' {x})) (u : ℤˣ) :
    ↑(⋯.monodromy ((fundamentalGroupMulEquiv n hn e).symm u) e) = u • ↑e

    The inverse equivalence sends an integer unit u to the loop class whose monodromy translates the chosen lift by u.

    source
    theorem TauCeti.RealProjectiveSpace.fundamentalGroupMulEquiv_eq_one_iff (n : ℕ) (hn : 2 ≤ n) {x : RealProjectiveSpace n} (e : ↑(mk n ⁻¹' {x})) (γ : FundamentalGroup (RealProjectiveSpace n) x) :
    (fundamentalGroupMulEquiv n hn e) γ = 1 ↔ ⋯.monodromy γ e = e

    A loop class maps to 1 under the fundamental group equivalence exactly when its monodromy fixes the chosen lift.

    source
    noncomputable def TauCeti.RealProjectiveSpace.fundamentalGroupMulEquivAt (n : ℕ) (hn : 2 ≤ n) (x : RealProjectiveSpace n) :
    FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ

    The fundamental group of real projective space RPⁿ (for 2 ≤ n) is isomorphic to ℤˣ for any basepoint x: FundamentalGroup (RealProjectiveSpace n) x ≃* ℤˣ.

    Equations
    Instances For
      source
      theorem TauCeti.RealProjectiveSpace.card_fundamentalGroup_of_two_le (n : ℕ) (hn : 2 ≤ n) (x : RealProjectiveSpace n) :
      Nat.card (FundamentalGroup (RealProjectiveSpace n) x) = 2

      For 2 ≤ n, the fundamental group of RPⁿ has exactly two elements.

      source
      theorem TauCeti.RealProjectiveSpace.nontrivial_fundamentalGroup (n : ℕ) (hn : 2 ≤ n) (x : RealProjectiveSpace n) :
      Nontrivial (FundamentalGroup (RealProjectiveSpace n) x)

      For 2 ≤ n, the fundamental group of RPⁿ is nontrivial.

      source
      theorem TauCeti.RealProjectiveSpace.not_simplyConnectedSpace (n : ℕ) (hn : 2 ≤ n) :
      ¬SimplyConnectedSpace (RealProjectiveSpace n)

      For 2 ≤ n, real projective space RPⁿ is not simply connected.

      source
      theorem TauCeti.RealProjectiveSpace.not_contractibleSpace (n : ℕ) (hn : 2 ≤ n) :
      ¬ContractibleSpace (RealProjectiveSpace n)

      For 2 ≤ n, real projective space RPⁿ is not contractible.

      source
      theorem TauCeti.RealProjectiveSpace.isEmpty_homeomorph_real (n : ℕ) (hn : 2 ≤ n) :
      IsEmpty (RealProjectiveSpace n ≃ₜ ℝ)

      For 2 ≤ n, real projective space RPⁿ is not homeomorphic to ℝ.