Finite-quotient determinacy of profinite groups

A topologically finitely generated profinite group is determined by its continuous finite quotients (TauCeti.IsFiniteContinuousQuotient, defined in TauCeti.Topology.Algebra.Group.FiniteQuotients): if G is topologically finitely generated and the profinite groups G and H have the same continuous finite quotients, then G ≃ₜ* H. Finite generation is assumed on one side only, and is a conclusion on the other.

The theorem is assembled from three implications between finite-quotient data and maps.

• Finite generation descends. If G is topologically finitely generated and every continuous finite quotient of the profinite group H is one of G, then H is topologically finitely generated (IsTopologicallyFinitelyGenerated.of_forall_isFiniteContinuousQuotient).
• Finite-quotient data produces a surjection. If H is a topologically finitely generated compact group and every quotient G ⧸ N of the profinite group G by an open normal subgroup occurs as a continuous quotient of H, then there is a continuous surjection H ↠ G (exists_continuous_surjective_of_forall_isFiniteContinuousQuotient).
• Surjections in both directions are isomorphisms. If G is topologically finitely generated and profinite, continuous surjections G ↠ H and H ↠ G make G ↠ H bijective (IsTopologicallyFinitelyGenerated.bijective_of_surjective_of_surjective, the Hopf property of G), hence a topological isomorphism when H is also compact Hausdorff.

Finite generation cannot be dropped on both sides: for a prime p, the products ∏_{i : ℕ} ℤ/p and ∏_{i : ℝ} ℤ/p have the same continuous finite quotients, namely the finite elementary abelian p-groups, but they have different cardinalities.

Main results

• TauCeti.IsTopologicallyFinitelyGenerated.of_forall_isFiniteContinuousQuotient: a profinite group whose continuous finite quotients all occur for a topologically finitely generated one is topologically finitely generated.
• TauCeti.exists_continuous_surjective_of_forall_isFiniteContinuousQuotient: a topologically finitely generated compact group surjects continuously onto a profinite group all of whose finite quotients it has.
• TauCeti.exists_surjective_and_exists_surjective_of_forall_isFiniteContinuousQuotient_iff: two profinite groups with the same continuous finite quotients, one of them topologically finitely generated, admit continuous surjections in both directions.
• TauCeti.nonempty_continuousMulEquiv_of_forall_isFiniteContinuousQuotient_iff: finite-quotient determinacy: such groups are topologically isomorphic.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 3.2.
• J. D. Dixon, E. W. Formanek, J. C. Poland and L. Ribes, Profinite completions and isomorphic finite quotients, J. Pure Appl. Algebra 23 (1982), 227–231.

theorem TauCeti.IsTopologicallyFinitelyGenerated.of_forall_isFiniteContinuousQuotient {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsTopologicallyFinitelyGenerated G) (h : ∀ (Q : Type v) [inst : Group Q] [Finite Q], IsFiniteContinuousQuotient H Q → IsFiniteContinuousQuotient G Q) : IsTopologicallyFinitelyGenerated H

Finite generation passes to a group with fewer continuous finite quotients. If the topological group G is topologically finitely generated and every continuous finite quotient of the profinite group H occurs as a continuous finite quotient of G, then H is topologically finitely generated.

theorem TauCeti.exists_continuous_surjective_of_forall_isFiniteContinuousQuotient {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] (hH : IsTopologicallyFinitelyGenerated H) (h : ∀ (N : OpenNormalSubgroup G), IsFiniteContinuousQuotient H (G ⧸ ↑N.toOpenSubgroup)) : ∃ (φ : H →* G), Continuous ⇑φ ∧ Function.Surjective ⇑φ

A continuous surjection from finite-quotient data. Let H be a topologically finitely generated compact group and G a profinite group such that every quotient G ⧸ N of G by an open normal subgroup occurs as a continuous finite quotient of H. Then there is a continuous surjective homomorphism H →* G.

theorem TauCeti.exists_surjective_and_exists_surjective_of_forall_isFiniteContinuousQuotient_iff {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsTopologicallyFinitelyGenerated G) (h : ∀ (Q : Type u) [inst : Group Q] [Finite Q], IsFiniteContinuousQuotient G Q ↔ IsFiniteContinuousQuotient H Q) : (∃ (φ : G →* H), Continuous ⇑φ ∧ Function.Surjective ⇑φ) ∧ ∃ (ψ : H →* G), Continuous ⇑ψ ∧ Function.Surjective ⇑ψ

Two epimorphisms. If G is topologically finitely generated and the profinite groups G and H have the same continuous finite quotients, then there are continuous surjections G ↠ H and H ↠ G. Finite generation of H is derived, not assumed.

theorem TauCeti.nonempty_continuousMulEquiv_of_forall_isFiniteContinuousQuotient_iff {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hG : IsTopologicallyFinitelyGenerated G) (h : ∀ (Q : Type u) [inst : Group Q] [Finite Q], IsFiniteContinuousQuotient G Q ↔ IsFiniteContinuousQuotient H Q) : Nonempty (G ≃ₜ* H)

Finite-quotient determinacy. If G is topologically finitely generated and the profinite groups G and H have the same continuous finite quotients, then G and H are topologically isomorphic. No finite-generation hypothesis is placed on H.