§8: central double covers, liftable counts, and the lift torsor

Central double covers and their pulled-back boundary-framed structure (Lemma 8.3 setup), corestriction of continuous homs, the totalized stratum count exactImageCountOn, the liftable count u^β_Γ(p, J) (liftableCount), and the scalar-twist torsor structure on cover lifts (Lemma 8.2's second clause).

Central double covers and the pulled-back boundary-framed structure (Lemma 8.3 setup)

A central double cover p : Ỹ ↠ Y carries its own group/topology data (all finite discrete). The pulled-back marked target (Ỹ, p⁻¹(L_Y), π_Y∘p, θ_Y∘p) of Lemma 8.3 is pullTarget; the paper's condition "the central kernel lies in ker(π̃, θ̃)" holds by construction.

noncomputable def GQ2.SectionEight.CentralCover.pullTarget {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (T : MarkedTarget H E Y) : MarkedTarget H E C.cover

The pulled-back boundary-framed structure (Lemma 8.3): give Ỹ the marked normal 2-subgroup p⁻¹(L_Y), head π_Y ∘ p, decoration θ_Y ∘ p.

Equations

• C.pullTarget T = { LY := Subgroup.comap C.p T.LY, normal := ⋯, isPGroup_two := ⋯, piY := T.piY.comp C.p, piY_surjective := ⋯, ker_piY := ⋯, thetaY := T.thetaY.comp C.p }

Corestriction of continuous homs to a subgroup

Mathlib has no ContinuousMonoidHom.codRestrict; we build the corestriction to a subgroup of the codomain containing the image, and the bijection between homs onto a subgroup and homs into the ambient group landing in it — the bookkeeping the Lemma 8.3 fibrations run on.

def GQ2.SectionEight.cmhCodRestrict {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [TopologicalSpace G₁] [Group G₂] [TopologicalSpace G₂] (f : G₁ →ₜ* G₂) (S : Subgroup G₂) (h : ∀ (x : G₁), f x ∈ S) : G₁ →ₜ* ↥S

Corestrict a continuous hom to a subgroup of its codomain containing its image.

Equations

• GQ2.SectionEight.cmhCodRestrict f S h = { toFun := fun (x : G₁) => ⟨f x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

def GQ2.SectionEight.cmhInclude {G₁ : Type u_1} {G₂ : Type u_2} [Group G₁] [TopologicalSpace G₁] [Group G₂] [TopologicalSpace G₂] (S : Subgroup G₂) (g : G₁ →ₜ* ↥S) : G₁ →ₜ* G₂

Include a continuous hom into a subgroup back into the ambient group.

Equations

• GQ2.SectionEight.cmhInclude S g = { toMonoidHom := S.subtype.comp g.toMonoidHom, continuous_toFun := ⋯ }

Liftable counts and the totalized stratum count

noncomputable def GQ2.SectionEight.CentralCover.pCont {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] (C : CentralCover Y) : C.cover →ₜ* Y

The covering map bundled as a continuous hom (continuous since the cover is discrete).

Equations

• C.pCont = { toMonoidHom := C.p, continuous_toFun := ⋯ }

noncomputable def GQ2.SectionEight.exactImageCountOn {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (J : Subgroup Y) : ℕ

The exact-image count of the J-stratum, totalized (0 when J does not project onto H) — the summand shape of the partitions (124)/(138)/(142).

Equations

• GQ2.SectionEight.exactImageCountOn b F T J = if h : Function.Surjective ⇑(T.piY.comp J.subtype) then GQ2.exactImageCount b F (T.stratum J h) else 0

noncomputable def GQ2.SectionEight.liftableCount {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (C : CentralCover Y) (J : Subgroup Y) (hJ : Function.Surjective ⇑(T.piY.comp J.subtype)) : ℕ

u^β_Γ(p, J) (Lemma 8.3): the number of boundary-framed exact-image maps onto the J-stratum whose pullback central cover is split — encoded as the existence of a continuous lift through p (an unobstructed map has a lift, and conversely).

Equations

• GQ2.SectionEight.liftableCount b F T C J hJ = Nat.card { f : GQ2.BoundaryLifts b F (T.stratum J hJ) // ∃ (g : Γ →ₜ* C.cover), ∀ (γ : Γ), C.p (g γ) = ↑(↑↑f γ) }

Scalar twisting (Lemma 8.2's second clause — proved)

theorem GQ2.SectionEight.z_pow_central {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (n : ℕ) (w : C.cover) : C.z ^ n * w = w * C.z ^ n

z-powers are central.

noncomputable def GQ2.SectionEight.scalarTwist {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (f : Γ →ₜ* C.cover) (c : Γ →ₜ* Multiplicative (ZMod 2)) : Γ →ₜ* C.cover

Scalar twist of a map into a central double cover by a 𝔽₂-character (Lemma 8.2/8.3: "multiplying a lift by a scalar character"). A homomorphism because z is central of square one.

Equations

• GQ2.SectionEight.scalarTwist C f c = { toFun := fun (γ : Γ) => f γ * C.z ^ (Multiplicative.toAdd (c γ)).val, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

The torsor structure on cover lifts

The continuous-hom lifts of a fixed f : Γ → Y through p form a torsor under Hom_cont(Γ, 𝔽₂), acting by scalarTwist. This is the combinatorial heart of Lemma 8.3 (and the half-torsor of 8.6): p_comp_scalarTwist (the action stays in the fibre), scalarTwist_left_injective (freeness), and liftDiff/scalarTwist_liftDiff (transitivity — every two lifts differ by a unique character).

theorem GQ2.SectionEight.orderOf_z {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) : orderOf C.z = 2

z has order exactly 2.

theorem GQ2.SectionEight.z_pow_eq_iff {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) {a b : ℕ} : C.z ^ a = C.z ^ b ↔ a ≡ b [MOD 2]

z^a = z^b in the cover iff a ≡ b [MOD 2].

theorem GQ2.SectionEight.p_z {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) : C.p C.z = 1

p kills z.

theorem GQ2.SectionEight.p_z_pow {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (n : ℕ) : C.p (C.z ^ n) = 1

p kills every z-power.

theorem GQ2.SectionEight.eq_one_or_z_of_mem_ker {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) {w : C.cover} (hw : w ∈ C.p.ker) : w = 1 ∨ w = C.z

Elements of ⟨z⟩ are 1 or z.

theorem GQ2.SectionEight.p_comp_scalarTwist {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (g : Γ →ₜ* C.cover) (c : Γ →ₜ* Multiplicative (ZMod 2)) (γ : Γ) : C.p ((scalarTwist C g c) γ) = C.p (g γ)

The twist projects to the same map: p ∘ (twist g c) = p ∘ g.

theorem GQ2.SectionEight.scalarTwist_left_injective {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (g : Γ →ₜ* C.cover) : Function.Injective (scalarTwist C g)

Freeness of the torsor action: c ↦ scalarTwist C g c is injective.

noncomputable def GQ2.SectionEight.liftDiff {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (g g' : Γ →ₜ* C.cover) (h : ∀ (γ : Γ), C.p (g γ) = C.p (g' γ)) : Γ →ₜ* Multiplicative (ZMod 2)

The difference character of two lifts agreeing under p. Defined so that scalarTwist C g (liftDiff C g g' h) = g' (scalarTwist_liftDiff, transitivity).

Equations

• GQ2.SectionEight.liftDiff C g g' h = { toFun := fun (γ : Γ) => Multiplicative.ofAdd (GQ2.SectionEight.liftChar✝ C g g' γ), map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

theorem GQ2.SectionEight.scalarTwist_liftDiff {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (g g' : Γ →ₜ* C.cover) (h : ∀ (γ : Γ), C.p (g γ) = C.p (g' γ)) : scalarTwist C g (liftDiff C g g' h) = g'

Transitivity of the torsor action: g' is the liftDiff-twist of g.

noncomputable def GQ2.SectionEight.fiberLiftEquiv {Γ : Type} [Group Γ] [TopologicalSpace Γ] {Y : Type} [Group Y] [Finite Y] (C : CentralCover Y) (g₀ : Γ →ₜ* C.cover) : (Γ →ₜ* Multiplicative (ZMod 2)) ≃ { g : Γ →ₜ* C.cover // ∀ (γ : Γ), C.p (g γ) = C.p (g₀ γ) }

The fibre of lifts over a fixed base is a torsor: twisting g₀ by a character bijects Hom_cont(Γ, 𝔽₂) with the continuous-hom lifts sharing g₀'s projection under p. Hence every such fibre has exactly |Hom_cont(Γ, 𝔽₂)| elements — the "8 lifts" of Lemma 8.3.

Equations

• One or more equations did not get rendered due to their size.