Continuous homomorphisms from a compact group into the units of a normed division ring #
A continuous homomorphism f from a compact group into the units of a normed division ring takes
values of norm 1: the norms ‖f (g ^ n)‖ = ‖f g‖ ^ n stay bounded for all n : ℤ, which forces
‖f g‖ = 1. For 𝕜 = ℂ this says that a continuous character of a compact group is unitary.
theorem
ContinuousMonoidHom.norm_apply_eq_one_of_compactSpace
{G : Type u_1}
{𝕜 : Type u_2}
[Group G]
[TopologicalSpace G]
[CompactSpace G]
[NormedDivisionRing 𝕜]
(f : G →ₜ* 𝕜ˣ)
(g : G)
:
A continuous homomorphism from a compact group into the units of a normed division ring takes
values of norm 1.