Continuous automorphisms of pro-p groups

Let G be a compact pro-p group and write Φ(G) = proPFrattini p G for its Frattini subgroup. The continuous automorphisms of G acting trivially on the Frattini quotient G ⧸ Φ(G) form the kernel of ContinuousAut.mapQuotient : ContinuousAut G →* MulAut (G ⧸ Φ(G)). This file shows that this kernel is a pro-p group for the congruence topology, and that when G is topologically finitely generated it is moreover open and of finite index. So the continuous automorphism group of a topologically finitely generated pro-p group is virtually pro-p.

The pro-p property is the finite theorem IsPGroup.isPGroup_ker_mapQuotient_frattini, passed to the limit. A neighbourhood of the identity in the congruence topology contains the automorphisms acting trivially on some finite quotient P = G ⧸ N by a topologically characteristic open normal subgroup. An automorphism acting trivially on G ⧸ Φ(G) induces on the finite p-group P an automorphism acting trivially on P ⧸ frattini P, because the image of Φ(G) in P lies in the Frattini subgroup of P. Such automorphisms of P form a p-group, so some p-power of the original automorphism acts trivially on P, and lies in the given neighbourhood.

Openness holds because Φ(G) is an open, topologically characteristic subgroup of a topologically finitely generated compact group, so the kernel is that of a coordinate of the congruence topology; the finite index holds because G ⧸ Φ(G) is then finite.

For a topologically finitely generated pro-p group the kernel is moreover the inverse limit of the finite kernels of the theorem above, taken over the topologically characteristic open normal subgroups N ≤ Φ(G). These are cofinal among the open subgroups because Φ(G) is open. For such N the Frattini subgroup of G ⧸ N is exactly the image of Φ(G), so an automorphism acts trivially on G ⧸ Φ(G) exactly when its coordinate on G ⧸ N acts trivially on the Frattini quotient of G ⧸ N. A compatible family of such coordinates is induced by a continuous automorphism, by the limit description along a cofinal family (ContinuousAut.exists_mapQuotient_eq_of_forall_exists_le).

Main results

• TauCeti.IsProP.isProP_ker_mapQuotient_proPFrattini: for a compact pro-p group, the continuous automorphisms acting trivially on the Frattini quotient form a pro-p group.
• TauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini: for a topologically finitely generated compact group, this kernel is open in the congruence topology.
• TauCeti.ContinuousAut.finiteIndex_ker_mapQuotient_proPFrattini: for a topologically finitely generated compact group, this kernel has finite index.
• TauCeti.IsProP.mapQuotient_mem_ker_mapQuotient_frattini_iff: for N ≤ Φ(G), the kernel is detected on the Frattini quotient of the finite p-group G ⧸ N.
• TauCeti.IsProP.range_pi_mapQuotient_ker_proPFrattini, TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient_ker_proPFrattini: for a topologically finitely generated pro-p group, the coordinates on the quotients G ⧸ N, N ≤ Φ(G) topologically characteristic and open, embed the kernel onto the compatible families of elements of the finite kernels.

References

• L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., §4.4 and §4.5.
• J. D. Dixon, M. P. F. du Sautoy, A. Mann, D. Segal, Analytic pro-p groups, 2nd ed., Chapter 5.

theorem TauCeti.ContinuousAut.isOpen_ker_mapQuotient_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) : IsOpen ↑(mapQuotient ⋯).ker

For a topologically finitely generated compact group, the continuous automorphisms acting trivially on the pro-p Frattini quotient form an open subgroup for the congruence topology: the pro-p Frattini subgroup is open and topologically characteristic.

theorem TauCeti.ContinuousAut.finiteIndex_ker_mapQuotient_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) : (mapQuotient ⋯).ker.FiniteIndex

For a topologically finitely generated compact group, the continuous automorphisms acting trivially on the pro-p Frattini quotient form a subgroup of finite index: the Frattini quotient is finite, and so is its automorphism group.

theorem TauCeti.IsProP.mapQuotient_mem_ker_mapQuotient_frattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) {N : OpenNormalSubgroup G} (hN : IsTopCharacteristic G ↑N.toOpenSubgroup) {φ : ContinuousAut G} (hφ : φ ∈ (ContinuousAut.mapQuotient ⋯).ker) : (ContinuousAut.mapQuotient hN) φ ∈ (MulAut.mapQuotient (frattini (G ⧸ ↑N.toOpenSubgroup))).ker

For a compact pro-p group G, a continuous automorphism acting trivially on the Frattini quotient G ⧸ proPFrattini p G induces, on each finite quotient G ⧸ N by a topologically characteristic open normal subgroup, an automorphism acting trivially on the Frattini quotient of the finite p-group G ⧸ N: the image of proPFrattini p G lies in its Frattini subgroup.

theorem TauCeti.IsProP.isProP_ker_mapQuotient_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) : IsProP p ↥(ContinuousAut.mapQuotient ⋯).ker

The continuous automorphisms of a pro-p group acting trivially on its Frattini quotient form a pro-p group. For a compact pro-p group G, the kernel of ContinuousAut G →* MulAut (G ⧸ proPFrattini p G) is pro-p for the congruence topology.

theorem TauCeti.IsProP.mapQuotient_mem_ker_mapQuotient_frattini_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) {N : OpenNormalSubgroup G} (hN : IsTopCharacteristic G ↑N.toOpenSubgroup) (hle : ↑N.toOpenSubgroup ≤ proPFrattini p G) {φ : ContinuousAut G} : (ContinuousAut.mapQuotient hN) φ ∈ (MulAut.mapQuotient (frattini (G ⧸ ↑N.toOpenSubgroup))).ker ↔ φ ∈ (ContinuousAut.mapQuotient ⋯).ker

For a compact pro-p group G and a topologically characteristic open normal subgroup N ≤ proPFrattini p G, a continuous automorphism acts trivially on the Frattini quotient of G exactly when it induces on the finite p-group G ⧸ N an automorphism acting trivially on the Frattini quotient of G ⧸ N: the Frattini subgroup of G ⧸ N is the image of proPFrattini p G.

theorem TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient_ker_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (p : ℕ) : Topology.IsEmbedding fun (φ : ↥(mapQuotient ⋯).ker) (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ proPFrattini p G }) => (mapQuotient ⋯) ↑φ

For a topologically finitely generated profinite group G, the coordinates on the quotients G ⧸ N by the topologically characteristic open normal subgroups N ≤ proPFrattini p G embed the kernel of ContinuousAut G →* MulAut (G ⧸ proPFrattini p G) into the product of the discrete automorphism groups of these finite quotients.

theorem TauCeti.IsProP.range_pi_mapQuotient_ker_proPFrattini {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) (hfg : IsTopologicallyFinitelyGenerated G) : (Set.range fun (φ : ↥(ContinuousAut.mapQuotient ⋯).ker) (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ proPFrattini p G }) => (ContinuousAut.mapQuotient ⋯) ↑φ) = {σ : (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ proPFrattini p G }) → MulAut (G ⧸ ↑(↑N).toOpenSubgroup) | (∀ (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ proPFrattini p G }), σ N ∈ (MulAut.mapQuotient (frattini (G ⧸ ↑(↑N).toOpenSubgroup))).ker) ∧ ∀ ⦃N M : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ proPFrattini p G }⦄ (hle : ↑N ≤ ↑M) (q : G ⧸ ↑(↑N).toOpenSubgroup), (QuotientGroup.mapOfLE hle) ((σ N) q) = (σ M) ((QuotientGroup.mapOfLE hle) q)}

The kernel on the Frattini quotient is the inverse limit of the finite kernels. For a topologically finitely generated pro-p group G, the coordinates on the quotients G ⧸ N by the topologically characteristic open normal subgroups N ≤ proPFrattini p G identify the kernel of ContinuousAut G →* MulAut (G ⧸ proPFrattini p G) with the families of automorphisms σ N of the finite p-groups G ⧸ N that act trivially on the Frattini quotients of G ⧸ N and are compatible with the quotient maps G ⧸ N → G ⧸ M for N ≤ M. The coordinate map is injective and a topological embedding by ContinuousAut.isEmbedding_pi_mapQuotient_ker_proPFrattini.