Conditions on unitary elements imposed by the continuous functional calculus #
Main theorems #
unitary_iff_isStarNormal_and_spectrum_subset_unitary
: An element is unitary if and only if it is star-normal and its spectrum lies on the unit circle.
theorem
cfc_unitary_iff
{R : Type u_1}
{A : Type u_2}
{p : A → Prop}
[CommRing R]
[StarRing R]
[MetricSpace R]
[TopologicalRing R]
[ContinuousStar R]
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra R A]
[ContinuousFunctionalCalculus R p]
(f : R → R)
(a : A)
(ha : autoParam (p a) _auto✝)
(hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝)
:
theorem
unitary_iff_isStarNormal_and_spectrum_subset_unitary
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{u : A}
:
theorem
mem_unitary_of_spectrum_subset_unitary
{A : Type u_1}
[TopologicalSpace A]
[Ring A]
[StarRing A]
[Algebra ℂ A]
[ContinuousFunctionalCalculus ℂ IsStarNormal]
{u : A}
[IsStarNormal u]
(hu : spectrum ℂ u ⊆ ↑(unitary ℂ))
: