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
@[protected, simp, norm_cast]
theorem weak_dual.character_space.coe_coe {π•œ : 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)) :
@[protected, instance]

Elements of the character space are continuous linear maps.

Equations
@[ext]
theorem weak_dual.character_space.ext {π•œ : 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)} (h : βˆ€ (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
@[simp]
@[protected, instance]

Elements of the character space are non-unital algebra homomorphisms.

Equations
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
@[protected, instance]
theorem weak_dual.character_space.union_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} = {Ο† : weak_dual π•œ A | βˆ€ (x y : A), ⇑φ (x * y) = ⇑φ x * ⇑φ y}
theorem weak_dual.character_space.union_zero_is_closed (π•œ : 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] [t2_space π•œ] [has_continuous_mul π•œ] :

The character_space π•œ A along with 0 is always a closed set in weak_dual π•œ A.

@[protected, instance]
def weak_dual.character_space.alg_hom_class {π•œ : 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] :
alg_hom_class β†₯(weak_dual.character_space π•œ A) π•œ A π•œ

In a unital algebra, elements of the character space are algebra homomorphisms.

Equations
@[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 of a unital algebra, 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}
@[protected]
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 π•œ] :

under suitable mild assumptions on π•œ, the character space is a closed set in weak_dual π•œ A.

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
theorem weak_dual.character_space.ext_ker {π•œ : 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] {Ο† ψ : β†₯(weak_dual.character_space π•œ A)} (h : ring_hom.ker Ο† = ring_hom.ker ψ) :
Ο† = ψ
@[protected, instance]
def weak_dual.ker_is_maximal {π•œ : Type u_1} {A : Type u_2} [field π•œ] [topological_space π•œ] [has_continuous_add π•œ] [has_continuous_const_smul π•œ π•œ] [ring A] [topological_space A] [algebra π•œ A] (Ο† : β†₯(weak_dual.character_space π•œ A)) :

The ring_hom.ker of Ο† : character_space π•œ A is maximal.

def weak_dual.gelfand_transform (π•œ : Type u_1) (A : Type u_2) [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [topological_ring π•œ] [topological_space A] [semiring A] [algebra π•œ A] :

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
@[simp]
theorem weak_dual.gelfand_transform_apply_apply (π•œ : Type u_1) (A : Type u_2) [comm_ring π•œ] [no_zero_divisors π•œ] [topological_space π•œ] [topological_ring π•œ] [topological_space A] [semiring A] [algebra π•œ A] (a : A) (Ο† : β†₯(weak_dual.character_space π•œ A)) :