Profiniteness of the continuous automorphism group

For a topologically finitely generated profinite group G, the congruence topology makes the group ContinuousAut G of continuous automorphisms a profinite group, and the group ContinuousOut G of continuous outer automorphisms is profinite for the quotient topology.

The characteristic quotient coordinates ContinuousAut.mapQuotient embed ContinuousAut G into the product of the finite discrete groups MulAut (G ⧸ N), N ranging over the topologically characteristic open normal subgroups of G (ContinuousAut.isEmbedding_pi_mapQuotient). This file identifies the range of that embedding: it consists exactly of the families of automorphisms compatible with the quotient maps G ⧸ N → G ⧸ M for N ≤ M (ContinuousAut.range_pi_mapQuotient). A compatible family is induced by a continuous automorphism because G is the inverse limit of its characteristic open quotients, which are cofinal among all open quotients; the limit description for homomorphisms along a cofinal family (TauCeti.existsUnique_monoidHom_mk'_comp_eq_of_forall_exists_le) produces the endomorphism of G and its inverse, and its uniqueness clause shows that the two are inverse to each other. The compatibility conditions are closed in the product, so the range is closed and ContinuousAut G is compact (ContinuousAut.compactSpace). The inner automorphisms then form a closed subgroup, the image of the compact group G, and the outer automorphism group is a quotient of a profinite group by a closed normal subgroup.

Main results

• TauCeti.ContinuousAut.exists_mapQuotient_eq: every compatible family of automorphisms of the characteristic open quotients is induced by a continuous automorphism.
• TauCeti.ContinuousAut.exists_mapQuotient_eq_of_forall_exists_le: the same along any cofinal family of characteristic open normal subgroups.
• TauCeti.ContinuousAut.range_pi_mapQuotient, TauCeti.ContinuousAut.isClosedEmbedding_pi_mapQuotient: the characteristic quotient coordinates are a closed embedding onto the compatible families.
• TauCeti.ContinuousAut.compactSpace: the congruence topology on the continuous automorphisms of a topologically finitely generated profinite group is compact.
• TauCeti.ContinuousAut.isClosed_range_conj: the inner automorphisms form a closed subgroup.
• TauCeti.ContinuousOut.compactSpace, TauCeti.ContinuousOut.t2Space, TauCeti.ContinuousOut.totallyDisconnectedSpace: the continuous outer automorphism group is profinite.

References

• L. Ribes, P. Zalesskii, Profinite Groups, 2nd ed., §4.4.

theorem TauCeti.ContinuousAut.exists_mapQuotient_eq_of_forall_exists_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {ι : Type u_2} {N : ι → OpenNormalSubgroup G} (hN : ∀ (i : ι), IsTopCharacteristic G ↑(N i).toOpenSubgroup) (hcof : ∀ (U : OpenNormalSubgroup G), ∃ (i : ι), N i ≤ U) (σ : (i : ι) → MulAut (G ⧸ ↑(N i).toOpenSubgroup)) (hσ : ∀ ⦃i j : ι⦄ (hle : N i ≤ N j) (q : G ⧸ ↑(N i).toOpenSubgroup), (QuotientGroup.mapOfLE hle) ((σ i) q) = (σ j) ((QuotientGroup.mapOfLE hle) q)) : ∃ (φ : ContinuousAut G), ∀ (i : ι), (mapQuotient ⋯) φ = σ i

Let N i be a family of topologically characteristic open normal subgroups of a profinite group G, cofinal among the open normal subgroups. A family of automorphisms of the quotients G ⧸ N i that is compatible with the quotient maps G ⧸ N i → G ⧸ N j for N i ≤ N j is induced by a continuous automorphism of G.

theorem TauCeti.ContinuousAut.exists_mapQuotient_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (σ : (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }) → MulAut (G ⧸ ↑(↑N).toOpenSubgroup)) (hσ : ∀ ⦃N M : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }⦄ (hle : ↑N ≤ ↑M) (q : G ⧸ ↑(↑N).toOpenSubgroup), (QuotientGroup.mapOfLE hle) ((σ N) q) = (σ M) ((QuotientGroup.mapOfLE hle) q)) : ∃ (φ : ContinuousAut G), ∀ (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }), (mapQuotient ⋯) φ = σ N

For a topologically finitely generated profinite group G, a family of automorphisms of the characteristic open quotients G ⧸ N that is compatible with the quotient maps G ⧸ N → G ⧸ M for N ≤ M is induced by a continuous automorphism of G.

theorem TauCeti.ContinuousAut.range_pi_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : (Set.range fun (φ : ContinuousAut G) (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }) => (mapQuotient ⋯) φ) = {σ : (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }) → MulAut (G ⧸ ↑(↑N).toOpenSubgroup) | ∀ ⦃N M : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }⦄ (hle : ↑N ≤ ↑M) (q : G ⧸ ↑(↑N).toOpenSubgroup), (QuotientGroup.mapOfLE hle) ((σ N) q) = (σ M) ((QuotientGroup.mapOfLE hle) q)}

For a topologically finitely generated profinite group, the range of the joint characteristic quotient coordinate map consists exactly of the families of automorphisms compatible with the quotient maps between characteristic quotients: the continuous automorphisms of G are the compatible families of automorphisms of its characteristic open quotients.

theorem TauCeti.ContinuousAut.isClosed_range_pi_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : IsClosed (Set.range fun (φ : ContinuousAut G) (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }) => (mapQuotient ⋯) φ)

For a topologically finitely generated profinite group, the range of the joint characteristic quotient coordinate map is closed in the product of the discrete automorphism groups.

theorem TauCeti.ContinuousAut.isClosedEmbedding_pi_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : Topology.IsClosedEmbedding fun (φ : ContinuousAut G) (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }) => (mapQuotient ⋯) φ

For a topologically finitely generated profinite group, the joint characteristic quotient coordinate map is a closed embedding of ContinuousAut G into the product of the discrete automorphism groups of the characteristic open quotients.

theorem TauCeti.ContinuousAut.compactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : CompactSpace (ContinuousAut G)

For a topologically finitely generated profinite group, the congruence topology on the continuous automorphisms is compact: ContinuousAut G is a closed subspace of the product of the finite automorphism groups of the characteristic open quotients.

theorem TauCeti.ContinuousAut.isClosed_range_conj {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : IsClosed ↑conj.range

For a topologically finitely generated profinite group, the inner automorphisms form a closed subgroup of ContinuousAut G: the image of the compact group G in a Hausdorff group.

theorem TauCeti.ContinuousOut.compactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : CompactSpace (ContinuousOut G)

For a topologically finitely generated profinite group, the continuous outer automorphism group is compact for the quotient topology.

theorem TauCeti.ContinuousOut.t2Space {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : T2Space (ContinuousOut G)

For a topologically finitely generated profinite group, the continuous outer automorphism group is Hausdorff for the quotient topology: the inner automorphisms form a closed subgroup.

theorem TauCeti.ContinuousOut.totallyDisconnectedSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : TotallyDisconnectedSpace (ContinuousOut G)

For a topologically finitely generated profinite group, the continuous outer automorphism group is totally disconnected for the quotient topology; with ContinuousOut.compactSpace and ContinuousOut.t2Space, it is a profinite group.