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
Alias of isClosedEmbedding_cfcₙAux
.
Continuous functional calculus for normal elements #
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.
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.
Continuous functional calculus for nonnegative elements #
The spectrum of a nonnegative element is nonnegative #
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
.
The restriction of a continuous functional calculus is equal to the original one #
This lemma requires a lot from type class synthesis, and so one should instead favor the bespoke
versions for ℝ≥0
, ℝ
, and ℂ
.
note: the version for ℝ≥0
, Unization.nnreal_cfcₙ_eq_cfc_inr
, can be found in
Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order