Character space of a topological algebra #
The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms. This space is used in the Gelfand transform, which gives an isomorphism between a commutative Cβ-algebra and continuous functions on the character space of the algebra. This, in turn, is used to construct the continuous functional calculus on Cβ-algebras.
Implementation notes #
We define character_space π A
as a subset of the weak dual, which automatically puts the
correct topology on the space. We then define to_alg_hom
which provides the algebra homomorphism
corresponding to any element. We also provide to_clm
which provides the element as a
continuous linear map. (Even though weak_dual π A
is a type copy of A βL[π] π
, this is
often more convenient.)
Tags #
character space, Gelfand transform, functional calculus
The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms.
Equations
Instances for β₯weak_dual.character_space
- weak_dual.character_space.continuous_linear_map_class
- weak_dual.character_space.non_unital_alg_hom_class
- weak_dual.character_space.is_empty
- weak_dual.character_space.alg_hom_class
- weak_dual.character_space.compact_space
- weak_dual.character_space.complex.star_alg_hom_class
- weak_dual.character_space.nonempty
Elements of the character space are continuous linear maps.
Equations
- weak_dual.character_space.continuous_linear_map_class = {coe := Ξ» (Ο : β₯(weak_dual.character_space π A)), βΟ, coe_injective' := _, map_add := _, map_smulββ := _, map_continuous := _}
An element of the character space, as a continuous linear map.
Equations
Elements of the character space are non-unital algebra homomorphisms.
Equations
An element of the character space, as an non-unital algebra homomorphism.
The character_space π A
along with 0
is always a closed set in weak_dual π A
.
In a unital algebra, elements of the character space are algebra homomorphisms.
Equations
- weak_dual.character_space.alg_hom_class = have map_one' : β (Ο : β₯(weak_dual.character_space π A)), βΟ 1 = 1, from weak_dual.character_space.alg_hom_class._proof_6, {coe := non_unital_alg_hom_class.coe weak_dual.character_space.non_unital_alg_hom_class, coe_injective' := _, map_mul := _, map_one := map_one', map_add := _, map_zero := _, commutes := _}
An element of the character space of a unital algebra, as an algebra homomorphism.
under suitable mild assumptions on π
, the character space is a closed set in
weak_dual π A
.
The ring_hom.ker
of Ο : character_space π A
is maximal.
The Gelfand transform is an algebra homomorphism (over π
) from a topological π
-algebra
A
into the π
-algebra of continuous π
-valued functions on the character_space π A
.
The character space itself consists of all algebra homomorphisms from A
to π
.
Equations
- weak_dual.gelfand_transform π A = {to_fun := Ξ» (a : A), {to_fun := Ξ» (Ο : β₯(weak_dual.character_space π A)), βΟ a, continuous_to_fun := _}, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}