mathlib3 documentation

topology.algebra.module.character_space

Character space of a topological algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
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
source
@[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)) :
⇑↑φ = ⇑φ
source
@[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
source
@[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) :
φ = ψ
source
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
source
@[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 φ) = ⇑φ
source
@[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
source
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
source
@[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 φ) = ⇑φ
source
@[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)
source
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}
source
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.

source
@[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
source
@[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 ᾰ
source
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
source
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}
source
@[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.

source
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
source
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 ψ) :
φ = ψ
source
@[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.

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