mathlib documentation

topology.algebra.module.character_space

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

def weak_dual.character_space (π•œ : Type u_1) (A : Type u_2) [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] :
set (weak_dual π•œ A)

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
theorem weak_dual.character_space.coe_apply {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (x : A) :
⇑↑φ x = ⇑φ x
def weak_dual.character_space.to_clm {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
A β†’L[π•œ] π•œ

An element of the character space, as a continuous linear map.

Equations
theorem weak_dual.character_space.to_clm_apply {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (x : A) :
@[simp]
theorem weak_dual.character_space.to_non_unital_alg_hom_apply {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (αΎ° : A) :
def weak_dual.character_space.to_non_unital_alg_hom {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
A →ₙₐ[π•œ] π•œ

An element of the character space, as an non-unital algebra homomorphism.

Equations
theorem weak_dual.character_space.map_zero {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
⇑φ 0 = 0
theorem weak_dual.character_space.map_add {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (x y : A) :
⇑φ (x + y) = ⇑φ x + ⇑φ y
theorem weak_dual.character_space.map_smul {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (r : π•œ) (x : A) :
⇑φ (r β€’ x) = r β€’ ⇑φ x
theorem weak_dual.character_space.map_mul {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (x y : A) :
⇑φ (x * y) = ⇑φ x * ⇑φ y
theorem weak_dual.character_space.continuous {π•œ : Type u_1} {A : Type u_2} [comm_semiring π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [non_unital_non_assoc_semiring A] [topological_space A] [module π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
theorem weak_dual.character_space.map_one {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [semiring A] [algebra π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
⇑φ 1 = 1
@[simp]
theorem weak_dual.character_space.to_alg_hom_apply {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [semiring A] [algebra π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) (αΎ° : A) :
def weak_dual.character_space.to_alg_hom {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [semiring A] [algebra π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :
A →ₐ[π•œ] π•œ

An element of the character space, as an algebra homomorphism.

Equations
theorem weak_dual.character_space.eq_set_map_one_map_mul {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [semiring A] [algebra π•œ A] [nontrivial π•œ] :
weak_dual.character_space π•œ A = {Ο† : weak_dual π•œ A | ⇑φ 1 = 1 ∧ βˆ€ (x y : A), ⇑φ (x * y) = ⇑φ x * ⇑φ y}
theorem weak_dual.character_space.is_closed {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [semiring A] [algebra π•œ A] [nontrivial π•œ] [t2_space π•œ] [has_continuous_mul π•œ] :
theorem weak_dual.character_space.apply_mem_spectrum {π•œ : Type u_1} {A : Type u_2} [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [topological_space A] [ring A] [algebra π•œ A] [nontrivial π•œ] (Ο† : β†₯(weak_dual.character_space π•œ A)) (a : A) :
⇑φ a ∈ spectrum π•œ a