Spectral properties in C⋆-algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. In this file, we establish various properties related to the spectrum of elements in C⋆-algebras.
theorem
unitary.spectrum_subset_circle
{𝕜 : Type u_1}
[normed_field 𝕜]
{E : Type u_2}
[normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_algebra 𝕜 E]
[complete_space E]
(u : ↥(unitary E)) :
spectrum 𝕜 ↑u ⊆ metric.sphere 0 1
theorem
spectrum.subset_circle_of_unitary
{𝕜 : Type u_1}
[normed_field 𝕜]
{E : Type u_2}
[normed_ring E]
[star_ring E]
[cstar_ring E]
[normed_algebra 𝕜 E]
[complete_space E]
{u : E}
(h : u ∈ unitary E) :
spectrum 𝕜 u ⊆ metric.sphere 0 1
theorem
is_self_adjoint.spectral_radius_eq_nnnorm
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
{a : A}
(ha : is_self_adjoint a) :
theorem
is_star_normal.spectral_radius_eq_nnnorm
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
(a : A)
[is_star_normal a] :
theorem
is_self_adjoint.mem_spectrum_eq_re
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
{a : A}
(ha : is_self_adjoint a)
{z : ℂ}
(hz : z ∈ spectrum ℂ a) :
Any element of the spectrum of a selfadjoint is real.
theorem
self_adjoint.mem_spectrum_eq_re
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
(a : ↥(self_adjoint A))
{z : ℂ}
(hz : z ∈ spectrum ℂ ↑a) :
Any element of the spectrum of a selfadjoint is real.
theorem
is_self_adjoint.coe_re_map_spectrum
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
{a : A}
(ha : is_self_adjoint a) :
The spectrum of a selfadjoint is real
theorem
self_adjoint.coe_re_map_spectrum
{A : Type u_1}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
(a : ↥(self_adjoint A)) :
The spectrum of a selfadjoint is real
theorem
star_alg_hom.nnnorm_apply_le
{F : Type u_1}
{A : Type u_2}
{B : Type u_3}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[normed_ring B]
[normed_algebra ℂ B]
[complete_space B]
[star_ring B]
[cstar_ring B]
[hF : star_alg_hom_class F ℂ A B]
(φ : F)
(a : A) :
A star algebra homomorphism of complex C⋆-algebras is norm contractive.
theorem
star_alg_hom.norm_apply_le
{F : Type u_1}
{A : Type u_2}
{B : Type u_3}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[normed_ring B]
[normed_algebra ℂ B]
[complete_space B]
[star_ring B]
[cstar_ring B]
[hF : star_alg_hom_class F ℂ A B]
(φ : F)
(a : A) :
A star algebra homomorphism of complex C⋆-algebras is norm contractive.
@[protected, instance]
noncomputable
def
star_alg_hom.continuous_linear_map_class
{F : Type u_1}
{A : Type u_2}
{B : Type u_3}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[normed_ring B]
[normed_algebra ℂ B]
[complete_space B]
[star_ring B]
[cstar_ring B]
[hF : star_alg_hom_class F ℂ A B] :
continuous_linear_map_class F ℂ A B
Star algebra homomorphisms between C⋆-algebras are continuous linear maps. See note [lower instance priority]
Equations
- star_alg_hom.continuous_linear_map_class = {coe := semilinear_map_class.coe alg_hom_class.linear_map_class, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
@[protected, instance]
noncomputable
def
weak_dual.complex.star_hom_class
{F : Type u_1}
{A : Type u_2}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
[hF : alg_hom_class F ℂ A ℂ] :
star_hom_class F A ℂ
This instance is provided instead of star_alg_hom_class to avoid type class inference loops.
See note [lower instance priority]
Equations
- weak_dual.complex.star_hom_class = {coe := λ (φ : F), ⇑φ, coe_injective' := _, map_star := _}
noncomputable
def
alg_hom_class.star_alg_hom_class
{F : Type u_1}
{A : Type u_2}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A]
[hF : alg_hom_class F ℂ A ℂ] :
star_alg_hom_class F ℂ A ℂ
This is not an instance to avoid type class inference loops. See
weak_dual.complex.star_hom_class.
@[protected, instance]
noncomputable
def
weak_dual.character_space.complex.star_alg_hom_class
{A : Type u_2}
[normed_ring A]
[normed_algebra ℂ A]
[complete_space A]
[star_ring A]
[cstar_ring A]
[star_module ℂ A] :
Equations
- weak_dual.character_space.complex.star_alg_hom_class = {coe := λ (f : ↥(weak_dual.character_space ℂ A)), ⇑f, coe_injective' := _, map_mul := _, map_one := _, map_add := _, map_zero := _, commutes := _, map_star := _}