The canonical ZMod 2 monodromy class of the double cover S^n → RP n

toward the canonical degree-one class

α ∈ H¹(RPⁿ; F₂)

associated with the double cover proj n : S^n → RP n.

What is honestly constructed here

The covering / monodromy side of Route A is realised as a genuine, fully-proved group homomorphism

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

— the monodromy classifying homomorphism of the double cover. It is the composite

π₁(RP n, x) --projMonodromyHom--> Equiv.Perm (proj n ⁻¹' {x})
 --permToZMod2--> Multiplicative (ZMod 2)

where projMonodromyHom (from Monodromy.lean) is the genuine action of the fundamental group on the two-element fibre, and permToZMod2 is the parity (Equiv.Perm.sign composed with ℤˣ ≅ ZMod 2) of a permutation of a finite set. On the two-element fibre this parity records exactly whether a loop swaps the two sheets of the cover, i.e. it is the classifying datum of the regular ZMod 2-cover.

This homomorphism is the source datum from which α is obtained, in Route A, by the degree-one universal coefficient theorem H¹(X; F₂) ≅ Hom(π₁(X)ᵃᵇ, F₂). That theorem is absent from the pinned Mathlib, so an honest α ∈ H¹(RPⁿ; F₂) cannot yet be produced; this file therefore stops exactly at the last formalized object before α, plus the H¹ target abbreviations, with **

Monodromy → ZMod 2

• intUnitsToZMod2 — the canonical isomorphism ℤˣ →* Multiplicative (ZMod 2).
• permToZMod2 — the parity homomorphism Equiv.Perm α →* Multiplicative (ZMod 2) for a finite α.
• classifyingHom n x — the monodromy classifying homomorphism π₁(RP n, x) →* Multiplicative (ZMod 2) of the double cover.

Naturality under descended odd maps

• classifyingHom_inducedOnRP_naturality — the descended odd map fbar acts trivially on the classifying homomorphism: classifyingHom n (fbar x) ∘ (π₁ map fbar) = classifyingHom n x. This is the fundamental-group form of the eventual fbar^*(α) = α.

Target abbreviations: H¹(RP n; F₂)

@[reducible, inline]

noncomputable abbrev SphereOddDegree.rpH1ZMod2 (n : ℕ) : ModuleCat (ZMod 2)

The genuine degree-one mod-2 singular cohomology object H¹(RP n; F₂) of real projective space, which contains the canonical class α.

Equations

• SphereOddDegree.rpH1ZMod2 n = SphereOddDegree.rpCohomology n 1

@[reducible, inline]

noncomputable abbrev SphereOddDegree.rpDegreeOneCohomology (n : ℕ) : ModuleCat (ZMod 2)

Verbose alias for rpH1ZMod2: the degree-one mod-2 cohomology of RP n.

Equations

• SphereOddDegree.rpDegreeOneCohomology n = SphereOddDegree.rpCohomology n 1

The parity homomorphism Equiv.Perm α →* Multiplicative (ZMod 2)

def SphereOddDegree.intUnitsToZMod2 : ℤˣ →* Multiplicative (ZMod 2)

The canonical group isomorphism ℤˣ →* Multiplicative (ZMod 2) sending the trivial unit 1 to 0 and -1 to 1. Both groups are cyclic of order two; this is the homomorphism underlying the sign-parity of a permutation.

Equations

• SphereOddDegree.intUnitsToZMod2 = { toFun := fun (u : ℤˣ) => Multiplicative.ofAdd (if u = 1 then 0 else 1), map_one' := SphereOddDegree.intUnitsToZMod2._proof_1, map_mul' := ⋯ }

@[simp]

theorem SphereOddDegree.intUnitsToZMod2_one : intUnitsToZMod2 1 = 1

@[simp]

theorem SphereOddDegree.intUnitsToZMod2_neg_one : intUnitsToZMod2 (-1) = Multiplicative.ofAdd 1

noncomputable def SphereOddDegree.permToZMod2 {α : Type u_1} [Finite α] : Equiv.Perm α →* Multiplicative (ZMod 2)

The parity homomorphism of a permutation of a finite type, valued in Multiplicative (ZMod 2): it is Equiv.Perm.sign followed by the isomorphism ℤˣ ≅ Multiplicative (ZMod 2). For a two-element type this is an isomorphism recording whether the permutation is the identity or the transposition.

Equations

• SphereOddDegree.permToZMod2 = SphereOddDegree.intUnitsToZMod2.comp Equiv.Perm.sign

theorem SphereOddDegree.permToZMod2_permCongr {α : Type u_1} {β : Type u_2} [Finite α] [Finite β] (e : α ≃ β) (p : Equiv.Perm α) : permToZMod2 (e.permCongr p) = permToZMod2 p

permToZMod2 is invariant under transporting a permutation along an equivalence of finite types (parity is a conjugation invariant). This is the algebraic engine of the descended-map naturality of classifyingHom.

Faithfulness of the parity character on a two-point fibre

On a two-element type the parity homomorphism permToZMod2 is not merely a homomorphism but a bijection: there are exactly two permutations of a two-element set (the identity and the swap) and exactly two values in ZMod 2, and parity distinguishes them. This is the canonical, choice-free identification Equiv.Perm α ≃* Multiplicative (ZMod 2) for Nat.card α = 2 underlying the ZMod 2-valued monodromy character: it shows the character loses no information about the two-sheet monodromy.

theorem SphereOddDegree.intUnitsToZMod2_injective : Function.Injective ⇑intUnitsToZMod2

The unit isomorphism ℤˣ →* Multiplicative (ZMod 2) is injective (indeed it is an isomorphism of the two cyclic groups of order two).

theorem SphereOddDegree.card_two_elim {α : Type u_1} [Finite α] (h : Nat.card α = 2) : ∃ (a : α) (b : α), a ≠ b ∧ ∀ (x : α), x = a ∨ x = b

A two-element type is exhausted by two distinct elements: there exist a ≠ b such that every element equals a or b.

theorem SphereOddDegree.perm_two_eq_one_or_fixedpointfree {α : Type u_1} [Finite α] (h : Nat.card α = 2) (p : Equiv.Perm α) : p = 1 ∨ ∀ (x : α), p x ≠ x

Every permutation of a two-point set is either the identity or the swap. Phrased without DecidableEq: a permutation of a type with exactly two elements is either the identity or fixed-point-free (and a fixed-point-free permutation of a two-element set is exactly the transposition of its two elements).

theorem SphereOddDegree.permToZMod2_injective {α : Type u_1} [Finite α] (h : Nat.card α = 2) : Function.Injective ⇑permToZMod2

On a two-element type the parity homomorphism permToZMod2 is injective.

theorem SphereOddDegree.permToZMod2_eq_one_iff {α : Type u_1} [Finite α] (h : Nat.card α = 2) (p : Equiv.Perm α) : permToZMod2 p = 1 ↔ p = 1

On a two-element type the parity character is trivial exactly on the identity permutation: permToZMod2 p = 1 ↔ p = 1.

noncomputable def SphereOddDegree.permTwoMulEquivZMod2 {α : Type u_1} [Finite α] (h : Nat.card α = 2) : Equiv.Perm α ≃* Multiplicative (ZMod 2)

The canonical identification of the two-point permutation group with ZMod 2. For a type α with exactly two elements, the parity homomorphism permToZMod2 is a group isomorphism Equiv.Perm α ≃* Multiplicative (ZMod 2). This is choice-free (no labelling of the two points is needed): it is the canonical reason a ZMod 2-valued monodromy character exists for the double cover, since each fibre of proj n is a two-element set.

Equations

• SphereOddDegree.permTwoMulEquivZMod2 h = MulEquiv.ofBijective SphereOddDegree.permToZMod2 ⋯

@[simp]

theorem SphereOddDegree.permTwoMulEquivZMod2_apply {α : Type u_1} [Finite α] (h : Nat.card α = 2) (p : Equiv.Perm α) : (permTwoMulEquivZMod2 h) p = permToZMod2 p

The monodromy classifying homomorphism π₁(RP n) →* ZMod 2

instance SphereOddDegree.projFiberFinite (n : ℕ) (x : RP n) : Finite ↑(⇑(proj n) ⁻¹' {x})

Every fibre of proj n is a finite type (it has two elements).

noncomputable def SphereOddDegree.classifyingHom (n : ℕ) (x : RP n) : FundamentalGroup (RP n) x →* Multiplicative (ZMod 2)

The monodromy classifying homomorphism of the double cover proj n : S^n → RP n: the action of the fundamental group π₁(RP n, x) on the two-element fibre over x, composed with the permutation parity into Multiplicative (ZMod 2). A loop maps to 1 iff its monodromy swaps the two sheets of the cover.

This is the genuine covering-theoretic datum from which the canonical class α ∈ H¹(RP n; F₂) is obtained, via a degree-one cohomological classifier H¹(X; F₂) ≅ Hom(π₁(X)ᵃᵇ, F₂). It is a proved homomorphism out of π₁(RP n, x).

Equations

• SphereOddDegree.classifyingHom n x = SphereOddDegree.permToZMod2.comp (SphereOddDegree.projMonodromyHom n x)

theorem SphereOddDegree.classifyingHom_apply (n : ℕ) (x : RP n) (a : FundamentalGroup (RP n) x) : (classifyingHom n x) a = permToZMod2 (projMonodromyPerm n a.toPath)

The classifying homomorphism applied to a class is the parity of its monodromy permutation on the fibre.

The two-sheet dichotomy and faithfulness of the classifying character

Because every fibre of proj n has exactly two elements (proj_fiber_nat_card_eq_two), the abstract two-point facts above apply to the monodromy permutation of a loop: it either fixes both sheets (trivial monodromy) or swaps them, and the ZMod 2-valued classifying character records exactly this dichotomy with no loss of information.

theorem SphereOddDegree.projMonodromyPerm_eq_one_or_swaps (n : ℕ) {x : RP n} (γ : Path.Homotopic.Quotient x x) : projMonodromyPerm n γ = 1 ∨ ∀ (e : ↑(⇑(proj n) ⁻¹' {x})), (projMonodromyPerm n γ) e ≠ e

Two-sheet dichotomy of the monodromy. For a loop γ at x, the monodromy permutation of the two-element fibre is either the identity (the loop preserves both sheets of the cover) or fixed-point-free (the loop swaps the two sheets). This is perm_two_eq_one_or_fixedpointfree applied to the fibre, whose cardinality is two.

theorem SphereOddDegree.classifyingHom_eq_one_iff (n : ℕ) (x : RP n) (a : FundamentalGroup (RP n) x) : (classifyingHom n x) a = 1 ↔ (projMonodromyHom n x) a = 1

Faithfulness of the classifying character. The classifying character is trivial on a class a iff the monodromy permutation of its underlying loop is the identity: the ZMod 2 value loses no information about the two-sheet monodromy. (This uses permToZMod2_eq_one_iff on the two-element fibre.)

theorem SphereOddDegree.classifyingHom_ne_one_iff (n : ℕ) (x : RP n) (a : FundamentalGroup (RP n) x) : (classifyingHom n x) a ≠ 1 ↔ ∀ (e : ↑(⇑(proj n) ⁻¹' {x})), (projMonodromyPerm n a.toPath) e ≠ e

The classifying character is nontrivial on a class a iff the monodromy of its underlying loop swaps the two sheets, i.e. it is fixed-point-free on the fibre. This is the loop-level meaning of classifyingHom n x a ≠ 1.

Naturality of the classifying homomorphism under descended odd maps

theorem SphereOddDegree.inducedOnRPFiberMap_bijective (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (q : RP n) : Function.Bijective (inducedOnRPFiberMap n f hf)

The fibrewise map inducedOnRPFiberMap of an odd map f is bijective: an odd map restricts to a bijection between the two-element fibres of the double cover.

noncomputable def SphereOddDegree.inducedOnRPFiberEquiv (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (q : RP n) : ↑(⇑(proj n) ⁻¹' {q}) ≃ ↑(⇑(proj n) ⁻¹' {(inducedOnRP f hf) q})

The fibrewise map of an odd map f, packaged as an equivalence between the two-element fibre over q and the fibre over the descended image inducedOnRP f hf q.

Equations

• SphereOddDegree.inducedOnRPFiberEquiv n f hf q = Equiv.ofBijective (SphereOddDegree.inducedOnRPFiberMap n f hf) ⋯

@[simp]

theorem SphereOddDegree.inducedOnRPFiberEquiv_apply (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) {q : RP n} (e : ↑(⇑(proj n) ⁻¹' {q})) : (inducedOnRPFiberEquiv n f hf q) e = inducedOnRPFiberMap n f hf e

theorem SphereOddDegree.projMonodromyPerm_map_eq_permCongr (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) {x : RP n} (γ : Path.Homotopic.Quotient x x) : projMonodromyPerm n (γ.map { toFun := ⇑(inducedOnRP f hf), continuous_toFun := ⋯ }) = (inducedOnRPFiberEquiv n f hf x).permCongr (projMonodromyPerm n γ)

The descended-loop monodromy permutation is the conjugate of the base-loop monodromy permutation by the fibre equivalence of the odd map: for a loop γ at x, projMonodromyPerm (γ.map fbar) = (fibreEquiv).permCongr (projMonodromyPerm γ).

theorem SphereOddDegree.classifyingHom_inducedOnRP_naturality (n : ℕ) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (x : RP n) : (classifyingHom n ((inducedOnRP f hf) x)).comp (FundamentalGroup.map { toFun := ⇑(inducedOnRP f hf), continuous_toFun := ⋯ } x) = classifyingHom n x

Naturality of the classifying homomorphism under a descended odd map. The descended odd map fbar = inducedOnRP f hf acts trivially on the monodromy classifying homomorphism: precomposing the classifying homomorphism at fbar x with the induced map on π₁ recovers the classifying homomorphism at x,

classifyingHom n (fbar x) ∘ (π₁ map fbar) = classifyingHom n x.

This is the fundamental-group form of the eventual cohomological identity fbar^*(α) = α: the parity of a loop's monodromy is preserved by the descended odd map, because f restricts to a bijection of fibres and parity is a conjugation invariant.