Lemma 2.5 — one-sided profinite reconstruction

Paper Lemma 2.5: Let P be a topologically finitely generated profinite group and Q any profinite group. If |Sur(P, H)| = |Sur(Q, H)| for every finite group H, then P ≅ Q.

The proof (paper): finiteness of Sur(P, Pₙ) gives, by compactness, an epimorphism Q ↠ P; symmetrically P ↠ Q; the composite P ↠ Q ↠ P is a surjective endomorphism of a topologically finitely generated profinite group, which is Hopfian, hence an isomorphism.

The proof below packages the Hopfian property, constructs compatible surjections through finite quotients, and applies compactness to obtain the required inverse maps.

def GQ2.ContSurj (P : Type u_1) [Group P] [TopologicalSpace P] (H : Type u_2) [Group H] [TopologicalSpace H] : Type (max u_1 u_2)

Continuous surjections from a topological group P onto a finite (discrete) group H.

Equations

• GQ2.ContSurj P H = { f : P →ₜ* H // Function.Surjective ⇑f }

noncomputable def GQ2.continuousMulEquivOfBijective {P : Type u_1} {Q : Type u_2} [Group P] [TopologicalSpace P] [Group Q] [TopologicalSpace Q] [CompactSpace P] [T2Space Q] (f : P →ₜ* Q) (hf : Function.Bijective ⇑f) : P ≃ₜ* Q

A bijective continuous group homomorphism from a compact group to a Hausdorff group is a topological isomorphism. (Mirrors ProfiniteGrp.continuousMulEquivLimittoFiniteQuotientFunctor, but stated for bare types so it can be used on the reconstruction hypotheses.)

Equations

• GQ2.continuousMulEquivOfBijective f hf = { toEquiv := ⋯.homeoOfEquivCompactToT2.toEquiv, map_mul' := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem GQ2.finite_continuousMonoidHom {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hPfg : ∃ (s : Finset P), (Subgroup.closure ↑s).topologicalClosure = ⊤) (H : Type u_2) [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] : Finite (P →ₜ* H)

For a topologically finitely generated profinite group P and a finite discrete group H, there are only finitely many continuous homomorphisms P → H: such a hom is determined by its values on a topological generating set (it is continuous, and two continuous homs agreeing on a dense subgroup agree everywhere), giving an injection into s → H.

theorem GQ2.profinite_hopfian {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hPfg : ∃ (s : Finset P), (Subgroup.closure ↑s).topologicalClosure = ⊤) (φ : P →ₜ* P) (hφ : Function.Surjective ⇑φ) : Function.Injective ⇑φ

Profinite Hopfian property (paper Lemma 2.5, key input): a continuous surjective endomorphism of a topologically finitely generated profinite group is injective. Non-standard; absent from Mathlib. Proof idea: a topologically f.g. profinite group has only finitely many open subgroups of each index, so a surjective endomorphism acts as a surjection — hence a bijection — on each finite quotient level, forcing injectivity in the limit.

theorem GQ2.contSurj_quotient_nonempty_finite {S R : Type} [Group S] [TopologicalSpace S] [IsTopologicalGroup S] [CompactSpace S] [TotallyDisconnectedSpace S] [Group R] [TopologicalSpace R] [IsTopologicalGroup R] [CompactSpace R] [TotallyDisconnectedSpace R] (hRfin : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Finite (ContSurj R H)) (h : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Nat.card (ContSurj R H) ≤ Nat.card (ContSurj S H)) (V : OpenNormalSubgroup R) : Nonempty (ContSurj S (R ⧸ ↑V.toOpenSubgroup)) ∧ Finite (ContSurj S (R ⧸ ↑V.toOpenSubgroup))

The arithmetic heart of exists_contSurj_of_card_le, isolated and proved: under its hypotheses, S continuously surjects onto every finite quotient R ⧸ V of R, and only finitely many ways. (The projection witnesses ContSurj R (R ⧸ V), which is finite by hRfin, so its count is ≥ 1; the count hypothesis h transports this to S, and Nat.card_pos_iff unpacks it as nonempty-and-finite — the latter automatically, since an infinite level set would have count 0.) These level sets, over V : OpenNormalSubgroup R (a SemilatticeInf, hence cofiltered), are the nonempty finite objects used in the compactness assembly below.

König assembly for exists_contSurj_of_card_le

The compatible surjections onto the finite quotients are organized by the functor konigFunctor below (U ↦ {S ↠ R/U}), whose level sets are nonempty and finite by contSurj_quotient_nonempty_finite; nonempty_sections_of_finite_cofiltered_system (König) then picks a compatible choice. The compatible family is assembled into the surjection S ↠ R by an elementary embedding of R into the product of its finite quotients + two applications of Cantor's intersection theorem — see the exists_contSurj_of_card_le proof.

noncomputable def GQ2.projMap {R : Type} [Group R] [TopologicalSpace R] {U U' : Subgroup R} [U.Normal] [U'.Normal] [DiscreteTopology (R ⧸ U)] (hle : U ≤ U') : R ⧸ U →ₜ* R ⧸ U'

The projection R/U ↠ R/U' for U ≤ U' (both open normal, so the quotients are discrete).

Equations

• GQ2.projMap hle = { toMonoidHom := QuotientGroup.map U U' (MonoidHom.id R) hle, continuous_toFun := ⋯ }

theorem GQ2.projMap_surjective {R : Type} [Group R] [TopologicalSpace R] {U U' : Subgroup R} [U.Normal] [U'.Normal] [DiscreteTopology (R ⧸ U)] (hle : U ≤ U') : Function.Surjective ⇑(projMap hle)

noncomputable def GQ2.konigFunctor {R : Type} [Group R] [TopologicalSpace R] {S : Type} [Group S] [TopologicalSpace S] [IsTopologicalGroup R] [CompactSpace R] [TotallyDisconnectedSpace R] : CategoryTheory.Functor (OpenNormalSubgroup ↑(ProfiniteGrp.of R).toProfinite.toTop) Type

The König functor: U ↦ {continuous surjections S ↠ R/U}, with restriction along U ≤ U' (post-composition with projMap). Its sections are the compatible families of surjections.

Equations

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

theorem GQ2.exists_contSurj_of_card_le {S R : Type} [Group S] [TopologicalSpace S] [IsTopologicalGroup S] [CompactSpace S] [TotallyDisconnectedSpace S] [Group R] [TopologicalSpace R] [IsTopologicalGroup R] [CompactSpace R] [TotallyDisconnectedSpace R] (hRfin : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Finite (ContSurj R H)) (h : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Nat.card (ContSurj R H) ≤ Nat.card (ContSurj S H)) : Nonempty (ContSurj S R)

Surjection assembly from surjection counts (paper Lemma 2.5, compactness input): if a profinite group S continuously surjects onto at least as many finite groups (counted with multiplicity) as a profinite group R whose surjection sets are all finite (hRfin), then S continuously surjects onto R. Finiteness of the target level sets is essential: without it Nat.card collapses an infinite level set to 0 and the count hypothesis becomes vacuous (e.g. R = (ℤ/2)^ℕ, S = 1).

This is standard profinite group theory (Ribes–Zalesskiĭ, Profinite Groups, Ch. 1–2). Proof:

• For each V : OpenNormalSubgroup R, contSurj_quotient_nonempty_finite gives the level set {S ↠ R/V} nonempty and finite (from hRfin + the count hypothesis h). These, with the restriction maps projMap for V' ≤ V, form konigFunctor : OpenNormalSubgroup R ⥤ Type, a cofiltered system of nonempty finite sets; nonempty_sections_of_finite_cofiltered_system (König) supplies a compatible family of surjections σ V : S ↠ R/V.
• R embeds into Q := ∏_V R/V via e = (mk_V)_V (injective since the open normal subgroups meet in 1; a closed embedding as R is compact and Q is Hausdorff). Cantor's intersection theorem in the compact R realizes each compatible family (σ V s)_V as e r, so ψ := e⁻¹ ∘ Φ (Φ = (σ V)_V : S → Q) is a well-defined continuous homomorphism with mk_V ∘ ψ = σ V.
• A second Cantor intersection, in the compact S, shows ψ surjective: for each r, the compatible closed sets {s | σ V s = mk_V r} meet, giving s with ψ s = r.

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 : Finset P), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hequiv : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Nonempty (ContSurj P H ≃ 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.

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 : Finset P), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hQfg : ∃ (s : Finset Q), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hcount : ∀ (H : Type) [inst : Group H] [inst_1 : TopologicalSpace H] [DiscreteTopology H] [Finite H], Nat.card (ContSurj P H) = Nat.card (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.

theorem GQ2.reconstruction_finite {P Q : Type} [Group P] [Group Q] [Finite P] [Finite Q] (hcount : ∀ (H : Type) [inst : Group H] [Finite H], Nat.card { f : P →* H // Function.Surjective ⇑f } = Nat.card { f : Q →* H // Function.Surjective ⇑f }) : Nonempty (P ≃* Q)

Finite core of the reconstruction lemma. For finite groups, having the same number of surjections onto every finite group forces an isomorphism. This is the counting heart of Lemma 2.5 (the profinite case reduces to it, level by level, along the finite quotient system): |Sur(P,P)| ≥ 1 gives a surjection Q ↠ P, symmetrically P ↠ Q, so |P| = |Q|, and a surjection between equinumerous finite groups is an isomorphism.

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

• Lemma 2.5 = ⟦lem-reconstruction⟧