Topologically characteristic subgroups

A subgroup of a topological group is topologically characteristic if every continuous automorphism preserves it. This is weaker than Mathlib's Subgroup.Characteristic, which tests all abstract automorphisms. The distinction matters for profinite groups, whose abstract automorphisms need not be continuous.

The predicate TauCeti.IsTopCharacteristic G N is expressed by the image equation N.map φ = N. Its equivalent image and preimage inclusion criteria make it convenient to prove, and it is stable under arbitrary suprema and infima. A topologically characteristic subgroup is normal as soon as inner automorphisms are continuous, and so is a topologically characteristic subgroup of a normal subgroup.

In a topologically finitely generated compact group the topologically characteristic open normal subgroups are cofinal among the open subgroups: an open subgroup has finite index, there are finitely many open subgroups of that index, and their intersection is preserved by every continuous automorphism. When the group is moreover totally disconnected, these subgroups form a neighbourhood basis of the identity. This is what makes the congruence topology on ContinuousAut G behave well for a topologically finitely generated profinite group G.

The characterizations and lattice API parallel Mathlib's API for Subgroup.Characteristic in Mathlib.Algebra.Group.Subgroup.Basic.

Main definitions

• TauCeti.IsTopCharacteristic: invariance of a subgroup under every continuous automorphism.

Main results

• Subgroup.Characteristic.isTopCharacteristic: every abstractly characteristic subgroup is topologically characteristic.
• TauCeti.IsTopCharacteristic.normal: a topologically characteristic subgroup is normal when inner automorphisms are continuous.
• TauCeti.IsTopCharacteristic.map_subtype_normal: a topologically characteristic subgroup of a normal subgroup is normal in the ambient group.
• TauCeti.IsTopologicallyFinitelyGenerated.exists_isTopCharacteristic_le: in a topologically finitely generated compact group, every open subgroup contains a topologically characteristic open normal subgroup.
• TauCeti.IsTopologicallyFinitelyGenerated.exists_isTopCharacteristic_subset: in a topologically finitely generated profinite group, every neighbourhood of the identity contains a topologically characteristic open normal subgroup.

References

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

def TauCeti.IsTopCharacteristic (G : Type u) [Group G] [TopologicalSpace G] (N : Subgroup G) : Prop

A subgroup is topologically characteristic if every continuous automorphism maps it onto itself. This is weaker than Subgroup.Characteristic, which quantifies over all abstract automorphisms.

Equations

• TauCeti.IsTopCharacteristic G N = ∀ (φ : TauCeti.ContinuousAut G), Subgroup.map φ.toMonoidHom N = N

theorem TauCeti.isTopCharacteristic_iff_map_eq {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), Subgroup.map φ.toMonoidHom N = N

A subgroup is topologically characteristic exactly when every continuous automorphism maps it onto itself.

theorem TauCeti.isTopCharacteristic_iff_comap_eq {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), Subgroup.comap φ.toMonoidHom N = N

A subgroup is topologically characteristic exactly when it is the preimage of itself under every continuous automorphism.

theorem TauCeti.isTopCharacteristic_iff_comap_le {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), Subgroup.comap φ.toMonoidHom N ≤ N

To prove that a subgroup is topologically characteristic, it suffices to prove that its preimage under every continuous automorphism is contained in it.

theorem TauCeti.isTopCharacteristic_iff_le_comap {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), N ≤ Subgroup.comap φ.toMonoidHom N

To prove that a subgroup is topologically characteristic, it suffices to prove that it is contained in its preimage under every continuous automorphism.

theorem TauCeti.isTopCharacteristic_iff_map_le {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), Subgroup.map φ.toMonoidHom N ≤ N

To prove that a subgroup is topologically characteristic, it suffices to prove that every continuous automorphism maps it into itself.

theorem TauCeti.isTopCharacteristic_iff_le_map {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} : IsTopCharacteristic G N ↔ ∀ (φ : ContinuousAut G), N ≤ Subgroup.map φ.toMonoidHom N

To prove that a subgroup is topologically characteristic, it suffices to prove that the image under every continuous automorphism contains it.

theorem Subgroup.Characteristic.isTopCharacteristic {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} (hN : N.Characteristic) : TauCeti.IsTopCharacteristic G N

Every abstractly characteristic subgroup is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.bot {G : Type u} [Group G] [TopologicalSpace G] : IsTopCharacteristic G ⊥

The trivial subgroup is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.top {G : Type u} [Group G] [TopologicalSpace G] : IsTopCharacteristic G ⊤

The whole group is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.sup {G : Type u} [Group G] [TopologicalSpace G] {N K : Subgroup G} (hN : IsTopCharacteristic G N) (hK : IsTopCharacteristic G K) : IsTopCharacteristic G (N ⊔ K)

The supremum of two topologically characteristic subgroups is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.iSup {G : Type u} [Group G] [TopologicalSpace G] {ι : Sort u_1} {N : ι → Subgroup G} (hN : ∀ (i : ι), IsTopCharacteristic G (N i)) : IsTopCharacteristic G (⨆ (i : ι), N i)

An arbitrary supremum of topologically characteristic subgroups is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.inf {G : Type u} [Group G] [TopologicalSpace G] {N K : Subgroup G} (hN : IsTopCharacteristic G N) (hK : IsTopCharacteristic G K) : IsTopCharacteristic G (N ⊓ K)

The infimum of two topologically characteristic subgroups is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.iInf {G : Type u} [Group G] [TopologicalSpace G] {ι : Sort u_1} {N : ι → Subgroup G} (hN : ∀ (i : ι), IsTopCharacteristic G (N i)) : IsTopCharacteristic G (⨅ (i : ι), N i)

An arbitrary infimum of topologically characteristic subgroups is topologically characteristic.

theorem TauCeti.IsTopCharacteristic.normal {G : Type u} [Group G] [TopologicalSpace G] {N : Subgroup G} [SeparatelyContinuousMul G] (hN : IsTopCharacteristic G N) : N.Normal

A topologically characteristic subgroup is normal when inner automorphisms are continuous.

theorem TauCeti.IsTopCharacteristic.map_subtype_normal {G : Type u} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] {H : Subgroup G} [H.Normal] {K : Subgroup ↥H} (hK : IsTopCharacteristic (↥H) K) : (Subgroup.map H.subtype K).Normal

A topologically characteristic subgroup of a normal subgroup is normal in the ambient group when inner automorphisms are continuous. This is the topological analogue of Subgroup.normal_of_characteristic_of_normal.

theorem TauCeti.IsTopologicallyFinitelyGenerated.exists_isTopCharacteristic_le {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (hG : IsTopologicallyFinitelyGenerated G) (U : OpenSubgroup G) : ∃ (N : OpenNormalSubgroup G), IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N.toOpenSubgroup ≤ ↑U

In a topologically finitely generated compact group, every open subgroup U contains a topologically characteristic open normal subgroup: the intersection of the finitely many open subgroups of the same index as U.

theorem TauCeti.IsTopologicallyFinitelyGenerated.exists_isTopCharacteristic_subset {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) {U : Set G} (hU : IsOpen U) (h1 : 1 ∈ U) : ∃ (N : OpenNormalSubgroup G), IsTopCharacteristic G ↑N.toOpenSubgroup ∧ ↑N ⊆ U

In a topologically finitely generated profinite group, every open neighbourhood of the identity contains a topologically characteristic open normal subgroup.

theorem TauCeti.IsTopologicallyFinitelyGenerated.iInf_isTopCharacteristic_eq_bot {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (hG : IsTopologicallyFinitelyGenerated G) : ⨅ (N : { N : OpenNormalSubgroup G // IsTopCharacteristic G ↑N.toOpenSubgroup }), ↑(↑N).toOpenSubgroup = ⊥

In a topologically finitely generated profinite group, the topologically characteristic open normal subgroups intersect in the trivial subgroup.