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] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : ‖WeakDual.toNormedDual ↑φ‖ ≤ ‖1‖

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

Equations

• (_ : CompactSpace ↑(WeakDual.characterSpace 𝕜 A)) = (_ : CompactSpace ↑(WeakDual.characterSpace 𝕜 A))