Real projective space as an antipodal quotient

This file defines the first genuinely topological object in the library:

RP n = S^n / (x ~ -x).

Implemented here:

• the antipodal equivalence relation on Sphere n;
• RP n as the quotient by that relation;
• the quotient projection proj : Sphere n -> RP n as a bundled continuous map;
• the quotient-map theorem for proj;
• descent of an odd map f : Sphere n -> Sphere n to RP n -> RP n;
• the basic commutative-square theorem, both pointwise and as a bundled continuous-map equality;
• a uniqueness theorem for the descended map;
• the fiber/relation API of proj: the membership criterion proj_eq_iff, the fiber proj_fiber x = {x, -x}, and the two-element cardinality of each fiber (proj_fiber_ncard, proj_fiber_encard, proj_two_sheeted). These depend only on the quotient relation, not on any covering-space machinery, so they live here next to the quotient rather than in Covering.lean.

def SphereOddDegree.AntipodalRel {n : ℕ} (x y : Sphere n) : Prop

The antipodal relation on the sphere: x ~ y iff x = y or x = -y.

Equations

• SphereOddDegree.AntipodalRel x y = (x = y ∨ x = -y)

@[instance_reducible]

instance SphereOddDegree.AntipodalSetoid (n : ℕ) : Setoid (Sphere n)

The antipodal relation is an equivalence relation.

Equations

• SphereOddDegree.AntipodalSetoid n = { r := SphereOddDegree.AntipodalRel, iseqv := ⋯ }

@[reducible, inline]

abbrev SphereOddDegree.RP (n : ℕ) : Type

Real projective n-space, modeled as S^n/(x ~ -x).

Equations

• SphereOddDegree.RP n = Quotient (SphereOddDegree.AntipodalSetoid n)

def SphereOddDegree.proj (n : ℕ) : C(Sphere n, RP n)

The quotient projection S^n -> RP n.

Equations

• SphereOddDegree.proj n = { toFun := Quotient.mk', continuous_toFun := ⋯ }

@[simp]

theorem SphereOddDegree.proj_apply {n : ℕ} (x : Sphere n) : (proj n) x = Quotient.mk' x

theorem SphereOddDegree.proj_isQuotientMap (n : ℕ) : Topology.IsQuotientMap ⇑(proj n)

The projection is a quotient map.

theorem SphereOddDegree.proj_neg {n : ℕ} (x : Sphere n) : (proj n) (-x) = (proj n) x

The projection identifies antipodal points.

theorem SphereOddDegree.proj_eq_proj_neg {n : ℕ} (x : Sphere n) : (proj n) x = (proj n) (-x)

A symmetric version of proj_neg.

Deck transformations (informal sense)

A deck transformation of the double cover proj n : S^n → RP n is a self-homeomorphism φ of S^n with proj n ∘ φ = proj n. Mathlib has no standalone deck-transformation abstraction (no DeckTransformation/deck declaration; only IsCoveringMap and the quotient-covering API built on MulAction/ProperlyDiscontinuousSMul), so we record here only the two elementary facts that the identity and the antipodal map are deck transformations of proj n, in the bare proj n ∘ φ = proj n sense. No abstract deck-transformation group is introduced.

theorem SphereOddDegree.proj_antipodal {n : ℕ} (x : Sphere n) : (proj n) ((antipodal n) x) = (proj n) x

The antipodal map commutes with the projection: proj n (antipodal n x) = proj n x. This is proj_neg phrased through the bundled antipodal map, and is the pointwise statement that the antipodal map is a deck transformation of the double cover proj n.

theorem SphereOddDegree.proj_comp_antipodal (n : ℕ) : (proj n).comp (antipodal n) = proj n

Bundled form of proj_antipodal: precomposing proj n with the antipodal map recovers proj n. This is the deck-transformation identity proj n ∘ antipodal n = proj n for the nontrivial deck transformation.

theorem SphereOddDegree.proj_comp_id (n : ℕ) : (proj n).comp (ContinuousMap.id (Sphere n)) = proj n

The identity map is (trivially) a deck transformation of proj n: proj n ∘ id = proj n.

Induction, recursion, and extensionality

Every point of RP n is proj n x for some sphere point x. The following lemmas package the standard Quotient boilerplate (Quotient.inductionOn, Quotient.inductionOn₂, funext/ContinuousMap.ext) specialized to proj n, so that downstream proofs can reason directly in terms of the projection rather than the underlying Quotient.mk'.

theorem SphereOddDegree.RP.ind {n : ℕ} {motive : RP n → Prop} (h : ∀ (x : Sphere n), motive ((proj n) x)) (q : RP n) : motive q

Induction principle for RP n: to prove a property of every point of RP n, it suffices to prove it for every proj n x.

theorem SphereOddDegree.RP.ind₂ {n : ℕ} {motive : RP n → RP n → Prop} (h : ∀ (x y : Sphere n), motive ((proj n) x) ((proj n) y)) (p q : RP n) : motive p q

Binary induction principle for RP n: to prove a property of every pair of points of RP n, it suffices to prove it for pairs proj n x, proj n y.

theorem SphereOddDegree.RP.exists_rep {n : ℕ} (q : RP n) : ∃ (x : Sphere n), (proj n) x = q

Every point of RP n is the image under proj n of some sphere point.

theorem SphereOddDegree.RP.funext {n : ℕ} {β : Sort u_1} {f g : RP n → β} (h : ∀ (x : Sphere n), f ((proj n) x) = g ((proj n) x)) : f = g

Extensionality for functions out of RP n: two functions agree if they agree after precomposition with proj n (i.e. on all representatives).

theorem SphereOddDegree.RP.hom_ext {n : ℕ} {β : Type u_1} [TopologicalSpace β] {f g : C(RP n, β)} (h : ∀ (x : Sphere n), f ((proj n) x) = g ((proj n) x)) : f = g

Extensionality for continuous maps out of RP n: two continuous maps are equal if they agree on all representatives proj n x. Tagged @[ext], so the ext tactic reduces a goal f = g between maps C(RP n, β) directly to the goal f (proj n x) = g (proj n x) on a representative x : Sphere n.

theorem SphereOddDegree.RP.hom_ext_iff {n : ℕ} {β : Type u_1} [TopologicalSpace β] {f g : C(RP n, β)} : f = g ↔ ∀ (x : Sphere n), f ((proj n) x) = g ((proj n) x)

theorem SphereOddDegree.proj_surjective (n : ℕ) : Function.Surjective ⇑(proj n)

The quotient projection is surjective.

theorem SphereOddDegree.proj_eq_of_antipodalRel {n : ℕ} {x y : Sphere n} (hxy : AntipodalRel x y) : (proj n) x = (proj n) y

Equality in RP n follows from the antipodal relation upstairs.

theorem SphereOddDegree.antipodalRel_map_of_isOdd {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) {x y : Sphere n} (hxy : AntipodalRel x y) : AntipodalRel (f x) (f y)

If two sphere points are related by the antipodal relation, then their images under an odd map are again related.

def SphereOddDegree.inducedOnRP {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : C(RP n, RP n)

Map on projective space induced by an odd sphere self-map.

This is the formal version of the descent f to bar f along the quotient S^n -> RP n.

Equations

• SphereOddDegree.inducedOnRP f hf = { toFun := Quotient.lift (fun (x : SphereOddDegree.Sphere n) => (SphereOddDegree.proj n) (f x)) ⋯, continuous_toFun := ⋯ }

theorem SphereOddDegree.inducedOnRP_comm {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (x : Sphere n) : (inducedOnRP f hf) ((proj n) x) = (proj n) (f x)

Commutativity of the square defining the descended map, pointwise.

theorem SphereOddDegree.inducedOnRP_proj {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (x : Sphere n) : (inducedOnRP f hf) ((proj n) x) = (proj n) (f x)

The defining computation rule of the descended map, as a simp lemma: inducedOnRP f hf (proj n x) = proj n (f x). This is the single-point form of inducedOnRP_comm, tagged @[simp] so that simp automatically pushes the descended map through proj n to the odd map f upstairs.

theorem SphereOddDegree.inducedOnRP_comp_proj {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : (inducedOnRP f hf).comp (proj n) = (proj n).comp f

Commutativity of the square defining the descended map, as continuous maps.

theorem SphereOddDegree.inducedOnRP_unique {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) {g : C(RP n, RP n)} (hg : ∀ (x : Sphere n), g ((proj n) x) = (proj n) (f x)) : g = inducedOnRP f hf

The descended map is uniquely determined by the pointwise commutative square.

theorem SphereOddDegree.inducedOnRP_unique_comp {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) {g : C(RP n, RP n)} (hg : g.comp (proj n) = (proj n).comp f) : g = inducedOnRP f hf

The descended map is uniquely determined by the bundled commutative square.

theorem SphereOddDegree.inducedOnRP_id (n : ℕ) : inducedOnRP (ContinuousMap.id (Sphere n)) ⋯ = ContinuousMap.id (RP n)

The descent of the identity odd map is the identity on RP n.

theorem SphereOddDegree.inducedOnRP_comp {n : ℕ} {f g : C(Sphere n, Sphere n)} (hf : IsOddMap f) (hg : IsOddMap g) : (inducedOnRP g hg).comp (inducedOnRP f hf) = inducedOnRP (g.comp f) ⋯

Descent is functorial: it sends a composite of odd maps to the composite of the descended maps.

theorem SphereOddDegree.inducedOnRP_congr {n : ℕ} {f g : C(Sphere n, Sphere n)} (hf : IsOddMap f) (hg : IsOddMap g) (h : f = g) : inducedOnRP f hf = inducedOnRP g hg

The descended map depends only on the underlying odd map, not on the chosen oddness proof: equal odd maps descend to equal maps on RP n. (Proof irrelevance handles the oddness hypotheses, so only the equality f = g of the maps matters.)

theorem SphereOddDegree.inducedOnRP_antipodal (n : ℕ) : inducedOnRP (antipodal n) ⋯ = ContinuousMap.id (RP n)

The descent of the antipodal map is the identity on RP n: the nontrivial deck transformation antipodal n becomes trivial after passing to the quotient, since proj n (-x) = proj n x. This is the descent counterpart of proj_comp_antipodal.

theorem SphereOddDegree.inducedOnRP_surjective {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) (hsurj : Function.Surjective ⇑f) : Function.Surjective ⇑(inducedOnRP f hf)

The descended map is surjective whenever the odd map it descends from is surjective. (Surjectivity of proj n lets us lift any target point, and the commuting square inducedOnRP_comm transports a preimage upstairs to a preimage downstairs.)

Fibers of the projection

The fiber of proj n over proj n x is the antipodal pair {x, -x}, which consists of two distinct points. These facts use only the quotient relation (Quotient.exact/Quotient.sound, proj_neg) together with the sphere-level fixed-point-free fact ne_neg_self; they require no covering-space machinery, so they belong with the quotient definition rather than in Covering.lean.

theorem SphereOddDegree.proj_eq_iff {n : ℕ} {x y : Sphere n} : (proj n) y = (proj n) x ↔ y = x ∨ y = -x

Two sphere points have the same image under proj n iff they are equal or antipodal. This is the membership criterion for the fibers of the quotient projection.

theorem SphereOddDegree.proj_eq_iff_antipodalRel {n : ℕ} {x y : Sphere n} : (proj n) x = (proj n) y ↔ AntipodalRel x y

Two sphere points have the same image under proj n iff they are related by the antipodal relation. This is proj_eq_iff phrased through AntipodalRel, the form that matches the Setoid underlying RP n (and the converse to proj_eq_of_antipodalRel).

theorem SphereOddDegree.eq_or_eq_neg_of_proj_eq {n : ℕ} {x y : Sphere n} (h : (proj n) y = (proj n) x) : y = x ∨ y = -x

If two sphere points have the same image under proj n, then they are equal or antipodal.

theorem SphereOddDegree.mem_proj_fiber {n : ℕ} {x y : Sphere n} : y ∈ ⇑(proj n) ⁻¹' {(proj n) x} ↔ y = x ∨ y = -x

Membership criterion for the fiber of proj n over proj n x: a point y lies in the fiber iff it equals x or its antipode -x. This is the simp-form of proj_eq_iff phrased as fiber membership.

theorem SphereOddDegree.proj_fiber {n : ℕ} (x : Sphere n) : ⇑(proj n) ⁻¹' {(proj n) x} = {x, -x}

The fiber of proj n over proj n x is exactly the antipodal pair {x, -x}.

theorem SphereOddDegree.proj_fiber_ncard {n : ℕ} (x : Sphere n) : (⇑(proj n) ⁻¹' {(proj n) x}).ncard = 2

The fiber of proj n over proj n x has exactly two elements (Set.ncard version): the antipodal pair {x, -x} of two distinct points.

theorem SphereOddDegree.proj_fiber_encard {n : ℕ} (x : Sphere n) : (⇑(proj n) ⁻¹' {(proj n) x}).encard = 2

The fiber of proj n over proj n x has exactly two elements (Set.encard version).

theorem SphereOddDegree.proj_two_sheeted {n : ℕ} (x : Sphere n) : x ≠ -x ∧ ⇑(proj n) ⁻¹' {(proj n) x} = {x, -x}

Two-sheetedness of proj n, packaged: the fiber over proj n x is the unordered pair {x, -x} of two distinct points.

theorem SphereOddDegree.proj_fiber_eq_deck_orbit {n : ℕ} (x : Sphere n) : ⇑(proj n) ⁻¹' {(proj n) x} = {(ContinuousMap.id (Sphere n)) x, (antipodal n) x}

The fiber of proj n over proj n x is exactly the orbit of x under the two deck transformations (the identity and the antipodal map): the pair {id x, antipodal n x} = {x, -x}. This is proj_fiber phrased through the deck transformations, making explicit that each fiber is a single deck-group orbit.

Fibers over arbitrary points

The fiber lemmas above are phrased over proj n x, i.e. over a chosen representative. Since proj n is surjective, the same facts hold over an arbitrary point q : RP n: every fiber is the antipodal pair of some representative and therefore has exactly two elements. These generalizations still use only the quotient relation.

theorem SphereOddDegree.proj_fiber_eq {n : ℕ} {q : RP n} {x : Sphere n} (hx : (proj n) x = q) : ⇑(proj n) ⁻¹' {q} = {x, -x}

The fiber of proj n over an arbitrary point q : RP n is the antipodal pair {x, -x} of any representative x of q.

theorem SphereOddDegree.proj_fiber_ncard_eq_two {n : ℕ} (q : RP n) : (⇑(proj n) ⁻¹' {q}).ncard = 2

Every fiber of proj n has exactly two elements (Set.ncard version).

theorem SphereOddDegree.proj_fiber_encard_eq_two {n : ℕ} (q : RP n) : (⇑(proj n) ⁻¹' {q}).encard = 2

Every fiber of proj n has exactly two elements (Set.encard version).

theorem SphereOddDegree.proj_fiber_nat_card_eq_two {n : ℕ} (q : RP n) : Nat.card ↑(⇑(proj n) ⁻¹' {q}) = 2

Every fiber of proj n has exactly two elements (Nat.card version).

theorem SphereOddDegree.proj_fiber_finite {n : ℕ} (q : RP n) : (⇑(proj n) ⁻¹' {q}).Finite

Every fiber of proj n is finite (it has exactly two elements).

theorem SphereOddDegree.proj_preimage_singleton_eq_iff {n : ℕ} {q₁ q₂ : RP n} : ⇑(proj n) ⁻¹' {q₁} = ⇑(proj n) ⁻¹' {q₂} ↔ q₁ = q₂

Fiber extensionality for proj n: two fibers coincide iff their base points in RP n are equal. (One direction is congrArg; the other uses surjectivity of proj n.)

Action of the descended map on the fibers of the cover

The descended map inducedOnRP f hf is, by inducedOnRP_comp_proj, the unique map making the square

S^n --f--> S^n
 | |
proj proj
 ▼ ▼
RP^n -fbar-> RP^n

commute. The lemmas below extract from that square the fiberwise data that a pullback-of-covers / monodromy-naturality argument consumes: the odd map f carries the fiber over q into the fiber over fbar q (inducedOnRP_mapsTo_fiber), the image of a whole fiber is exactly the target fiber (inducedOnRP_image_fiber), and f is injective on each (two-element) fiber (inducedOnRP_injOn_fiber). Together these say f restricts to a bijection between the two-element fibers, which is precisely the base-point-to-base-point compatibility the descended map needs to act on the canonical double cover. These are pure quotient/point-set facts (they use only inducedOnRP_comm, proj_fiber, and the oddness of f), so they live here rather than in Covering.lean; no covering-space, classifying-map, or cohomology machinery is involved.

theorem SphereOddDegree.inducedOnRP_mapsTo_fiber {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (q : RP n) : Set.MapsTo (⇑f) (⇑(proj n) ⁻¹' {q}) (⇑(proj n) ⁻¹' {(inducedOnRP f hf) q})

The descended map respects fibers: the odd map f carries the fiber over q into the fiber over the descended image inducedOnRP f hf q. This is the fiberwise form of the commuting square inducedOnRP_comp_proj, and the basic input for treating inducedOnRP f hf as a map of the double cover by pullback.

theorem SphereOddDegree.inducedOnRP_image_fiber {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (x : Sphere n) : ⇑f '' ⇑(proj n) ⁻¹' {(proj n) x} = ⇑(proj n) ⁻¹' {(inducedOnRP f hf) ((proj n) x)}

The image under the odd map f of the fiber over proj n x is exactly the fiber over the descended image inducedOnRP f hf (proj n x). Equivalently, f {x, -x} = {f x, -f x}. This is the surjective-on-fibers half of the statement that f restricts to a bijection between the two-element fibers.

theorem SphereOddDegree.inducedOnRP_injOn_fiber {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (x : Sphere n) : Set.InjOn (⇑f) (⇑(proj n) ⁻¹' {(proj n) x})

The odd map f is injective on each (two-element) fiber of proj n: it cannot identify the two antipodal points x and -x, since f (-x) = -f x ≠ f x. This is the injective-on-fibers half of the statement that f restricts to a bijection between the two-element fibers.

theorem SphereOddDegree.inducedOnRP_bijOn_fiber {n : ℕ} (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (q : RP n) : Set.BijOn (⇑f) (⇑(proj n) ⁻¹' {q}) (⇑(proj n) ⁻¹' {(inducedOnRP f hf) q})

The odd map f restricts to a bijection between the two-element fibers of the double cover: it maps the fiber over q bijectively onto the fiber over the descended image inducedOnRP f hf q. This packages inducedOnRP_mapsTo_fiber, inducedOnRP_injOn_fiber, and inducedOnRP_image_fiber into a single Set.BijOn, the fiberwise statement that inducedOnRP f hf is a map of the canonical double cover.