§8: the eight-lift partition (Lemma 8.3) and the half-torsor count (Lemma 8.6)

Lemma 8.3 (display (124)): the eight-lift partition of the master set of cover lifts. Lemma 8.6 (displays (127)/(128)): the radical-edge half-torsor count, per source.

Lemma 8.3: the eight-lift partition (display (124))

The proof assembles two fibrations of the master set R = {g : Γ →ₜ* Ỹ // (p∘g).range = J ∧ boundary-framed}: by image g ↦ g.range (a Nat.card_sigma over subgroups J' ≤ Ỹ with p(J') = J, each fibre ≃ BoundaryLifts(stratum J') by corestriction) — this is the RHS; and by projection g ↦ p∘g (each fibre the torsor ≃ Hom_cont(Γ,𝔽₂) = 8 of fiberLiftEquiv) — this is 8 · u^β. Needs Γ topologically finitely generated (hfg), the finite_boundaryLifts shape, to finitize the counted sets.

@[reducible, inline]

abbrev GQ2.SectionEight.masterLifts {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) : Type

The master set of Lemma 8.3: cover lifts whose projection has image exactly J and is boundary-framed for T. The two fibrations of this set (by image g ↦ g.range and by projection g ↦ p∘g) give the two sides of (124).

Equations

• GQ2.SectionEight.masterLifts b F T C J = { g : Γ →ₜ* C.cover // (C.pCont.comp g).range = J ∧ GQ2.IsBoundaryLift b F T (C.pCont.comp g) }

theorem GQ2.SectionEight.stratum_surj {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] {T : MarkedTarget H E Y} {C : CentralCover Y} {J : Subgroup Y} (hJ : Function.Surjective ⇑(T.piY.comp J.subtype)) {J' : Subgroup C.cover} (hJ' : Subgroup.map C.p J' = J) : Function.Surjective ⇑((C.pullTarget T).piY.comp J'.subtype)

A subgroup of the cover projecting onto J also projects onto H — so its pullback stratum is well-defined.

theorem GQ2.SectionEight.lemma_8_3 {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] [DiscreteTopology Y] [Finite Y] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) (b : Γ →ₜ* ↥boundarySubgroup) (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (C : CentralCover Y) (hscalar : Nat.card (Γ →ₜ* Multiplicative (ZMod 2)) = 8) (J : Subgroup Y) (hJ : Function.Surjective ⇑(T.piY.comp J.subtype)) : 8 * liftableCount b F T C J hJ = ∑ᶠ (J' : Subgroup C.cover) (_ : J' ∈ {J' : Subgroup C.cover | Subgroup.map C.p J' = J}), exactImageCountOn b F (C.pullTarget T) J'

Central-cover exact-image transform. For a scalar central cover, eight times the liftable count over an image subgroup J equals the sum of exact-image counts over the subgroups of the cover mapping onto J. This is the result currently numbered Lemma 8.3 in the paper (stable paper identifier lem-covertransform).

Lemma 8.6: radical edge and the half-torsor count

The §8 datum: a central double cover of B whose restriction to the elementary abelian M ◁ B is a quadratic form (the square map into ⟨z⟩) with polar radical T and vanishing on T. The H¹-valued edge class of (128) is carried operationally: the cover descends to B/T iff p⁻¹(T) has a normal complement missing z (the paper's own descent clause), and "edge ≠ 0" is the negation.

theorem GQ2.SectionEight.lemma_8_6_gammaA {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) (hedge : D.NoDescent) (ρ : ↑GammaA.toProfinite.toTop →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6 (half-torsor count), candidate source: with a nonzero radical edge, for every lower epimorphism ρ : Γ_A ↠ B/M, exactly half of the unrestricted M-lifts of ρ satisfy the central relation. (The degree-one duality making the variation functional (127) nonzero is §5 content for Γ_A — B7 enters through 5.15/5.16.) [the §8 proof layer statement; proof = O-half.]

theorem GQ2.SectionEight.lemma_8_6_local {Bg : Type} [Group Bg] [TopologicalSpace Bg] [DiscreteTopology Bg] [Finite Bg] (D : RadicalCoverData Bg) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hfg : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hedge : D.NoDescent) (ρ : AbsGalQ2 →ₜ* Bg ⧸ D.M) (hρ : Function.Surjective ⇑ρ) : 2 * Nat.card { f : MLifts D ρ // MLifts.Central D f } = Nat.card (MLifts D ρ)

Lemma 8.6 (half-torsor count), local source: as lemma_8_6_gammaA, for G_ℚ₂ (degree-one duality = B6). The standing §8 side conditions are explicit, following lemma_8_2_local (compactness) and lemma_8_3 (hfg topological finite generation, the B1-shaped input) precedents — they finitize the counted MLifts. Proof: the central-obstruction framework's central-obstruction engine + the B6 twist of GQ2/RadicalEdgeLocal.lean (half_torsor_local). Ax: B6, B7.