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

@[protected, simp, norm_cast]
@[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) :
φ = ψ

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

Equations

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

Equations
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}

The character_space 𝕜 A along with 0 is always a closed set in weak_dual 𝕜 A.

@[protected, instance]

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

Equations

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]

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]

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