# mathlib3documentation

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

def weak_dual.character_space (𝕜 : Type u_1) (A : Type u_2) [ A] :
set 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} [ 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} [ A] {φ ψ : } (h : (x : A), φ x = ψ x) :
φ = ψ
def weak_dual.character_space.to_clm {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) :
A →L[𝕜] 𝕜

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

Equations
@[simp]
theorem weak_dual.character_space.coe_to_clm {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) :
@[protected, instance]
def weak_dual.character_space.non_unital_alg_hom_class {𝕜 : Type u_1} {A : Type u_2} [ A] :

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} [ A] (φ : ) :
A →ₙₐ[𝕜] 𝕜

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

Equations
@[simp]
theorem weak_dual.character_space.coe_to_non_unital_alg_hom {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) :
@[protected, instance]
def weak_dual.character_space.is_empty {𝕜 : Type u_1} {A : Type u_2} [ A] [subsingleton A] :
theorem weak_dual.character_space.union_zero (𝕜 : Type u_1) (A : Type u_2) [ A] :
{0} = {φ : A | (x y : A), φ (x * y) = φ x * φ y}
theorem weak_dual.character_space.union_zero_is_closed (𝕜 : Type u_1) (A : Type u_2) [ A] [t2_space 𝕜]  :

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 𝕜] [semiring A] [ 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 𝕜] [semiring A] [ A] (φ : ) (ᾰ : A) :
def weak_dual.character_space.to_alg_hom {𝕜 : Type u_1} {A : Type u_2} [comm_ring 𝕜] [semiring A] [ 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 𝕜] [semiring A] [ A] [nontrivial 𝕜] :
= {φ : 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 𝕜] [semiring A] [ A] [nontrivial 𝕜] [t2_space 𝕜]  :

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 𝕜] [ring A] [ A] [nontrivial 𝕜] (φ : ) (a : A) :
φ a a
theorem weak_dual.character_space.ext_ker {𝕜 : Type u_1} {A : Type u_2} [comm_ring 𝕜] [ring A] [ A] {φ ψ : } (h : = ) :
φ = ψ
@[protected, instance]
def weak_dual.ker_is_maximal {𝕜 : Type u_1} {A : Type u_2} [field 𝕜] [ring A] [ 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 𝕜] [semiring A] [ A] :
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 𝕜] [semiring A] [ A] (a : A) (φ : ) :
( a) φ = φ a