Topological groups

Groups carrying a compatible topology: metrizability, profinite groups and profinite completions, and functions on locally compact groups.

• Profinite completion of topological groups

TheoremBirkhoff–Kakutani metrization theorem#✓fully proved

Every Hausdorff first-countable topological group is metrizable.

theorem birkhoff_kakutani_metrization
    {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [T2Space G] [FirstCountableTopology G] :
    TopologicalSpace.MetrizableSpace G

Sources

• G. Birkhoff, Compositio Math. 3 (1936), 427-430; S. Kakutani, Proc. Imp. Acad. Tokyo 12 (1936), 4-7, DOI 10.3792/PIA/1195580206.

TheoremLocally constant compactly supported functions have uniform stabilizers#✓fully proved

A locally constant compactly supported function on a topological group is invariant under left and right multiplication by elements of some open neighborhood of 1.

theorem exists_isOpen_one_mem_forall_mul_eq_of_hasCompactSupport
    {G M : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Zero M]
    (Φ : G → M) (hlc : IsLocallyConstant Φ) (hcs : HasCompactSupport Φ) :
    ∃ W : Set G, IsOpen W ∧ (1 : G) ∈ W ∧
      ∀ g : G, ∀ w ∈ W, Φ (g * w) = Φ g ∧ Φ (w * g) = Φ g

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.