Normed algebras #
This file contains basic facts about normed algebras.
Main results #
- We show that the character space of a normed algebra is compact using the Banach-Alaoglu theorem.
TODO #
- Show compactness for topological vector spaces; this requires the TVS version of Banach-Alaoglu.
Tags #
normed algebra, character space, continuous functional calculus
theorem
WeakDual.CharacterSpace.norm_le_norm_one
{𝕜 : Type u_1}
{A : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
[CompleteSpace A]
(φ : (characterSpace 𝕜 A).Elem)
:
LE.le (Norm.norm (DFunLike.coe toNormedDual φ.val)) (Norm.norm 1)
theorem
WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace
{𝕜 : Type u_1}
{A : Type u_2}
[NontriviallyNormedField 𝕜]
[NormedRing A]
[NormedAlgebra 𝕜 A]
[CompleteSpace A]
[ProperSpace 𝕜]
:
CompactSpace (characterSpace 𝕜 A).Elem