# mathlibdocumentation

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) [ 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
theorem weak_dual.character_space.coe_apply {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (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
theorem weak_dual.character_space.to_clm_apply {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (x : A) :
φ x =
@[simp]
theorem weak_dual.character_space.to_non_unital_alg_hom_apply {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (ᾰ : A) :
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
theorem weak_dual.character_space.map_zero {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) :
φ 0 = 0
theorem weak_dual.character_space.map_add {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (x y : A) :
φ (x + y) = φ x + φ y
theorem weak_dual.character_space.map_smul {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (r : 𝕜) (x : A) :
φ (r x) = r φ x
theorem weak_dual.character_space.map_mul {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) (x y : A) :
φ (x * y) = φ x * φ y
theorem weak_dual.character_space.continuous {𝕜 : Type u_1} {A : Type u_2} [ A] (φ : ) :
theorem weak_dual.character_space.map_one {𝕜 : Type u_1} {A : Type u_2} [comm_ring 𝕜] [semiring A] [ A] (φ : ) :
φ 1 = 1
@[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, 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}
theorem weak_dual.character_space.is_closed {𝕜 : Type u_1} {A : Type u_2} [comm_ring 𝕜] [semiring A] [ A] [nontrivial 𝕜] [t2_space 𝕜]  :
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