The antipodal quotient is a covering map

This file establishes that the projection proj n : S^n → RP n is a covering map: the canonical double cover of real projective space by the sphere.

The argument uses the fact that the cyclic group DeckGroup = Multiplicative (ZMod 2) acts freely and (because it is finite acting on a Hausdorff space) properly discontinuously on the sphere by the antipodal involution, whose orbit relation is exactly the relation defining RP n. Mathlib's MulAction.isQuotientCoveringMap_of_properlyDiscontinuousSMul then yields that the quotient projection is a covering map.

Main results

• proj_isCoveringMap — proj n is a covering map;
• proj_isLocalHomeomorph — hence a local homeomorphism;
• proj_isCoveringMap_two_sheeted — proj n is a covering map and every fiber has exactly two elements (the "canonical double cover" packaged).

These covering-theoretic statements are the only public declarations of this file.

The purely quotient-relation facts about the fibers of proj n (the membership criterion proj_eq_iff, the fiber proj_fiber x = {x, -x}, and its two-element cardinality proj_fiber_ncard/proj_fiber_encard/proj_two_sheeted) live in RealProjectiveSpace.lean, since they need no covering-space machinery.

Implementation notes

DeckGroup is the order-two deck-transformation group of the cover. We model it as Multiplicative (ZMod 2) so that it is a genuine (multiplicative) group and MulAction/IsCancelSMul apply directly.

The antipodal deck action of DeckGroup on Sphere n is pure scaffolding: it exists only to discharge, by typeclass search, the hypotheses of the Mathlib quotient-covering lemma at the one call site below. Nothing outside this file consumes it, so the action (DeckGroup, the SMul/MulAction/ ContinuousConstSMul/IsCancelSMul instances, their defining equations, and the orbit criterion proj_eq_iff_mem_orbit) is kept out of the public surface: the four typeclass facts are local instances (so they never pollute global typeclass resolution downstream), and the supporting abbrev/lemmas are private. The genuinely covering-theoretic public API is exactly proj_isCoveringMap and proj_isLocalHomeomorph.

The antipodal deck-transformation action

The order-two group DeckGroup acts on Sphere n by the antipodal involution. These local instances supply exactly the hypotheses (MulAction, ContinuousConstSMul, IsCancelSMul) that the Mathlib quotient-covering lemma discharges by typeclass search. They are local to this file: the action is only needed to invoke that lemma, and is not part of the covering API.

The covering map

theorem SphereOddDegree.proj_isCoveringMap (n : ℕ) : IsCoveringMap ⇑(proj n)

The projection proj n : S^n → RP n is a covering map: the canonical double cover of real projective space by the sphere.

theorem SphereOddDegree.proj_isLocalHomeomorph (n : ℕ) : IsLocalHomeomorph ⇑(proj n)

The projection proj n is a local homeomorphism.

Local-homeomorphism consequences

The following are the standard consequences of proj n being a covering map / local homeomorphism, specialised to the canonical double cover.

theorem SphereOddDegree.proj_map_nhds_eq {n : ℕ} (x : Sphere n) : Filter.map (⇑(proj n)) (nhds x) = nhds ((proj n) x)

proj n maps the neighborhood filter of x isomorphically onto the neighborhood filter of proj n x: (𝓝 x).map (proj n) = 𝓝 (proj n x). A direct consequence of proj n being a local homeomorphism.

theorem SphereOddDegree.proj_isLocallyInjective (n : ℕ) : IsLocallyInjective ⇑(proj n)

proj n is locally injective: every point has a neighborhood on which the projection is injective. A consequence of proj n being a local homeomorphism.

theorem SphereOddDegree.proj_fiber_discreteTopology {n : ℕ} (q : RP n) : DiscreteTopology ↑(⇑(proj n) ⁻¹' {q})

The fibers of the covering map proj n are discrete: each (two-element) fiber proj n ⁻¹' {q} carries the discrete subspace topology. This is the characteristic discreteness of fibers of a covering map; here it follows from finiteness of the fiber in the Hausdorff sphere.

theorem SphereOddDegree.proj_isCoveringMap_two_sheeted (n : ℕ) : IsCoveringMap ⇑(proj n) ∧ ∀ (q : RP n), (⇑(proj n) ⁻¹' {q}).encard = 2

The projection proj n : S^n → RP n is a two-sheeted covering map: it is a covering map and every fiber has exactly two elements. This packages the covering-map property with the fiber-cardinality fact (proj_fiber_encard_eq_two) into the single statement "canonical double cover".