One-sided profinite reconstruction

This file is a self-contained, reusable module of profinite group theory. It is mathematically independent of the Q₂ word: it formalises the one-sided reconstruction lemma used at the very end of the main proof.

The headline result is profinite_reconstruction_of_surj_counts: if P is a topologically finitely generated profinite group, Q is any profinite group, and P and Q admit the same number of surjective continuous homomorphisms onto every finite group, then P ≅ Q.

Faithfulness note on the cardinality

The manuscript states the hypothesis as |Sur(P,H)| = |Sur(Q,H)| and its proof derives finiteness of Sur(Q,H) from finiteness of Sur(P,H) together with this equality (manuscript, proof of Lemma 2.5, first paragraph). We therefore use genuine cardinality Cardinal.mk rather than Fintype.card:

• Fintype.card (Sur P (of G)) does not even elaborate, because there is no Fintype (P ⟶ of G) instance available a priori (finiteness needs P t.f.g., and the Q-side is not known finite before the argument runs); and
• with Nat.card the theorem is false — take P trivial and Q an infinite-rank free profinite group: then Nat.card (Sur Q (ℤ/2)) = 0 = Nat.card (Sur P (ℤ/2)) for the wrong reason (the set is infinite), yet P ≇ Q.

Cardinal.mk records the genuine cardinality, equals Fintype.card when a Fintype instance is present (Nat.card_eq_fintype_card/Cardinal.mk_fintype), and makes the one-sided lemma a true statement with only P finitely generated.

Main statements

• SurjContHom — a surjective continuous homomorphism of profinite groups.
• TopologicallyFinitelyGenerated — a finite set whose generated subgroup is dense.
• tfg_hom_to_finite_finite — a t.f.g. profinite group has only finitely many continuous homomorphisms to a fixed finite group.
• profinite_epimorphism_from_compatible_finite_quotients — a compactness / finite-intersection assembly of compatible finite quotient surjections.
• tfg_profinite_hopfian — a t.f.g. profinite group is Hopfian.
• profinite_reconstruction_of_surj_counts — the assembled reconstruction lemma.

structure Q2Presentation.Profinite.SurjContHom (P Q : ProfiniteGrp.{u}) : Type u

A surjective continuous homomorphism of profinite groups (a profinite "epimorphism", recorded as data: the morphism together with surjectivity of the underlying map).

• hom : P ⟶ Q

  The underlying morphism of profinite groups.

• surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.hom)

  The underlying map is surjective.

@[reducible, inline]

abbrev Q2Presentation.Profinite.SurjContEnd (P : ProfiniteGrp.{u}) : Type u

A surjective continuous endomorphism of a profinite group.

Equations

• Q2Presentation.Profinite.SurjContEnd P = Q2Presentation.Profinite.SurjContHom P P

def Q2Presentation.Profinite.TopologicallyFinitelyGenerated (P : ProfiniteGrp.{u}) : Prop

A profinite group is topologically finitely generated if some finite subset generates a dense subgroup, i.e. the topological closure of the subgroup it generates is the whole group.

Equations

• Q2Presentation.Profinite.TopologicallyFinitelyGenerated P = ∃ (S : Finset ↑P.toProfinite.toTop), (Subgroup.closure ↑S).topologicalClosure = ⊤

theorem Q2Presentation.Profinite.SurjContHom.hom_injective {P Q : ProfiniteGrp.{u}} : Function.Injective hom

A surjective continuous homomorphism is determined by its underlying morphism (the surjectivity field is a proposition).

instance Q2Presentation.Profinite.SurjContHom.instFinite {P Q : ProfiniteGrp.{u}} [Finite (P ⟶ Q)] : Finite (SurjContHom P Q)

If there are only finitely many morphisms P ⟶ Q, then there are only finitely many surjective ones.

def Q2Presentation.Profinite.SurjContHom.comp {P Q R : ProfiniteGrp.{u}} (f : SurjContHom P Q) (g : SurjContHom Q R) : SurjContHom P R

The composite of two surjective continuous homomorphisms.

Equations

• f.comp g = { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, surj := ⋯ }

Finitely many homomorphisms to a finite group

theorem Q2Presentation.Profinite.hom_ext_of_dense {P R : ProfiniteGrp.{u}} [T2Space ↑R.toProfinite.toTop] {K : Subgroup ↑P.toProfinite.toTop} (hK : K.topologicalClosure = ⊤) {f g : P ⟶ R} (h : Set.EqOn ⇑(ProfiniteGrp.Hom.hom f) ⇑(ProfiniteGrp.Hom.hom g) ↑K) : f = g

A continuous homomorphism out of a profinite group is determined by its values on any dense subset: two morphisms to a (finite, hence T2) profinite group that agree on a dense subgroup are equal.

theorem Q2Presentation.Profinite.tfg_hom_to_finite_finite (P : ProfiniteGrp.{u}) (hP : TopologicallyFinitelyGenerated P) (H : ProfiniteGrp.{u}) [Finite ↑H.toProfinite.toTop] : Finite (P ⟶ H)

A topologically finitely generated profinite group has only finitely many continuous homomorphisms to a fixed finite group. A continuous homomorphism is determined by the images of the finite (dense-subgroup-)generating set, so the homomorphism type embeds into S → H, which is finite.

Hopficity

theorem Q2Presentation.Profinite.tfg_profinite_hopfian (P : ProfiniteGrp.{u}) (hP : TopologicallyFinitelyGenerated P) (f : SurjContEnd P) : Function.Bijective ⇑(ProfiniteGrp.Hom.hom f.hom)

A topologically finitely generated profinite group is Hopfian: a surjective continuous endomorphism is automatically bijective.

The argument is the standard Hom-counting one. For a fixed finite quotient P ⧸ N, precomposition φ ↦ f ∘ φ is an injective self-map of the finite set Hom(P, P ⧸ N) (injective because f is surjective), hence surjective; so the quotient map factors through f. Evaluating that factorisation at a hypothetical nontrivial element of ker f (separated from 1 by some open normal N) gives a contradiction.

Compatible finite quotients assemble to an epimorphism

theorem Q2Presentation.Profinite.profinite_epimorphism_from_compatible_finite_quotients (A Q : ProfiniteGrp.{u}) (hfin : ∀ (N : OpenNormalSubgroup ↑Q.toProfinite.toTop), Finite (SurjContHom A (Q.diagram.obj N))) (hne : ∀ (N : OpenNormalSubgroup ↑Q.toProfinite.toTop), Nonempty (SurjContHom A (Q.diagram.obj N))) : Nonempty (SurjContHom A Q)

From compatible finite quotient surjections to a global surjection. If, for every open normal subgroup N of Q, the set of surjections A ↠ Q ⧸ N is finite and nonempty, then the inverse limit of these finite nonempty sets is nonempty (compactness / finite intersection property), giving a surjection A ↠ Q.

This is the topological core of the reconstruction lemma; see CategoryTheory.nonempty_sections_of_finite_cofiltered_system.

The reconstruction lemma

theorem Q2Presentation.Profinite.profinite_reconstruction_of_surj_counts (P Q : ProfiniteGrp.{u}) (hP : TopologicallyFinitelyGenerated P) (h : ∀ (G : Type u) [inst : Group G] [inst_1 : Finite G], Cardinal.mk (SurjContHom P (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (SurjContHom Q (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))) : Nonempty (P ≅ Q)

One-sided profinite reconstruction. Let P be a topologically finitely generated profinite group and Q any profinite group. If for every finite group G the numbers of surjective continuous homomorphisms P ↠ G and Q ↠ G are equal (as cardinals), then P ≅ Q.

The proof builds epimorphisms P ↠ Q and Q ↠ P from the equal counts (each finite quotient receives at least one surjection on the side that is its own quotient, and equal cardinality transports nonemptiness and finiteness across), and then uses Hopficity of the t.f.g. group P to upgrade P ↠ Q to an isomorphism.