Real projective space as an antipodal quotient

Real projective n-space is modelled as the quotient of the unit sphere in EuclideanSpace ℝ (Fin (n + 1)) by the antipodal action. The acting group is ℤˣ, whose two elements 1 and -1 act respectively as the identity and negation. This file defines the quotient, characterizes equality of its representatives, and proves that the quotient map from the sphere is a two-sheeted quotient covering map.

This is the quotient-cover prerequisite for the computation of π₁(RPⁿ) in TauCetiRoadmap/UniversalCovers/README.md, Stage 4, item 13. The covering argument uses isQuotientCoveringMap_quotientMk_of_properlyDiscontinuousSMul from Mathlib's quotient-covering API, due to Junyan Xu. Finiteness of ℤˣ supplies proper discontinuity; the only additional input is that the antipodal action on the unit sphere is free. The integer-unit sphere action is provided by TauCeti.Analysis.Normed.Module.Ball.IntUnitsAction.

Main declarations

• TauCeti.RealProjectiveSpace: real projective n-space as an antipodal quotient of Sⁿ.
• TauCeti.RealProjectiveSpace.instNonemptySphere and TauCeti.RealProjectiveSpace.connectedSpace_sphere: the covering sphere Sⁿ is nonempty, and connected once 1 ≤ n.
• TauCeti.RealProjectiveSpace.instCompactSpace: real projective space is compact.
• TauCeti.RealProjectiveSpace.inductionOn, TauCeti.RealProjectiveSpace.lift, and TauCeti.RealProjectiveSpace.lift_unique: elimination principles for the antipodal quotient.
• TauCeti.RealProjectiveSpace.mk_eq_mk_iff: two unit vectors define the same projective point exactly when they are equal or antipodal.
• TauCeti.RealProjectiveSpace.isQuotientCoveringMap_mk: the unit-sphere quotient is a quotient covering map with group ℤˣ.
• TauCeti.RealProjectiveSpace.isCoveringMap_mk: the underlying covering-map statement.
• TauCeti.RealProjectiveSpace.instUniqueZero: RP⁰ has exactly one point.
• TauCeti.RealProjectiveSpace.instPathConnectedSpace: RPⁿ is path-connected for every n.

def TauCeti.RealProjectiveSpace (n : ℕ) : Type

Real projective n-space, modelled as the orbit quotient of the unit sphere Sⁿ under the antipodal action of the two-element group ℤˣ = {1, -1}.

Equations

• TauCeti.RealProjectiveSpace n = Quotient (MulAction.orbitRel ℤˣ ↑(Metric.sphere 0 1))

instance TauCeti.RealProjectiveSpace.instNonemptySphere (n : ℕ) : Nonempty ↑(Metric.sphere 0 1)

The unit sphere of EuclideanSpace ℝ (Fin (n + 1)) is nonempty.

theorem TauCeti.RealProjectiveSpace.connectedSpace_sphere (n : ℕ) (hn : 1 ≤ n) : ConnectedSpace ↑(Metric.sphere 0 1)

The unit sphere of EuclideanSpace ℝ (Fin (n + 1)) is connected once 1 ≤ n, that is, from the circle S¹ on. This is the standing hypothesis behind the identification of the deck group of the antipodal cover.

@[instance_reducible]

instance TauCeti.RealProjectiveSpace.instTopologicalSpace (n : ℕ) : TopologicalSpace (RealProjectiveSpace n)

The quotient topology on real projective space.

Equations

• TauCeti.RealProjectiveSpace.instTopologicalSpace n = { IsOpen := TauCeti.RealProjectiveSpace.instTopologicalSpace._aux_1 n, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

instance TauCeti.RealProjectiveSpace.instCompactSpace (n : ℕ) : CompactSpace (RealProjectiveSpace n)

Real projective space is compact as the quotient of the compact unit sphere.

noncomputable def TauCeti.RealProjectiveSpace.mk (n : ℕ) : ↑(Metric.sphere 0 1) → RealProjectiveSpace n

The quotient map from the unit sphere to real projective space.

Equations

• TauCeti.RealProjectiveSpace.mk n = Quotient.mk (MulAction.orbitRel ℤˣ ↑(Metric.sphere 0 1))

theorem TauCeti.RealProjectiveSpace.mk_surjective (n : ℕ) : Function.Surjective (mk n)

Every point of real projective space has a unit-vector representative.

theorem TauCeti.RealProjectiveSpace.inductionOn (n : ℕ) {motive : RealProjectiveSpace n → Prop} (x : RealProjectiveSpace n) (h : ∀ (y : ↑(Metric.sphere 0 1)), motive (mk n y)) : motive x

To prove a property of every point of real projective space, it suffices to prove it on the image of every unit vector.

noncomputable def TauCeti.RealProjectiveSpace.lift (n : ℕ) {α : Sort u_1} (f : ↑(Metric.sphere 0 1) → α) (h : ∀ (x : ↑(Metric.sphere 0 1)), f (-x) = f x) : RealProjectiveSpace n → α

An antipodal-invariant function on the unit sphere descends to real projective space.

Equations

• TauCeti.RealProjectiveSpace.lift n f h = Quotient.lift f ⋯

@[simp]

theorem TauCeti.RealProjectiveSpace.lift_mk (n : ℕ) {α : Sort u_1} (f : ↑(Metric.sphere 0 1) → α) (h : ∀ (x : ↑(Metric.sphere 0 1)), f (-x) = f x) (x : ↑(Metric.sphere 0 1)) : RealProjectiveSpace.lift n f h (mk n x) = f x

Lifting an antipodal-invariant function and applying it to a representative recovers the original function.

theorem TauCeti.RealProjectiveSpace.lift_unique (n : ℕ) {α : Sort u_1} (f : ↑(Metric.sphere 0 1) → α) (h : ∀ (x : ↑(Metric.sphere 0 1)), f (-x) = f x) (g : RealProjectiveSpace n → α) (hg : ∀ (x : ↑(Metric.sphere 0 1)), g (mk n x) = f x) : g = RealProjectiveSpace.lift n f h

A function out of real projective space agreeing with an antipodal-invariant function on representatives is its lift.

@[simp]

theorem TauCeti.RealProjectiveSpace.mk_eq_mk_iff (n : ℕ) (x y : ↑(Metric.sphere 0 1)) : mk n x = mk n y ↔ x = y ∨ x = -y

Two unit vectors define the same point of real projective space exactly when they are equal or antipodal.

@[simp]

theorem TauCeti.RealProjectiveSpace.mk_neg (n : ℕ) (x : ↑(Metric.sphere 0 1)) : mk n (-x) = mk n x

Antipodal unit vectors have the same image in real projective space.

theorem TauCeti.RealProjectiveSpace.isQuotientCoveringMap_mk (n : ℕ) : IsQuotientCoveringMap (mk n) ℤˣ

The unit sphere modulo the antipodal action is a quotient covering map. Its fibres are the two-element orbits {x, -x}.

theorem TauCeti.RealProjectiveSpace.isQuotientMap_mk (n : ℕ) : Topology.IsQuotientMap (mk n)

The unit-sphere projection onto real projective space is a quotient map.

theorem TauCeti.RealProjectiveSpace.continuous_mk (n : ℕ) : Continuous (mk n)

The unit-sphere projection onto real projective space is continuous.

instance TauCeti.RealProjectiveSpace.instNonempty (n : ℕ) : Nonempty (RealProjectiveSpace n)

Real projective space is nonempty.

@[instance_reducible]

noncomputable instance TauCeti.RealProjectiveSpace.instUniqueZero : Unique (RealProjectiveSpace 0)

Zero-dimensional real projective space has exactly one point.

Equations

• TauCeti.RealProjectiveSpace.instUniqueZero = uniqueOfSubsingleton TauCeti.RealProjectiveSpace.instUniqueZero._proof_3.some

instance TauCeti.RealProjectiveSpace.instPathConnectedSpace (n : ℕ) : PathConnectedSpace (RealProjectiveSpace n)

Real projective space is path-connected for every n, as a nonempty subsingleton for n = 0 and as the continuous image of the path-connected unit sphere Sⁿ for 1 ≤ n.

theorem TauCeti.RealProjectiveSpace.isCoveringMap_mk (n : ℕ) : IsCoveringMap (mk n)

The unit-sphere projection onto real projective space is a covering map.

theorem TauCeti.RealProjectiveSpace.isOpenMap_mk (n : ℕ) : IsOpenMap (mk n)

The projection from the unit sphere onto real projective space is open.