The units of a real normed algebra have no small subgroups

Let A be a real normed algebra, such as ℝ, ℂ, or an algebra of bounded operators. An element z ≠ 1 of A has a power at distance more than 1 / 2 from 1: as long as w stays within 1 / 2 of 1, the identity w² - 1 = 2 • (w - 1) + (w - 1)² shows that squaring multiplies the distance to 1 by at least 3 / 2. Hence the only subgroup of Aˣ inside the closed ball of radius 1 / 2 around 1 is trivial. For the unit circle alone, Mathlib's Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two is the analogous statement; the version here applies to characters with values in ℂˣ that need not be unitary.

For a continuous homomorphism f from a topological group G to Aˣ, the preimage of that ball is a neighbourhood of 1, and every subgroup of G inside it lies in the kernel of f. This is how a continuous character of a group with arbitrarily small open subgroups, such as the units of a nonarchimedean local field, is seen to be trivial on one of them.

Main results

• TauCeti.three_div_two_mul_norm_sub_one_le_norm_sq_sub_one: if ‖w - 1‖ ≤ 1 / 2, then squaring multiplies the distance to 1 by at least 3 / 2.
• TauCeti.eq_one_of_forall_norm_pow_sub_one_le: an element all of whose powers lie within 1 / 2 of 1 is 1.
• ContinuousMonoidHom.exists_mem_nhds_one_forall_le_ker: a continuous homomorphism into Aˣ is trivial on every subgroup contained in a suitable neighbourhood of 1.

theorem TauCeti.three_div_two_mul_norm_sub_one_le_norm_sq_sub_one {A : Type u_1} [SeminormedRing A] [NormedAlgebra ℝ A] {w : A} (hw : ‖w - 1‖ ≤ 1 / 2) : 3 / 2 * ‖w - 1‖ ≤ ‖w ^ 2 - 1‖

Squaring pushes an element near 1 away from 1. If ‖w - 1‖ ≤ 1 / 2, then ‖w ^ 2 - 1‖ ≥ 3 / 2 * ‖w - 1‖. This holds even in a real seminormed algebra.

theorem TauCeti.eq_one_of_forall_norm_pow_sub_one_le {A : Type u_1} [NormedRing A] [NormedAlgebra ℝ A] {z : A} (h : ∀ (n : ℕ), ‖z ^ n - 1‖ ≤ 1 / 2) : z = 1

No small subgroups. An element of a real normed algebra all of whose powers lie within 1 / 2 of 1 is 1 itself.

theorem ContinuousMonoidHom.exists_mem_nhds_one_forall_le_ker {G : Type u_1} {A : Type u_2} [Group G] [TopologicalSpace G] [NormedRing A] [NormedAlgebra ℝ A] (f : G →ₜ* Aˣ) : ∃ N ∈ nhds 1, ∀ (H : Subgroup G), ↑H ⊆ N → H ≤ f.ker

A continuous homomorphism into Aˣ kills every small subgroup. For a continuous homomorphism f from a topological group to the units of a real normed algebra, there is a neighbourhood N of 1 such that every subgroup contained in N lies in the kernel of f.