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

@[instance_reducible]

instance IntermediateField.instNontriviallyNormedFieldSubtypeMem {K : Type u_1} {L : Type u_2} [NontriviallyNormedField K] [NormedField L] [NormedAlgebra K L] (F : IntermediateField K L) : NontriviallyNormedField ↥F

Equations

• F.instNontriviallyNormedFieldSubtypeMem = { toNormedField := SubfieldClass.toNormedField F, non_trivial := ⋯ }

theorem WeakDual.CharacterSpace.norm_le_norm_one {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] (φ : ↑(characterSpace 𝕜 A)) : ‖toStrongDual ↑φ‖ ≤ ‖1‖

instance WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace {𝕜 : Type u_1} {A : Type u_2} [NontriviallyNormedField 𝕜] [NormedRing A] [NormedAlgebra 𝕜 A] [CompleteSpace A] [ProperSpace 𝕜] : CompactSpace ↑(characterSpace 𝕜 A)