Profinite groups are nonarchimedean

A topological group is nonarchimedean when every neighbourhood of the identity contains an open subgroup. In a compact totally disconnected topological group every open neighbourhood of the identity contains an open normal subgroup, which is Mathlib's ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one; this file records the consequence as the NonarchimedeanGroup instance, so that everything Mathlib and Tau Ceti prove about nonarchimedean groups — the basis of open subgroups at the identity, the transport to quotients and subgroups, total separatedness of Hausdorff nonarchimedean groups — applies to profinite groups and to compact totally disconnected topological modules without further argument.

Main results

• TauCeti.IsTopologicalGroup.nonarchimedeanGroup_of_compactSpace, and its additive form TauCeti.IsTopologicalAddGroup.nonarchimedeanAddGroup_of_compactSpace: a compact totally disconnected topological group is nonarchimedean.

@[instance 100]

instance TauCeti.IsTopologicalGroup.nonarchimedeanGroup_of_compactSpace {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : NonarchimedeanGroup G

A compact totally disconnected topological group is nonarchimedean: every neighbourhood of the identity contains an open subgroup.

@[instance 100]

instance TauCeti.IsTopologicalAddGroup.nonarchimedeanAddGroup_of_compactSpace {G : Type u_1} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : NonarchimedeanAddGroup G

A compact totally disconnected topological additive group is nonarchimedean: every neighbourhood of zero contains an open additive subgroup.