Instances of the continuous functional calculus #
Main theorems #
IsStarNormal.instContinuousFunctionalCalculus
: the continuous functional calculus for normal elements in a unital C⋆-algebra overℂ
.IsSelfAdjoint.instContinuousFunctionalCalculus
: the continuous functional calculus for selfadjoint elements in aℂ
-algebra with a continuous functional calculus for normal elements and where every element has compact spectrum. In particular, this includes unital C⋆-algebras overℂ
.Nonneg.instContinuousFunctionalCalculus
: the continuous functional calculus for nonnegative elements in anℝ
-algebra with a continuous functional calculus for selfadjoint elements, where every element has compact spectrum, and where nonnegative elements have nonnegative spectrum. In particular, this includes unital C⋆-algebras overℝ
.CStarAlgebra.instNonnegSpectrumClass
: In a unital C⋆-algebra overℂ
which is also aStarOrderedRing
, the spectrum of a nonnegative element is nonnegative.
Tags #
continuous functional calculus, normal, selfadjoint
Pull back a non-unital instance from a unital one on the unitization #
This is an auxiliary definition used for constructing an instance of the non-unital continuous functional calculus given a instance of the unital one on the unitization.
This is the natural non-unital star homomorphism obtained from the chain
calc
C(σₙ 𝕜 a, 𝕜)₀ →⋆ₙₐ[𝕜] C(σₙ 𝕜 a, 𝕜) := ContinuousMapZero.toContinuousMapHom
_ ≃⋆[𝕜] C(σ 𝕜 (↑a : A⁺¹), 𝕜) := Homeomorph.compStarAlgEquiv'
_ →⋆ₐ[𝕜] A⁺¹ := cfcHom
This range of this map is contained in the range of (↑) : A → A⁺¹
(see cfcₙAux_mem_range_inr
),
and so we may restrict it to A
to get the necessary homomorphism for the non-unital continuous
functional calculus.
Equations
- cfcₙAux hp₁ a ha = ((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' 𝕜 𝕜 (Homeomorph.setCongr ⋯))).comp ContinuousMapZero.toContinuousMapHom
Instances For
Continuous functional calculus for normal elements #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Continuous functional calculus for selfadjoint elements #
An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in ℝ
.
Alias of the forward direction of isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts
.
An element in a non-unital C⋆-algebra is selfadjoint if and only if it is normal and its
quasispectrum is contained in ℝ
.
A normal element whose ℂ
-quasispectrum is contained in ℝ
is selfadjoint.
Equations
- ⋯ = ⋯
An element in a C⋆-algebra is selfadjoint if and only if it is normal and its spectrum is
contained in ℝ
.
A normal element whose ℂ
-spectrum is contained in ℝ
is selfadjoint.
Equations
- ⋯ = ⋯
Continuous functional calculus for nonnegative elements #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The spectrum of a nonnegative element is nonnegative #
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The partial order on a unital C⋆-algebra defined by x ≤ y
if and only if y - x
is
selfadjoint and has nonnegative spectrum.
This is not declared as an instance because one may already have a partial order with better definitional properties. However, it can be useful to invoke this as an instance in proofs.
Equations
Instances For
The CStarAlgebra.spectralOrder
on a unital C⋆-algebra is a StarOrderedRing
.
Equations
- ⋯ = ⋯