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

weak_dual.character_space 𝕜 A = {φ : weak_dual 𝕜 A | φ ≠ 0 ∧ ∀ (x y : A), ⇑φ (x * y) = ⇑φ x * ⇑φ y}

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]

def weak_dual.character_space.continuous_linear_map_class {𝕜 : 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] :

continuous_linear_map_class ↥(weak_dual.character_space 𝕜 A) 𝕜 A 𝕜

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 := _}

@[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

weak_dual.character_space.to_clm φ = ↑φ

@[simp]

theorem weak_dual.character_space.coe_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)) :

⇑(weak_dual.character_space.to_clm φ) = ⇑φ

@[protected, instance]

def weak_dual.character_space.non_unital_alg_hom_class {𝕜 : 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] :

non_unital_alg_hom_class ↥(weak_dual.character_space 𝕜 A) 𝕜 A 𝕜

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

Equations

weak_dual.character_space.non_unital_alg_hom_class = {coe := continuous_semilinear_map_class.coe weak_dual.character_space.continuous_linear_map_class, coe_injective' := _, map_smul := _, map_add := _, map_zero := _, map_mul := _}

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

weak_dual.character_space.to_non_unital_alg_hom φ = {to_fun := ⇑φ, map_smul' := _, map_zero' := _, map_add' := _, map_mul' := _}

@[simp]

theorem weak_dual.character_space.coe_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)) :

⇑(weak_dual.character_space.to_non_unital_alg_hom φ) = ⇑φ

@[protected, instance]

def weak_dual.character_space.is_empty {𝕜 : 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] [subsingleton A] :

is_empty ↥(weak_dual.character_space 𝕜 A)

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 𝕜] :

is_closed (weak_dual.character_space 𝕜 A ∪ {0})

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

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 := _}

@[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) :

⇑(weak_dual.character_space.to_alg_hom φ) ᾰ = (weak_dual.character_space.to_non_unital_alg_hom φ).to_fun ᾰ

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

weak_dual.character_space.to_alg_hom φ = {to_fun := (weak_dual.character_space.to_non_unital_alg_hom φ).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

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 𝕜] :

is_closed (weak_dual.character_space 𝕜 A)

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)) :

(ring_hom.ker φ).is_maximal

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] :

A →ₐ[𝕜] C(↥(weak_dual.character_space 𝕜 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

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' := _}

@[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)) :

⇑(⇑(weak_dual.gelfand_transform 𝕜 A) a) φ = ⇑φ a