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] [IsTopologicalRing R] [ContinuousStar R] [TopologicalSpace A] [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R A p] (f : R → R) (a : A) (ha : p a := by cfc_tac) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) : cfc f a ∈ unitary A ↔ ∀ x ∈ spectrum R a, star (f x) * f x = 1

theorem unitary_iff_isStarNormal_and_spectrum_subset_unitary {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A} : u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

theorem mem_unitary_of_spectrum_subset_unitary {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A} [IsStarNormal u] (hu : spectrum ℂ u ⊆ ↑(unitary ℂ)) : u ∈ unitary A

theorem spectrum_subset_unitary_of_mem_unitary {A : Type u_1} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] {u : A} (hu : u ∈ unitary A) : spectrum ℂ u ⊆ ↑(unitary ℂ)