Topologically finitely generated profinite groups are Hopfian

A group is Hopfian when every surjective endomorphism of it is injective. A profinite group that is topologically finitely generated is Hopfian in the continuous sense: a continuous surjective f : G →* G is automatically a topological automorphism.

The proof is a counting argument on the open subgroups. Pulling back along a continuous surjection preserves the index of a subgroup and is injective, so it restricts to an injective self-map of the open subgroups of any fixed index; finite generation makes each of those sets finite (TauCeti.IsTopologicallyFinitelyGenerated.finite_openSubgroup_index_eq), so the restriction is a bijection and every open subgroup of G is a preimage f ⁻¹' V. Any such preimage contains ker f, and in a profinite group the open subgroups intersect in the trivial subgroup, so ker f is trivial. A continuous bijection of compact Hausdorff groups is a topological isomorphism, which upgrades injectivity to TauCeti.IsTopologicallyFinitelyGenerated.continuousMulEquivOfSurjective.

Sharpness

Finite generation cannot be dropped: on G = ∏_{i : ℕ} F with F a nontrivial finite group the shift (x₀, x₁, …) ↦ (x₁, x₂, …) is a continuous surjective endomorphism with nontrivial kernel.

There is no co-Hopfian counterpart: the converse implication, that a continuous injective endomorphism is surjective, is false even for G = ℤ_p, where multiplication by p is injective and not surjective.

Main results

• TauCeti.IsTopologicallyFinitelyGenerated.ker_eq_bot_of_surjective: a continuous surjective endomorphism of a topologically finitely generated profinite group has trivial kernel.
• TauCeti.IsTopologicallyFinitelyGenerated.injective_of_surjective: such an endomorphism is injective (the Hopf property).
• TauCeti.IsTopologicallyFinitelyGenerated.bijective_of_surjective: such an endomorphism is bijective.
• TauCeti.IsTopologicallyFinitelyGenerated.bijective_of_surjective_of_surjective: a continuous surjection out of such a group that admits a continuous surjection back is bijective.
• TauCeti.IsTopologicallyFinitelyGenerated.continuousMulEquivOfSurjective: it is a topological automorphism.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Proposition 2.5.2.

theorem TauCeti.IsTopologicallyFinitelyGenerated.ker_eq_bot_of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {f : G →* G} (hG : IsTopologicallyFinitelyGenerated G) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : f.ker = ⊥

A continuous surjective endomorphism of a topologically finitely generated profinite group has trivial kernel.

theorem TauCeti.IsTopologicallyFinitelyGenerated.injective_of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {f : G →* G} (hG : IsTopologicallyFinitelyGenerated G) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Injective ⇑f

Topologically finitely generated profinite groups are Hopfian. A continuous surjective endomorphism of such a group is injective.

theorem TauCeti.IsTopologicallyFinitelyGenerated.bijective_of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {f : G →* G} (hG : IsTopologicallyFinitelyGenerated G) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Bijective ⇑f

A continuous surjective endomorphism of a topologically finitely generated profinite group is bijective.

theorem TauCeti.IsTopologicallyFinitelyGenerated.bijective_of_surjective_of_surjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type u_2} [Group H] [TopologicalSpace H] (hG : IsTopologicallyFinitelyGenerated G) {φ : G →* H} {ψ : H →* G} (hφ : Continuous ⇑φ) (hφs : Function.Surjective ⇑φ) (hψ : Continuous ⇑ψ) (hψs : Function.Surjective ⇑ψ) : Function.Bijective ⇑φ

Continuous surjections in both directions are bijective. If G is a topologically finitely generated profinite group and φ : G →* H, ψ : H →* G are continuous surjections, then φ is bijective.

noncomputable def TauCeti.IsTopologicallyFinitelyGenerated.continuousMulEquivOfSurjective {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {f : G →* G} (hG : IsTopologicallyFinitelyGenerated G) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : G ≃ₜ* G

A continuous surjective endomorphism of a topologically finitely generated profinite group, packaged as a topological automorphism.

Equations

• hG.continuousMulEquivOfSurjective hf hsurj = { toMulEquiv := MulEquiv.ofBijective f ⋯, continuous_toFun := hf, continuous_invFun := ⋯ }

@[simp]

theorem TauCeti.IsTopologicallyFinitelyGenerated.continuousMulEquivOfSurjective_apply {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {f : G →* G} (hG : IsTopologicallyFinitelyGenerated G) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) (x : G) : (hG.continuousMulEquivOfSurjective hf hsurj) x = f x

The topological automorphism attached to a continuous surjective endomorphism is that endomorphism.