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 WeakDual.characterSpace 𝕜 A as a subset of the weak dual, which automatically puts the correct topology on the space. We then define WeakDual.CharacterSpace.toAlgHom which provides the algebra homomorphism corresponding to any element. We also provide WeakDual.CharacterSpace.toCLM which provides the element as a continuous linear map. (Even though WeakDual 𝕜 A is a type copy of A →L[𝕜] 𝕜, this is often more convenient.)

Tags

character space, Gelfand transform, functional calculus

def WeakDual.characterSpace (𝕜 : Type u_1) (A : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : Set (WeakDual 𝕜 A)

The character space of a topological algebra is the subset of elements of the weak dual that are also algebra homomorphisms.

Equations

• WeakDual.characterSpace 𝕜 A = {φ : WeakDual 𝕜 A | φ ≠ 0 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}

instance WeakDual.CharacterSpace.instFunLike {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : FunLike (↑(WeakDual.characterSpace 𝕜 A)) A 𝕜

Equations

• WeakDual.CharacterSpace.instFunLike = { coe := fun (φ : ↑(WeakDual.characterSpace 𝕜 A)) => ⇑↑φ, coe_injective' := ⋯ }

instance WeakDual.CharacterSpace.instContinuousLinearMapClass {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : ContinuousLinearMapClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜

Elements of the character space are continuous linear maps.

Equations

• ⋯ = ⋯

@[simp]

theorem WeakDual.CharacterSpace.coe_coe {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : ⇑↑φ = ⇑φ

theorem WeakDual.CharacterSpace.ext {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] {φ ψ : ↑(WeakDual.characterSpace 𝕜 A)} (h : ∀ (x : A), φ x = ψ x) : φ = ψ

def WeakDual.CharacterSpace.toCLM {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : A →L[𝕜] 𝕜

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

Equations

• WeakDual.CharacterSpace.toCLM φ = ↑φ

@[simp]

theorem WeakDual.CharacterSpace.coe_toCLM {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : ⇑(WeakDual.CharacterSpace.toCLM φ) = ⇑φ

instance WeakDual.CharacterSpace.instNonUnitalAlgHomClass {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : NonUnitalAlgHomClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜

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

Equations

• ⋯ = ⋯

def WeakDual.CharacterSpace.toNonUnitalAlgHom {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : A →ₙₐ[𝕜] 𝕜

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

Equations

• WeakDual.CharacterSpace.toNonUnitalAlgHom φ = { toFun := ⇑φ, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

@[simp]

theorem WeakDual.CharacterSpace.coe_toNonUnitalAlgHom {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : ⇑(WeakDual.CharacterSpace.toNonUnitalAlgHom φ) = ⇑φ

instance WeakDual.CharacterSpace.instIsEmpty {𝕜 : Type u_1} {A : Type u_2} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] [Subsingleton A] : IsEmpty ↑(WeakDual.characterSpace 𝕜 A)

Equations

• ⋯ = ⋯

theorem WeakDual.CharacterSpace.union_zero (𝕜 : Type u_1) (A : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] : WeakDual.characterSpace 𝕜 A ∪ {0} = {φ : WeakDual 𝕜 A | ∀ (x y : A), φ (x * y) = φ x * φ y}

theorem WeakDual.CharacterSpace.union_zero_isClosed (𝕜 : Type u_1) (A : Type u_2) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [NonUnitalNonAssocSemiring A] [TopologicalSpace A] [Module 𝕜 A] [T2Space 𝕜] [ContinuousMul 𝕜] : IsClosed (WeakDual.characterSpace 𝕜 A ∪ {0})

The characterSpace 𝕜 A along with 0 is always a closed set in WeakDual 𝕜 A.

instance WeakDual.CharacterSpace.instAlgHomClass {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] : AlgHomClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜

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

Equations

• ⋯ = ⋯

def WeakDual.CharacterSpace.toAlgHom {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : A →ₐ[𝕜] 𝕜

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

Equations

• WeakDual.CharacterSpace.toAlgHom φ = { toFun := (WeakDual.CharacterSpace.toNonUnitalAlgHom φ).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem WeakDual.CharacterSpace.toAlgHom_apply {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) (a✝ : A) : (WeakDual.CharacterSpace.toAlgHom φ) a✝ = (WeakDual.CharacterSpace.toNonUnitalAlgHom φ).toFun a✝

theorem WeakDual.CharacterSpace.eq_set_map_one_map_mul {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] [Nontrivial 𝕜] : WeakDual.characterSpace 𝕜 A = {φ : WeakDual 𝕜 A | φ 1 = 1 ∧ ∀ (x y : A), φ (x * y) = φ x * φ y}

theorem WeakDual.CharacterSpace.isClosed {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] [Nontrivial 𝕜] [T2Space 𝕜] [ContinuousMul 𝕜] : IsClosed (WeakDual.characterSpace 𝕜 A)

under suitable mild assumptions on 𝕜, the character space is a closed set in WeakDual 𝕜 A.

theorem WeakDual.CharacterSpace.apply_mem_spectrum {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Ring A] [Algebra 𝕜 A] [Nontrivial 𝕜] (φ : ↑(WeakDual.characterSpace 𝕜 A)) (a : A) : φ a ∈ spectrum 𝕜 a

theorem WeakDual.CharacterSpace.ext_ker {𝕜 : Type u_1} {A : Type u_2} [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [TopologicalSpace A] [Ring A] [Algebra 𝕜 A] {φ ψ : ↑(WeakDual.characterSpace 𝕜 A)} (h : RingHom.ker φ = RingHom.ker ψ) : φ = ψ

instance WeakDual.ker_isMaximal {𝕜 : Type u_1} {A : Type u_2} [Field 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [Ring A] [TopologicalSpace A] [Algebra 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)) : (RingHom.ker φ).IsMaximal

The RingHom.ker of φ : characterSpace 𝕜 A is maximal.

Equations

• ⋯ = ⋯

def WeakDual.gelfandTransform (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] : A →ₐ[𝕜] C(↑(WeakDual.characterSpace 𝕜 A), 𝕜)

The Gelfand transform is an algebra homomorphism (over 𝕜) from a topological 𝕜-algebra A into the 𝕜-algebra of continuous 𝕜-valued functions on the characterSpace 𝕜 A. The character space itself consists of all algebra homomorphisms from A to 𝕜.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeakDual.gelfandTransform_apply_apply (𝕜 : Type u_1) (A : Type u_2) [CommRing 𝕜] [NoZeroDivisors 𝕜] [TopologicalSpace 𝕜] [TopologicalRing 𝕜] [TopologicalSpace A] [Semiring A] [Algebra 𝕜 A] (a : A) (φ : ↑(WeakDual.characterSpace 𝕜 A)) : ((WeakDual.gelfandTransform 𝕜 A) a) φ = φ a