Operator Algebras in Lean

0.2 Continuous functional calculus

Definition 1 Continuous functional calculus
#

A \(*\)-\(R\)-algebra is said to have a continuous functional calculus for elements satisfying a predicate \(p\) if, for each \(a\) satisfying \(p\), there is a \(*\)-homomorphism \(\phi _a : C(\sigma _{R}(a), R) \to A\) sending the identity function to \(a\), and which is a closed embedding. Moreover, \(\sigma _{R}(a)\) is compact and nonempty, and \(\phi _a\) satisfies the spectral mapping property (i.e., \(\sigma _{R}(\phi _a(f)) = f(\sigma _{R}(a))\)).

Definition 2 Non-unital continuous functional calculus
#

A non-unital \(*\)-\(R\)-algebra is said to have a non-unital continuous functional calculus for elements satisfying a predicate \(p\) if, for each \(a\) satisfying \(p\), there is a non-unital \(*\)-homomorphism \(\phi _a : C(\sigma '_{R}(a), R)_0 \to A\) (here \(C(\sigma '_{R}(a), R)_0\) is the collection of functions vanishing at zero on the quasispectrum) sending the identity function to \(a\), and which is a closed embedding. Moreover, \(\sigma '_{R}(a)\) is compact (it’s always nonempty because it contains \(0\)), and \(\phi '_a\) satisfies the spectral mapping property (i.e., \(\sigma '_{R}(\phi '_a(f)) = f(\sigma '_{R}(a))\)).

Definition 3
#

Given \(a \in A\) satisfying \(p\) and \(f : R → R\) continuous on \(\sigma _{R}(a)\), we define \(f(a) := \phi '_a(f)\) (and we give it a junk value of zero when either \(a\) does not satisfy \(p\) or \(f\) is not continuous on the spectrum).

Definition 4
#

Given \(a \in A\) satisfying \(p\) and \(f : R → R\) continuous on \(\sigma _{R}(a)\) and \(f(0) = 0\), we define \(f(a) := \phi '_a(f)\) (and we give it a junk value of zero when and of the conditions on \(a\) and \(f\) are not met).

Theorem 5
#

For every normal element \(a\) in a unital \(C^*\)-algebra \(A\) there is a \(*\)-isomorphism between \(C(\sigma _{}(a), ℂ)\) and the \(C^*\)-subalgebra of \(A\) generated by \(a\).

Proof

Use the Gelfand transform.

Every unital \(C^*\)-algebra has a continuous functional calculus for normal elements.

Proof

Compose the \(*\)-isomorphism of Theorem 5, which is an isometry because its an isomorphism of \(C^*\)-algebras, with the inclusion of \(C^{*}_1(a)\) (the unital \(C^*\)-subalgebra generated by \(a\)) into \(A\). The latter is also an isometry and therefore a closed embedding.

Theorem 7

Every unital \(*\)-algebra \(A\) with a continuous functional calculus for normal elements over \(\mathbb {C}\) has a continuous functional calculus for self-adjoint elements over \(\mathbb {R}\).

Proof

Since self-adjoint elements are normal, the continuous functional calculus for normal elements over \(\mathbb {C}\) with its spectral mapping property guarantees that the \(\mathbb {C}\)-spectrum of \(a \in A\) normal is actually contained in \(\mathbb {R}\), and so coincides with the \(\mathbb {R}\)-spectrum of \(a\). Therefore, the map which sends \(f \in C(\sigma _{\mathbb {R}}(a), \mathbb {R})\) to \(\hat f \in C(\sigma _{\mathbb {C}}(a), \mathbb {C})\) is a \(*\)-homomorphism, and composing it with \(\phi _a\) yields the desired \(*\)-homomorphism for the contnuous functional calculus over \(\mathbb {R}\) for self-adjoint elements.

Every unital \(*\)-algebra \(A\) which is a \(*\)-ordered ring (i.e., nonnegative elements are those of the form \(x^* x\)) with the property that nonnegative elements have nonnegative spectrum, and with a continuous functional calculus for self-adjoint elements over \(\mathbb {R}\) has a continuous functional calculus for self-adjoint elements over \(\mathbb {R}_{\ge 0}\).

Proof

Omitted.