11. Passage to all finite quotients🔗

Lemma11.1

uses 0used by 1✓L∃∀N

Lemma 10.1 of the paper (Exhaustion by tame boundary frames).

Let G be finite and put L=O_2(G). For either source \Gamma, every epimorphism f:\Gamma\twoheadrightarrow G determines a unique tame boundary frame

\TA\twoheadrightarrow G/L.

Conversely, with decoration E=0, a boundary-framed epimorphism to G with a fixed tame frame is exactly an ordinary epimorphism to G inducing that frame. Distinct tame frames give disjoint sets of epimorphisms.

Lean code for Lemma11.1●2 theorems

theoremdefined in GQ2/SectionTen.lean

complete

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

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

theoremdefined in GQ2/SectionTen.lean

complete

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

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

Proof for Lemma 11.1

uses 1

Proved in §10 of the paper. Ingredients: Proposition 4.2.