The congruence topology on continuous automorphisms

The group ContinuousAut G of continuous automorphisms of a topological group G carries the congruence topology: the coarsest topology for which every coordinate ContinuousAut.mapQuotient : ContinuousAut G →* MulAut (G ⧸ N), for N a topologically characteristic open normal subgroup of G, is continuous into the discrete group MulAut (G ⧸ N). Two automorphisms are close when they agree modulo a small characteristic open normal subgroup. With this topology ContinuousAut G is a topological group and the inner automorphism map ContinuousAut.conj : G → ContinuousAut G is continuous.

The topology is well behaved for a topologically finitely generated profinite group G, where the topologically characteristic open normal subgroups form a neighbourhood basis of the identity (TauCeti.IsTopologicallyFinitelyGenerated.exists_isTopCharacteristic_subset). Then the evaluation ContinuousAut G × G → G is jointly continuous, the coordinates separate automorphisms, so ContinuousAut G is Hausdorff and totally disconnected, and the conditions φ x = y and IsConj (φ x) y on an automorphism φ define closed sets. The last is the form in which closed-graph arguments impose conjugacy conditions on an automorphism.

Without finite generation the congruence topology need not be compact, and without compactness of G it can be indiscrete (Multiplicative ℝ has no proper open subgroup) or infinite and discrete (Multiplicative (ℤ × ℤ) has the open characteristic subgroup ⊥, and ContinuousAut (Multiplicative (ℤ × ℤ)) ≅ GL₂(ℤ)).

Main definitions

• TauCeti.ContinuousAut.congruenceTopology: the congruence topology on ContinuousAut G, as an instance.

Main results

• TauCeti.ContinuousAut.continuous_mapQuotient: each characteristic quotient coordinate is continuous into the discrete automorphism group of the quotient.
• TauCeti.ContinuousAut.hasBasis_nhds, TauCeti.ContinuousAut.mem_nhds_iff: the neighbourhoods of φ are generated by the sets of automorphisms agreeing with φ modulo a topologically characteristic open normal subgroup.
• TauCeti.ContinuousAut.continuous_conj: the inner automorphism map is continuous.
• TauCeti.ContinuousAut.continuous_eval: for a topologically finitely generated profinite group, evaluation ContinuousAut G × G → G is continuous.
• TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient, TauCeti.ContinuousAut.t2Space, TauCeti.ContinuousAut.totallyDisconnectedSpace: for a topologically finitely generated profinite group, the coordinates embed ContinuousAut G into a product of discrete groups, so the congruence topology is Hausdorff and totally disconnected.
• TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient_of_forall_exists_le: the coordinates along any cofinal family of characteristic open normal subgroups already give such an embedding.
• TauCeti.ContinuousAut.isClosed_setOf_apply_eq, TauCeti.ContinuousAut.isClosed_isConj: the automorphisms with a prescribed value, or a prescribed conjugacy class of a value, at a point form a closed set.

References

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

@[instance_reducible]

instance TauCeti.ContinuousAut.congruenceTopology {G : Type u_1} [Group G] [TopologicalSpace G] : TopologicalSpace (ContinuousAut G)

The congruence topology on the continuous automorphisms of G: the coarsest topology for which every coordinate mapQuotient : ContinuousAut G →* MulAut (G ⧸ N), N ranging over the topologically characteristic open normal subgroups of G, is continuous into the discrete group MulAut (G ⧸ N).

theorem TauCeti.ContinuousAut.congruenceTopology_eq_iInf {G : Type u_1} [Group G] [TopologicalSpace G] : congruenceTopology = ⨅ (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }), TopologicalSpace.induced ⇑(mapQuotient ⋯) ⊥

The congruence topology is the infimum of the topologies induced by the characteristic quotient coordinates from the discrete topology ⊥.

instance TauCeti.ContinuousAut.instIsTopologicalGroup {G : Type u_1} [Group G] [TopologicalSpace G] : IsTopologicalGroup (ContinuousAut G)

The congruence topology makes ContinuousAut G a topological group, as an infimum of topologies induced along homomorphisms into discrete groups.

theorem TauCeti.ContinuousAut.continuous_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) (hN : IsTopCharacteristic G ↑N.toOpenSubgroup) : Continuous ⇑(mapQuotient hN)

Each characteristic quotient coordinate is continuous for the congruence topology and the discrete topology ⊥ on MulAut (G ⧸ N).

theorem TauCeti.ContinuousAut.continuous_iff_forall_continuous_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] {X : Type u_2} [TopologicalSpace X] {f : X → ContinuousAut G} : Continuous f ↔ ∀ (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }), Continuous (⇑(mapQuotient ⋯) ∘ f)

A map into ContinuousAut G is continuous exactly when all of its characteristic quotient coordinates are continuous into the corresponding discrete automorphism groups.

theorem TauCeti.ContinuousAut.isOpen_ker_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) (hN : IsTopCharacteristic G ↑N.toOpenSubgroup) : IsOpen ↑(mapQuotient hN).ker

The kernel of a characteristic quotient coordinate is open in the congruence topology.

theorem TauCeti.ContinuousAut.isOpen_setOf_mapQuotient_eq {G : Type u_1} [Group G] [TopologicalSpace G] (N : OpenNormalSubgroup G) (hN : IsTopCharacteristic G ↑N.toOpenSubgroup) (φ : ContinuousAut G) : IsOpen {ψ : ContinuousAut G | (mapQuotient hN) ψ = (mapQuotient hN) φ}

The automorphisms sharing a characteristic quotient coordinate with φ form an open set.

theorem TauCeti.ContinuousAut.hasBasis_nhds {G : Type u_1} [Group G] [TopologicalSpace G] (φ : ContinuousAut G) : (nhds φ).HasBasis (fun (N : OpenNormalSubgroup G) => IsTopCharacteristic G ↑N.toOpenSubgroup) fun (N : OpenNormalSubgroup G) => {ψ : ContinuousAut G | ∀ (x : G), ↑(ψ x) = ↑(φ x)}

The neighbourhoods of φ in the congruence topology are generated by the sets of automorphisms agreeing with φ modulo a topologically characteristic open normal subgroup.

theorem TauCeti.ContinuousAut.mem_nhds_iff {G : Type u_1} [Group G] [TopologicalSpace G] {φ : ContinuousAut G} {s : Set (ContinuousAut G)} : s ∈ nhds φ ↔ ∃ (N : OpenNormalSubgroup G), IsTopCharacteristic G ↑N.toOpenSubgroup ∧ {ψ : ContinuousAut G | ∀ (x : G), ↑(ψ x) = ↑(φ x)} ⊆ s

A set is a neighbourhood of φ in the congruence topology exactly when it contains every automorphism agreeing with φ modulo some topologically characteristic open normal subgroup.

theorem TauCeti.ContinuousAut.continuous_conj {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] : Continuous ⇑conj

The inner automorphism map G → ContinuousAut G is continuous for the congruence topology: on each characteristic open quotient it factors through the discrete group G ⧸ N.

theorem TauCeti.ContinuousAut.continuous_eval {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : Continuous fun (p : ContinuousAut G × G) => p.1 p.2

For a topologically finitely generated profinite group, the evaluation (φ, x) ↦ φ x is jointly continuous on ContinuousAut G × G.

theorem TauCeti.ContinuousAut.continuous_eval_const {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (x : G) : Continuous fun (φ : ContinuousAut G) => φ x

For a topologically finitely generated profinite group, evaluation at a point is continuous on ContinuousAut G.

theorem TauCeti.ContinuousAut.eq_of_forall_mapQuotient_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) {φ ψ : ContinuousAut G} (h : ∀ (N : OpenNormalSubgroup G) (hN : IsTopCharacteristic G ↑N.toOpenSubgroup), (mapQuotient hN) φ = (mapQuotient hN) ψ) : φ = ψ

For a topologically finitely generated profinite group, the characteristic quotient coordinates separate continuous automorphisms.

theorem TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : Topology.IsEmbedding 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 topological embedding of ContinuousAut G into the product of the discrete automorphism groups of the characteristic open quotients.

theorem TauCeti.ContinuousAut.isEmbedding_pi_mapQuotient_of_forall_exists_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) {ι : Type u_2} {N : ι → OpenNormalSubgroup G} (hN : ∀ (i : ι), IsTopCharacteristic G ↑(N i).toOpenSubgroup) (hcof : ∀ (M : OpenNormalSubgroup G), IsTopCharacteristic G ↑M.toOpenSubgroup → ∃ (i : ι), N i ≤ M) : Topology.IsEmbedding fun (φ : ContinuousAut G) (i : ι) => (mapQuotient ⋯) φ

For a topologically finitely generated profinite group, the characteristic quotient coordinates along any family N i of topologically characteristic open normal subgroups that is cofinal among them already embed ContinuousAut G into the product of the discrete automorphism groups: each other coordinate factors through one of the family.

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

For a topologically finitely generated profinite group, the congruence topology is Hausdorff.

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

For a topologically finitely generated profinite group, the congruence topology is totally disconnected.

theorem TauCeti.ContinuousAut.isClosed_setOf_apply_eq {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (x y : G) : IsClosed {φ : ContinuousAut G | φ x = y}

For a topologically finitely generated profinite group, the automorphisms taking a prescribed value at a point form a closed set.

theorem TauCeti.ContinuousAut.isClosed_isConj {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) (x y : G) : IsClosed {φ : ContinuousAut G | IsConj (φ x) y}

For a topologically finitely generated profinite group, the automorphisms carrying x into the conjugacy class of y form a closed set.