3. The candidate as a profinite group🔗

Proposition3.1

groupuses 0used by 1✓L∃∀N

Proposition 2.3 of the paper (Epimorphic finite-quotient semantics).

For every finite group G, epimorphisms \GA\twoheadrightarrow G are in natural bijection with generating quadruples (\sigma,\tau,x_0,x_1)\in G^4 satisfying (5), (6), and x_0,x_1\in O_2(G).

Lean code for Proposition3.1●2 declarations

defdefined in GQ2/Prop23.lean

complete

def GQ2.contSurjEquivAdmissible (G : Type) [Group G] [TopologicalSpace G]
  [DiscreteTopology G] [Finite G] :
  GQ2.ContSurj
      (↑(GQ2.FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ GQ2.NA) G ≃
    { t // t.Admissible }

def GQ2.contSurjEquivAdmissible (G : Type)
  [Group G] [TopologicalSpace G]
  [DiscreteTopology G] [Finite G] :
  GQ2.ContSurj
      (↑(GQ2.FreeProfiniteGroup
                (Fin
                  4)).toProfinite.toTop ⧸
        GQ2.NA)
      G ≃
    { t // t.Admissible }

**Prop. 2.3, bijection form** (paper §2.2): continuous surjections `Γ_A ↠ G` correspond to
admissible markings of `G`.  (Stated on the underlying quotient `F₄ ⧸ N_A`, to which `GammaA`
is definitionally equal.)

theoremdefined in GQ2/Prop23.lean

complete

theorem GQ2.prop_2_3 (G : Type) [Group G] [TopologicalSpace G]
  [DiscreteTopology G] [Finite G] :
  Nat.card (GQ2.ContSurj (↑GQ2.GammaA.toProfinite.toTop) G) =
    GQ2.admissibleCount G

theorem GQ2.prop_2_3 (G : Type) [Group G]
  [TopologicalSpace G]
  [DiscreteTopology G] [Finite G] :
  Nat.card
      (GQ2.ContSurj
        (↑GQ2.GammaA.toProfinite.toTop)
        G) =
    GQ2.admissibleCount G

**Proposition 2.3** (paper §2.2): the number of continuous surjections `Γ_A ↠ G` onto a
finite discrete group equals the number of admissible marked generating quadruples in `G` —
in exactly the `hΓA` shape that `main_presentation` (`GQ2/Statement.lean`) consumes.

Lemma3.2

groupuses 0used by 1✓L∃∀N

Lemma 2.5 of the paper (One-sided profinite reconstruction).

Let P be a topologically finitely generated profinite group and let Q be any profinite group. If

|\Sur(P,H)|=|\Sur(Q,H)|

for every finite group H, then P\cong Q.

Lean code for Lemma3.2●2 theorems

theoremdefined in GQ2/Reconstruction.lean

complete

theorem GQ2.reconstruction_of_equinum {P Q : Type} [Group P]
  [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P]
  [TotallyDisconnectedSpace P] [Group Q] [TopologicalSpace Q]
  [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q]
  (hPfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hequiv :
    ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H]
      [DiscreteTopology H] [Finite H],
      Nonempty (GQ2.ContSurj P H ≃ GQ2.ContSurj Q H)) :
  Nonempty (P ≃ₜ* Q)

theorem GQ2.reconstruction_of_equinum {P Q : Type}
  [Group P] [TopologicalSpace P]
  [IsTopologicalGroup P] [CompactSpace P]
  [TotallyDisconnectedSpace P] [Group Q]
  [TopologicalSpace Q]
  [IsTopologicalGroup Q] [CompactSpace Q]
  [TotallyDisconnectedSpace Q]
  (hPfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hequiv :
    ∀ (H : Type) [inst : Group H]
      [inst_1 : TopologicalSpace H]
      [DiscreteTopology H] [Finite H],
      Nonempty
        (GQ2.ContSurj P H ≃
          GQ2.ContSurj Q H)) :
  Nonempty (P ≃ₜ* Q)

**Lemma 2.5 (equinumerosity form).**  `P` is a topologically finitely generated profinite group,
`Q` is profinite, and for every finite group `H` the continuous-surjection sets are *equinumerous*
(`ContSurj P H ≃ ContSurj Q H`); then `P ≅ Q` as topological groups.  Equinumerosity, unlike
equality of `Nat.card`, forces the counts to be genuinely finite (via `P`'s finiteness) and so is
not vacuous on infinite level sets; it is the most general faithful reading of "the same *number*
of surjections"
and does not need `Q` finitely generated as a separate hypothesis (it follows).  Proved in full
modulo the standard compactness input `exists_contSurj_of_card_le`.

theoremdefined in GQ2/Reconstruction.lean

complete

theorem GQ2.reconstruction {P Q : Type} [Group P] [TopologicalSpace P]
  [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P]
  [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q]
  [TotallyDisconnectedSpace Q]
  (hPfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hQfg : ∃ s, (Subgroup.closure ↑s).topologicalClosure = ⊤)
  (hcount :
    ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H]
      [DiscreteTopology H] [Finite H],
      Nat.card (GQ2.ContSurj P H) = Nat.card (GQ2.ContSurj Q H)) :
  Nonempty (P ≃ₜ* Q)

theorem GQ2.reconstruction {P Q : Type} [Group P]
  [TopologicalSpace P]
  [IsTopologicalGroup P] [CompactSpace P]
  [TotallyDisconnectedSpace P] [Group Q]
  [TopologicalSpace Q]
  [IsTopologicalGroup Q] [CompactSpace Q]
  [TotallyDisconnectedSpace Q]
  (hPfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hQfg :
    ∃ s,
      (Subgroup.closure
            ↑s).topologicalClosure =
        ⊤)
  (hcount :
    ∀ (H : Type) [inst : Group H]
      [inst_1 : TopologicalSpace H]
      [DiscreteTopology H] [Finite H],
      Nat.card (GQ2.ContSurj P H) =
        Nat.card (GQ2.ContSurj Q H)) :
  Nonempty (P ≃ₜ* Q)

**Lemma 2.5 (one-sided profinite reconstruction).**  `P` and `Q` are topologically finitely
generated profinite groups with the same (finite) number of continuous surjections onto every finite
group; then `P ≅ Q` as topological groups.

Both `P` and `Q` are assumed topologically finitely generated (`hPfg`, `hQfg`).  The finite
generation of `Q` is essential and *cannot* be dropped while keeping the `Nat.card` hypothesis: for
`Q` not finitely generated some `ContSurj Q H` is infinite, so `Nat.card` reads it as `0` and the
count equality no longer means "equally many".  (Counterexample without `hQfg`: `P = Unit`,
`Q = (ℤ/2)^ℕ` satisfy `hcount` but are not isomorphic.)  With both groups finitely generated the
counts are genuinely finite, so `hcount` is real equinumerosity and this reduces to
`reconstruction_of_equinum`.

Proof for Lemma 3.2

uses 1

Proved in §2 of the paper. Ingredients: Proposition 1.1.