§10 — Passage to all finite quotients

Paper §10 (pp. 47–48): Lemma 10.1 (exhaustion by tame boundary frames) and the assembly of eq. (154) |Sur(Γ_A, G)| = |Sur(G_ℚ₂, G)|, which combined with Prop 2.3 gives main_surjection_count (GQ2/Statement.lean) and hence Theorem 1.2.

Proof architecture:

• The 2-core. Lemma 10.1 fixes L = O₂(G) — ONE marked target tameTarget G for all epimorphisms; only the tame frame α : Ttame ↠ G/O₂(G) varies. The image of the source's pro-2 wild kernel under any epimorphism is a normal 2-subgroup, hence lands in O₂(G) automatically — so the E = 0 boundary-framing condition is the fixed-frame condition, the fixed-frame sets are literally BoundaryLifts, and no Möbius/poset induction is needed. Mathlib has no pCore; twoCore and its three required properties are defined here.

• Γ-generic form. The paper's "for either source" is encoded hypothesis-side: lemma_10_1 and card_contSurj_eq are stated over any (Γ, b) with htame (the tame coordinate of b is onto) and hwild (its kernel is pro-2); these are proved for each source — the G_ℚ₂ side from the BoundaryMaps clauses (tameF_surjective, wild_isProP), the Γ_A side from the generator clauses + isProP_wildCore.

• Trivial decoration. E = 0 is E₀ := PUnit (hE2 and the ψ̄-condition are trivial).

• Splice geometry: Statement.lean is imported by GammaA/FoxHeisenberg, i.e. it sits UPSTREAM of the whole tower, so main_surjection_count cannot be proven in place. The proof lives here as main_surjection_count', while the upstream statement points to this theorem. The two AbsGalQ2 topology hypotheses remain explicit instance binders rather than global instances.

The 2-core O₂(G)

The family of normal 2-subgroups is directed (the join of two normal 2-subgroups is again a normal 2-subgroup, by the second isomorphism theorem and closure of p-groups under extensions), so its sSup is itself a normal 2-subgroup — the largest one.

def GQ2.SectionTen.twoCore (G : Type u_1) [Group G] : Subgroup G

The 2-core O₂(G): the join of all normal 2-subgroups of G.

Equations

• GQ2.SectionTen.twoCore G = sSup {N : Subgroup G | N.Normal ∧ IsPGroup 2 ↥N}

instance GQ2.SectionTen.twoCore_normal (G : Type u_1) [Group G] : (twoCore G).Normal

O₂(G) ◁ G (an sSup of normal subgroups is normal).

theorem GQ2.SectionTen.twoCore_isPGroup (G : Type u_1) [Group G] [Finite G] : IsPGroup 2 ↥(twoCore G)

O₂(G) is a 2-group (Sylow.sSup_of_normal: the sSup of a family of normal 2-subgroups is a 2-group — the extension/Sylow content lives in mathlib; [Finite G], which §10 always has).

theorem GQ2.SectionTen.le_twoCore {G : Type u_2} [Group G] {N : Subgroup G} (hN : N.Normal) (h2 : IsPGroup 2 ↥N) : N ≤ twoCore G

Every normal 2-subgroup lies in the 2-core.

The §10 target and frames (E = 0)

@[reducible, inline]

abbrev GQ2.SectionTen.E₀ : Type

The trivial decoration group (E = 0 of Theorem 4.2's §10 consumption).

Equations

• GQ2.SectionTen.E₀ = PUnit.{1}

instance GQ2.SectionTen.instDiscreteTopologyQuotientSubgroupTwoCore (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] : DiscreteTopology (G ⧸ twoCore G)

The quotient head G/O₂(G) of a finite discrete group is discrete (the quotient topology is coinduced, so every set is open).

noncomputable def GQ2.SectionTen.tameTarget (G : Type) [Group G] [Finite G] : MarkedTarget (G ⧸ twoCore G) E₀ G

The §10 marked target 𝒴_G = (G, O₂(G), π, θ = 0): the single boundary-framed marked target through which ALL epimorphisms onto G are counted (Lemma 10.1).

Equations

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

noncomputable def GQ2.SectionTen.tameFrame {H : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] (α : ↑Ttame.toProfinite.toTop →ₜ* H) (hα : Function.Surjective ⇑α) : BoundaryFrame H E₀

The §10 boundary frame of a tame frame α : Ttame ↠ H (decoration E₀ trivial, ψ̄ = 1).

Equations

• GQ2.SectionTen.tameFrame α hα = { alpha := α, alpha_surjective := hα, exponent_two := GQ2.SectionTen.tameFrame._proof_1, psiBar := 1 }

def GQ2.SectionTen.TameFrames (G : Type) [Group G] [TopologicalSpace G] : Type

The tame-frame index of Lemma 10.1: continuous surjections Ttame ↠ G/O₂(G). Finite because Ttame is topologically 2-generated (gen_ttame_quotient); the finiteness instance is the Lemma 10.1 proof's.

Equations

• GQ2.SectionTen.TameFrames G = { α : ↑GQ2.Ttame.toProfinite.toTop →ₜ* G ⧸ GQ2.SectionTen.twoCore G // Function.Surjective ⇑α }

theorem GQ2.SectionTen.ttame_tfg : ∃ (s : Finset ↑Ttame.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤

Ttame is topologically finitely generated (by σ, τ): topGen_ttame in the Finset form consumed by the t.f.g.-hom-finiteness machinery. [the Lemma 10.1 proof]

instance GQ2.SectionTen.instFiniteTameFrames (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : Finite (TameFrames G)

The tame-frame index is finite (so Lemma 10.1's sum is a finite sum): continuous homomorphisms from the topologically 2-generated Ttame into the finite discrete G/O₂(G) form a finite type. [the Lemma 10.1 proof]

The tame coordinate of a boundary map

noncomputable def GQ2.SectionTen.tameCoord {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) : Γ →ₜ* ↑Ttame.toProfinite.toTop

The tame coordinate pr₁ ∘ b : Γ → Ttame of a boundary map b : Γ → ∂bd. For the two sources this is B.tameA resp. B.tameF on the nose (bA_apply_coe/bF_apply_coe).

Equations

• GQ2.SectionTen.tameCoord b = { toFun := fun (γ : Γ) => (↑(b γ)).1, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem GQ2.SectionTen.tameCoord_apply {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (γ : Γ) : (tameCoord b) γ = (↑(b γ)).1

Lemma 10.1 — exhaustion by tame boundary frames

theorem GQ2.SectionTen.map_wildKer_le_twoCore {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] (hwild : IsProP 2 ↥(tameCoord b).ker) (f : ContSurj Γ G) : Subgroup.map (↑f).toMonoidHom (tameCoord b).ker ≤ twoCore G

The image of the wild kernel under a continuous epimorphism f : Γ ↠ G lands in the 2-core: it is normal (image of a kernel under a surjection) and a 2-group (the pro-2 image bridge isPGroup_map_of_isProP). [the Lemma 10.1 proof]

noncomputable def GQ2.SectionTen.inducedHom {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] (htame : Function.Surjective ⇑(tameCoord b)) (hwild : IsProP 2 ↥(tameCoord b).ker) (f : ContSurj Γ G) : ↑Ttame.toProfinite.toTop →* G ⧸ twoCore G

The descended homomorphism of Lemma 10.1's forward map: π ∘ f kills the wild kernel (map_wildKer_le_twoCore), so it factors through the surjective tame coordinate as α_f : Ttame →* G/O₂(G). [the Lemma 10.1 proof]

Equations

• GQ2.SectionTen.inducedHom b G htame hwild f = ((GQ2.SectionTen.tameCoord b).liftOfSurjective htame) ⟨(QuotientGroup.mk' (GQ2.SectionTen.twoCore G)).comp (↑f).toMonoidHom, ⋯⟩

theorem GQ2.SectionTen.inducedHom_tameCoord {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] (htame : Function.Surjective ⇑(tameCoord b)) (hwild : IsProP 2 ↥(tameCoord b).ker) (f : ContSurj Γ G) (γ : Γ) : (inducedHom b G htame hwild f) ((tameCoord b) γ) = (QuotientGroup.mk' (twoCore G)) (↑f γ)

The defining property of the descent: α_f ∘ (pr₁ ∘ b) = π ∘ f pointwise. [the Lemma 10.1 proof]

noncomputable def GQ2.SectionTen.inducedFrame {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [CompactSpace Γ] (htame : Function.Surjective ⇑(tameCoord b)) (hwild : IsProP 2 ↥(tameCoord b).ker) (f : ContSurj Γ G) : TameFrames G

The induced tame frame of a continuous epimorphism f : Γ ↠ G (Lemma 10.1, forward map): the descent α_f, continuous because the tame coordinate of a compact source is a topological quotient map (a continuous surjection onto the Hausdorff Ttame is closed, hence quotient), and surjective because π ∘ f is. [the Lemma 10.1 proof; the [CompactSpace Γ] binder is a statement amendment over the §10 statement layer skeleton — see docs/section10-extraction.md]

Equations

• GQ2.SectionTen.inducedFrame b G htame hwild f = ⟨let __MonoidHom := GQ2.SectionTen.inducedHom b G htame hwild f; { toMonoidHom := __MonoidHom, continuous_toFun := ⋯ }, ⋯⟩

theorem GQ2.SectionTen.lemma_10_1 {Γ : Type} [Group Γ] [TopologicalSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] [CompactSpace Γ] (htame : Function.Surjective ⇑(tameCoord b)) (hwild : IsProP 2 ↥(tameCoord b).ker) : Nonempty (ContSurj Γ G ≃ (α : TameFrames G) × BoundaryLifts b (tameFrame ↑α ⋯) (tameTarget G))

Lemma 10.1 (Exhaustion by tame boundary frames), partition form: for a source (Γ, b) whose tame coordinate is onto with pro-2 kernel, the ordinary continuous epimorphisms Γ ↠ G are exactly the boundary-framed epimorphisms onto the single target tameTarget G, fibered over the (finitely many) tame frames — f lands in the fiber of its induced frame α_f (well-defined because f(ker (pr₁ ∘ b)) is a normal 2-subgroup of G, hence ≤ O₂(G)); distinct frames give disjoint fibers (α is determined by α ∘ (pr₁ ∘ b)). [the Lemma 10.1 proof; [CompactSpace Γ] added over the §10 statement layer skeleton — the descent's continuity needs the tame coordinate to be a quotient map. Both sources are profinite, so this is free at the final count assembly.]

theorem GQ2.SectionTen.card_contSurj_eq {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] (b : Γ →ₜ* ↥boundarySubgroup) (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (htame : Function.Surjective ⇑(tameCoord b)) (hwild : IsProP 2 ↥(tameCoord b).ker) (hfg : ∃ (s : Finset Γ), (Subgroup.closure ↑s).topologicalClosure = ⊤) : Nat.card (ContSurj Γ G) = ∑ᶠ (α : TameFrames G), exactImageCount b (tameFrame ↑α ⋯) (tameTarget G)

Lemma 10.1, counting form (the (154)-assembly workhorse): the ordinary surjection count is the sum of the fixed-frame exact-image counts over all tame frames. [the Lemma 10.1 proof; finiteness of the fibers from hfg via finite_boundaryLifts (whence the [TotallyDisconnectedSpace Γ] binder, an amendment over the §10 statement layer skeleton like lemma_10_1's [CompactSpace Γ]), of the index from Ttame t.f.g.]

Eq. (154) and the surjection-count theorem

eq_154 (Nat.card (ContSurj GammaA G) = Nat.card (ContSurj AbsGalQ2 G)) and main_surjection_count' (contSurjCount G = admissibleCount G) are proved in GQ2/SectionTenSources.lean, not here: eq_154's A-side needs the concrete boundaryMapsWitness (the Γ_A tame surjectivity phiA_surjective is witness-specific), and GQ2/BoundaryMapsWitness.lean is downstream of this file. This placement avoids an import cycle; both the source-specific theorem and the thm_4_2 it consumes are proved in the downstream assembly.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (154) = ⟦eq-app-cup-convention⟧ [≥ drift window; verify against v428 tex]
• Lemma 10.1 = ⟦lem-tameframeexhaustion⟧
• Prop 2.3 = ⟦prop-epi-semantics⟧
• Theorem 1.2 = ⟦thm-main⟧
• Theorem 4.2 = ⟦thm-fixedframe⟧