Surjectivity detected by the Frattini quotient

A homomorphism into a profinite pro-p group has dense range exactly when its composites with all index-p quotient maps are surjective. Equivalently, its composite with the Frattini quotient map has dense range. For continuous homomorphisms from compact groups, the images are closed, so these criteria detect surjectivity itself.

These are the homomorphism forms of Burnside's basis theorem: they check surjectivity of a map given on generators by checking its values modulo the Frattini subgroup. The source need not be pro-p, and the density criteria need no topology on the source.

The same reduction shows that a topological generating family stays one when each member is replaced by a conjugate of a p-adic power of it by a unit (IsProP.topologicalClosure_closure_range_eq_top_of_isConj_padicPow): modulo the Frattini subgroup conjugation is trivial, and a unit power generates the same closed subgroup as its base. This is what makes a continuous endomorphism of a free pro-p group of finite rank that sends each generator to a conjugate of a unit power of itself an automorphism.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.

theorem TauCeti.IsProP.denseRange_iff_surjective_quotient_index_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsProP p H) (f : G →* H) : DenseRange ⇑f ↔ ∀ (U : OpenNormalSubgroup H), (↑U.toOpenSubgroup).index = p → Function.Surjective ⇑((QuotientGroup.mk' ↑U.toOpenSubgroup).comp f)

A homomorphism into a profinite pro-p group has dense range exactly when it surjects onto every quotient of index p. No topology or continuity on the source is needed.

theorem TauCeti.IsProP.denseRange_iff_denseRange_frattiniQuotient {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsProP p H) (f : G →* H) : DenseRange ⇑f ↔ DenseRange ⇑((QuotientGroup.mk' (proPFrattini p H)).comp f)

A homomorphism into a profinite pro-p group has dense range exactly when its composite with the Frattini quotient map has dense range.

theorem TauCeti.IsProP.surjective_iff_surjective_quotient_index_eq {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] [TopologicalSpace G] [CompactSpace G] (hH : IsProP p H) (f : G →* H) (hf : Continuous ⇑f) : Function.Surjective ⇑f ↔ ∀ (U : OpenNormalSubgroup H), (↑U.toOpenSubgroup).index = p → Function.Surjective ⇑((QuotientGroup.mk' ↑U.toOpenSubgroup).comp f)

Burnside's surjectivity criterion. A continuous homomorphism from a compact group to a profinite pro-p group is surjective exactly when its composites with all index-p quotient maps are surjective.

theorem TauCeti.IsProP.surjective_iff_surjective_frattiniQuotient {p : ℕ} [hp : Fact (Nat.Prime p)] {G : Type u_1} [Group G] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] [TopologicalSpace G] [CompactSpace G] (hH : IsProP p H) (f : G →* H) (hf : Continuous ⇑f) : Function.Surjective ⇑f ↔ Function.Surjective ⇑((QuotientGroup.mk' (proPFrattini p H)).comp f)

A continuous homomorphism from a compact group to a profinite pro-p group is surjective exactly when its composite with the Frattini quotient map is surjective.

theorem TauCeti.IsProP.topologicalClosure_closure_range_eq_top_of_isConj_padicPow {p : ℕ} [hp : Fact (Nat.Prime p)] {H : Type u_2} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (hH : IsProP p H) {ι : Type u_3} {x y : ι → H} (hx : (Subgroup.closure (Set.range x)).topologicalClosure = ⊤) (u : ι → ℤ_[p]ˣ) (h : ∀ (i : ι), IsConj (hH.padicPow (x i) ↑(u i)) (y i)) : (Subgroup.closure (Set.range y)).topologicalClosure = ⊤

Conjugates of unit powers of topological generators generate. If x topologically generates a profinite pro-p group H and each y i is conjugate to the p-adic power of x i by a unit u i, then y topologically generates H.