Bases of the Frattini quotient and topological generation

Burnside's topological generation criterion says that a set generates a profinite pro-p group topologically exactly when its image spans a dense subspace of the Frattini quotient over 𝔽_p. When the quotient is finite, this is equivalent to algebraic spanning. Any basis of the Frattini quotient lifts to topological generators, even when the quotient is infinite.

Dually, when the group is topologically finitely generated, a family whose classes in the Frattini quotient are linearly independent is separated by continuous characters: for any prescribed values in an 𝔽_p-module A carrying an arbitrary topology, there is a continuous homomorphism into A taking them (TauCeti.IsTopologicallyFinitelyGenerated.exists_continuousMonoidHom_apply_eq). Topological finite generation cannot be dropped: for an infinite linearly independent family the statement fails, since a continuous homomorphism into a discrete A is eventually trivial along a family converging to the identity.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8 (Burnside's basis theorem).

theorem TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_topologicalClosure_eq_top {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) (s : Set G) : (Subgroup.closure s).topologicalClosure = ⊤ ↔ (Submodule.span (ZMod p) ((fun (g : G) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) g)) '' s)).toAddSubgroup.topologicalClosure = ⊤

Burnside's basis theorem, dense spanning form. A set topologically generates a profinite pro-p group exactly when the span of its image in the Frattini quotient is dense.

theorem TauCeti.topologicallyGenerates_iff_frattiniQuotient_span_eq_top {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Finite (G ⧸ proPFrattini p G)] (hG : IsProP p G) (s : Set G) : (Subgroup.closure s).topologicalClosure = ⊤ ↔ Submodule.span (ZMod p) ((fun (g : G) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) g)) '' s) = ⊤

Burnside's basis theorem, spanning form. If the Frattini quotient is finite, a set topologically generates a profinite pro-p group exactly when its images span that quotient over 𝔽_p.

theorem TauCeti.topologicallyGenerates_of_basis_frattiniQuotient {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {ι : Type u_2} (b : Module.Basis ι (ZMod p) (Additive (G ⧸ proPFrattini p G))) (g : ι → G) (hg : ∀ (i : ι), Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g i)) = b i) : (Subgroup.closure (Set.range g)).topologicalClosure = ⊤

Any chosen lifts of a basis of the Frattini quotient topologically generate the profinite pro-p group.

theorem TauCeti.exists_lift_basis_frattiniQuotient_topologicallyGenerates {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsProP p G) {ι : Type u_2} (b : Module.Basis ι (ZMod p) (Additive (G ⧸ proPFrattini p G))) : ∃ (g : ι → G), (∀ (i : ι), Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g i)) = b i) ∧ (Subgroup.closure (Set.range g)).topologicalClosure = ⊤

Every basis of the Frattini quotient has a lift to a topological generating family.

theorem TauCeti.IsTopologicallyFinitelyGenerated.exists_continuousMonoidHom_apply_eq {p : ℕ} [Fact (Nat.Prime p)] {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hfg : IsTopologicallyFinitelyGenerated G) {ι : Type u_2} {g : ι → G} (hg : LinearIndependent (ZMod p) fun (k : ι) => Additive.ofMul ((QuotientGroup.mk' (proPFrattini p G)) (g k))) {A : Type u_3} [AddCommGroup A] [Module (ZMod p) A] [TopologicalSpace A] (a : ι → A) : ∃ (ψ : G →ₜ* Multiplicative A), ∀ (k : ι), ψ (g k) = Multiplicative.ofAdd (a k)

Continuous 𝔽_p-characters with prescribed values. In a topologically finitely generated compact group, a family g whose classes in the pro-p Frattini quotient are linearly independent over 𝔽_p takes any prescribed values a k under some continuous homomorphism into A, written multiplicatively. Here A is an 𝔽_p-module with an arbitrary topology: no compatibility between its topology and its module structure is assumed.