Documentation

TauCeti.AlgebraicTopology.UniversalCover.RealProjective.Deck

The deck group of the antipodal cover of real projective space #

The unit sphere Sⁿ covers real projective n-space as the quotient by the antipodal action of ℤˣ; TauCeti.RealProjectiveSpace.isQuotientCoveringMap_mk records this. This file identifies the deck transformation group of that cover.

The antipodal map is always a deck transformation, and it is never the identity because no unit vector is its own negative. Both facts are unconditional, and come from TauCeti.Deck.IsQuotientCoveringMap.toDeckHom, which turns an element of the acting group of a quotient covering map into a deck transformation, together with its injectivity TauCeti.Deck.IsQuotientCoveringMap.toDeckHom_injective.

For 1 ≤ n the sphere is connected, so a deck transformation is determined by its value at a single point, and TauCeti.Deck.IsQuotientCoveringMap.deckMulEquiv identifies the whole deck group with the two-element acting group:

Deck (mk n) ≃* ℤˣ.

The regularity of the antipodal cover needs no connectedness hypothesis.

For n = 0 the sphere is the two-point space S⁰, which is disconnected, so the argument does not apply; the statements that need it carry the hypothesis 1 ≤ n explicitly.

This advances TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13, the computation of π₁(RPⁿ): for a regular cover the deck group is a quotient of the fundamental group of the base, so knowing that the antipodal cover is regular with deck group of order two is the covering-space input to that computation.

Main declarations #

source
noncomputable def TauCeti.RealProjectiveSpace.antipode (n : ℕ) :
↥(Deck (mk n))

The antipodal map, as a deck transformation of the cover Sⁿ → RPⁿ. It is translation by the nontrivial integer unit.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.antipode_apply (n : ℕ) (x : ↑(Metric.sphere 0 1)) :
    ↑(antipode n) x = -x

    On points, the antipodal deck transformation negates.

    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.antipode_symm_apply (n : ℕ) (x : ↑(Metric.sphere 0 1)) :
    (↑(antipode n)).symm x = -x

    On points, the inverse of the antipodal deck transformation also negates.

    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.antipode_mul_self (n : ℕ) :
    antipode n * antipode n = 1

    The antipodal deck transformation is an involution.

    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.inv_antipode (n : ℕ) :
    (antipode n)⁻¹ = antipode n

    The antipodal deck transformation is its own inverse.

    source
    @[simp]
    theorem TauCeti.RealProjectiveSpace.antipode_ne_one (n : ℕ) :
    antipode n ≠ 1

    The antipodal deck transformation is not the identity: the nontrivial integer unit is not trivial, and translation is injective because the antipodal action is free.

    source
    noncomputable def TauCeti.RealProjectiveSpace.deckMulEquiv (n : ℕ) (hn : 1 ≤ n) :
    ℤˣ ≃* ↥(Deck (mk n))

    The deck group of the antipodal cover Sⁿ → RPⁿ is the two-element group ℤˣ, for 1 ≤ n. The isomorphism sends an integer unit to the corresponding antipodal translation.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.RealProjectiveSpace.deckMulEquiv_apply (n : ℕ) (hn : 1 ≤ n) (u : ℤˣ) (x : ↑(Metric.sphere 0 1)) :
      ↑((deckMulEquiv n hn) u) x = u • x

      On points, the deck-group isomorphism is the antipodal action.

      source
      @[simp]
      theorem TauCeti.RealProjectiveSpace.deckMulEquiv_symm_apply (n : ℕ) (hn : 1 ≤ n) (φ : ↥(Deck (mk n))) (x : ↑(Metric.sphere 0 1)) :
      (deckMulEquiv n hn).symm φ • x = ↑φ x

      On points, the inverse of the deck-group isomorphism recovers the given deck transformation.

      source
      @[simp]
      theorem TauCeti.RealProjectiveSpace.deckMulEquiv_neg_one (n : ℕ) (hn : 1 ≤ n) :
      (deckMulEquiv n hn) (-1) = antipode n

      The deck-group isomorphism sends the nontrivial integer unit to the antipodal map.

      source
      theorem TauCeti.RealProjectiveSpace.eq_one_or_eq_antipode (n : ℕ) (hn : 1 ≤ n) (φ : ↥(Deck (mk n))) :
      φ = 1 ∨ φ = antipode n

      For 1 ≤ n, a deck transformation of the antipodal cover is either the identity or the antipodal map.

      source
      theorem TauCeti.RealProjectiveSpace.card_deck (n : ℕ) (hn : 1 ≤ n) :
      Nat.card ↥(Deck (mk n)) = 2

      For 1 ≤ n, the deck group of the antipodal cover has exactly two elements.

      source
      theorem TauCeti.RealProjectiveSpace.isRegular_mk (n : ℕ) :
      Deck.IsRegular (mk n)

      The antipodal cover Sⁿ → RPⁿ is regular: its deck group acts transitively on every fibre. Unlike the identification of the deck group, this needs no connectedness.