Nontriviality of the monodromy classifying character of the double cover

This file proves that, for n ≥ 1, the monodromy classifying homomorphism

classifyingHom n x : FundamentalGroup (RP n) x →* Multiplicative (ZMod 2)

of the double cover proj n : S^n → RP n (constructed in DoubleCoverClass.lean) is surjective — equivalently, nontrivial: some loop of RP n has monodromy that swaps the two sheets of the cover.

This is the honest nontriviality statement of Route A toward α ∈ H¹(RPⁿ; F₂). It does not require the (absent) computation π₁(Sⁿ) = 0 nor SimplyConnectedSpace (Sphere n); it needs only that the sphere S^n is path-connected for n ≥ 1 (isPathConnected_sphere). The geometric content is exactly: a point e ∈ S^n and its antipode -e lie in the same path component, so the projection of any path e ⤳ -e is a loop of RP n whose monodromy sends the sheet e to the other sheet -e.

Main declarations

• joined_antipode — for n ≥ 1, every e : S^n is Joined to its antipode -e.
• projMonodromy_mk_of_lift — the monodromy of the class of a path γ sends a fibre point e to the endpoint of any continuous lift of γ starting at e.
• exists_loop_projMonodromyPerm_ne_one — for n ≥ 1, some loop class at x has a nontrivial (sheet-swapping) monodromy permutation.
• exists_classifyingHom_ne_one — for n ≥ 1, some class of π₁(RP n, x) has classifying value ≠ 1.
• classifyingHom_surjective — for n ≥ 1, classifyingHom n x is surjective.

theorem SphereOddDegree.one_lt_rank_euclidean (n : ℕ) (hn : 1 ≤ n) : 1 < Module.rank ℝ (EuclideanSpace ℝ (Fin (n + 1)))

For n ≥ 1, the ambient Euclidean space ℝ^{n+1} of S^n has rank > 1, the hypothesis of isPathConnected_sphere.

theorem SphereOddDegree.joined_antipode (n : ℕ) (hn : 1 ≤ n) (e : Sphere n) : Joined e (-e)

For n ≥ 1, every point e : S^n is joined by a path to its antipode -e (the unit sphere of ℝ^{n+1} is path-connected when n ≥ 1).

theorem SphereOddDegree.projMonodromy_mk_of_lift (n : ℕ) {x y : RP n} (γ : Path x y) (e : ↑(⇑(proj n) ⁻¹' {x})) (Γ : C(↑unitInterval, Sphere n)) (hΓ : ⇑(proj n) ∘ ⇑Γ = ⇑γ) (hΓ0 : Γ 0 = ↑e) : ↑(projMonodromy n ⟦γ⟧ e) = Γ 1

Monodromy via an explicit lift. If Γ is a continuous lift of the path γ (i.e. proj n ∘ Γ = γ pointwise) starting at the fibre point e, then the monodromy of the homotopy class ⟦γ⟧ sends e to the endpoint Γ 1.

theorem SphereOddDegree.exists_loop_projMonodromyPerm_ne_one (n : ℕ) (hn : 1 ≤ n) (x : RP n) : ∃ (γ : Path.Homotopic.Quotient x x), projMonodromyPerm n γ ≠ 1

A sheet-swapping loop. For n ≥ 1 and any base point x : RP n, there is a loop class at x whose monodromy permutation of the two-element fibre is nontrivial (it swaps the two sheets of the double cover).

theorem SphereOddDegree.exists_classifyingHom_ne_one (n : ℕ) (hn : 1 ≤ n) (x : RP n) : ∃ (a : FundamentalGroup (RP n) x), (classifyingHom n x) a ≠ 1

Nontriviality of the classifying character. For n ≥ 1 and any base point x : RP n, some class of π₁(RP n, x) has classifying value ≠ 1.

theorem SphereOddDegree.classifyingHom_surjective (n : ℕ) (hn : 1 ≤ n) (x : RP n) : Function.Surjective ⇑(classifyingHom n x)

Surjectivity of the monodromy classifying character. For n ≥ 1, the classifying homomorphism classifyingHom n x : π₁(RP n, x) → Multiplicative (ZMod 2) of the double cover proj n : S^n → RP n is surjective. This is the honest nontriviality statement of Route A toward α ∈ H¹(RPⁿ; F₂).