Td Groups

In this file we define totally disconnected locally compact Hausdorff topological groups ("td groups") and prove the equivalence between two standard definitions (Van Dantzig).

Main result

• hasCompactOpenSubgroupBasis_of_locallyCompact_t2_totallyDisconnected: Van Dantzig direction (Buzzard style).
• hasCompactOpenSubgroupBasis_iff_locallyCompact_totallyDisconnected: Van Dantzig equivalence (assuming [T2Space G]).
• hasCompactOpenSubgroupBasis_iff_locallyCompact_nonarchimedean: A variant using NonarchimedeanGroup (assuming [T2Space G]).

Definitions

• HasCompactOpenSubgroupBasis: 𝓝 1 has a basis of compact open subgroups.

Definitions

def HasCompactOpenSubgroupBasis (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

A td group in the sense of Van Dantzig: compact open subgroups form a neighborhood basis.

Equations

• HasCompactOpenSubgroupBasis G = (nhds 1).HasBasis (fun (S : OpenSubgroup G) => IsCompact ↑S) fun (S : OpenSubgroup G) => ↑S

Nonarchimedean groups from compact open subgroups

theorem nonarchimedeanGroup_of_hasCompactOpenSubgroupBasis (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (hb : (nhds 1).HasBasis (fun (S : OpenSubgroup G) => IsCompact ↑S) fun (S : OpenSubgroup G) => ↑S) : NonarchimedeanGroup G

A basis of compact open subgroups gives a nonarchimedean group.

Van Dantzig's theorem

theorem nhds_hasBasis_mulLeft (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {ι : Sort u_2} {p : ι → Prop} {s : ι → Set G} (x : G) (hb : (nhds 1).HasBasis p s) : (nhds x).HasBasis p fun (i : ι) => ⇑(Homeomorph.mulLeft x) '' s i

Transport a neighborhood basis at 1 to a neighborhood basis at x by left translation.

theorem totallyDisconnectedSpace_of_locallyCompact_t2_nonarchimedean (G : Type u_1) [Group G] [TopologicalSpace G] [LocallyCompactSpace G] [T2Space G] [NonarchimedeanGroup G] : TotallyDisconnectedSpace G

Van Dantzig direction: (td + locally compact + Hausdorff) → HasCompactOpenSubgroupBasis

We first construct compact clopen neighborhoods of 1, then find compact open subgroups inside them, and finally package this into a neighborhood basis at 1.

theorem exists_compact_clopen_nhds_one (G : Type u_1) [Group G] [TopologicalSpace G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {U : Set G} (hU : U ∈ nhds 1) : ∃ (K : Set G), IsCompact K ∧ IsClopen K ∧ 1 ∈ K ∧ K ⊆ U

In a td group, every neighborhood of 1 contains a compact clopen neighborhood of 1.

theorem exists_mem_nhds_one_mul_subset_of_isCompact_isOpen (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Set G} (hKc : IsCompact K) (hK_isOpen : IsOpen K) : ∃ V ∈ nhds 1, K * V ⊆ K

If K is compact and open, then there exists V ∈ 𝓝 1 such that K * V ⊆ K. This is a wrapper around compact_open_separated_mul_right.

theorem exists_mem_nhds_one_symm_mul_subset_of_isCompact_isOpen (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Set G} (hKc : IsCompact K) (hK_isOpen : IsOpen K) : ∃ V ∈ nhds 1, (∀ v ∈ V, v⁻¹ ∈ V) ∧ K * V ⊆ K

Strengthening of exists_mem_nhds_one_mul_subset_of_isCompact_isOpen producing a symmetric neighborhood V.

theorem exists_compactOpenSubgroup_subset_of_isCompact_isClopen (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {K : Set G} (hKc : IsCompact K) (hKcl : IsClopen K) (h1 : 1 ∈ K) : ∃ (H : OpenSubgroup G), IsCompact ↑H ∧ ↑H ⊆ K

Inside a compact clopen neighborhood of 1, there exists a compact open subgroup.

theorem exists_compactOpenSubgroup_nhds_one (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] {U : Set G} (hU : U ∈ nhds 1) : ∃ (H : OpenSubgroup G), IsCompact ↑H ∧ ↑H ⊆ U

In a td group, every neighborhood of 1 contains a compact open subgroup.

theorem hasCompactOpenSubgroupBasis_of_locallyCompact_t2_totallyDisconnected (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] [LocallyCompactSpace G] [T2Space G] : HasCompactOpenSubgroupBasis G

Van Dantzig direction (Buzzard style): assume the three properties separately.

Van Dantzig direction: HasCompactOpenSubgroupBasis → (locally compact + nonarchimedean)

theorem locallyCompactSpace_of_hasCompactOpenSubgroupBasis (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (h : HasCompactOpenSubgroupBasis G) : LocallyCompactSpace G

theorem totallyDisconnectedSpace_of_hasCompactOpenSubgroupBasis (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] (h : HasCompactOpenSubgroupBasis G) : TotallyDisconnectedSpace G

Main equivalence (Van Dantzig)

Under a Hausdorff assumption, having a basis of compact open subgroups is equivalent to being locally compact and totally disconnected.

theorem hasCompactOpenSubgroupBasis_iff_locallyCompact_totallyDisconnected (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] : HasCompactOpenSubgroupBasis G ↔ LocallyCompactSpace G ∧ TotallyDisconnectedSpace G

theorem hasCompactOpenSubgroupBasis_iff_locallyCompact_nonarchimedean (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] : HasCompactOpenSubgroupBasis G ↔ LocallyCompactSpace G ∧ NonarchimedeanGroup G