instNonnegSpectrumClassComplexNonUnital

English

There exists a canonical class describing nonnegative spectrum for complex scalars acting on a nonunital C*-algebra A, compatible with taking the unitization. In particular, if a ≥ 0, the nonnegative spectrum condition holds when viewed inside the unitization.

Русский

Существует канонический класс, задающий неотрицательный спектр для комплексных масштабов, действующих на безнулевое C*-алгебра A, совместимый с единичной нормой. В частности, если a ≥ 0, неотрицательное свойство спектра сохраняется при рассмотрении в единичной норме.

LaTeX

$$$\\text{NonnegSpectrumClass}_{\\mathbb{C}}(A)\\quad\\text{(for a in }A\\text{ with }a\\ge 0).$$$

Lean4

instance instNonnegSpectrumClassComplexNonUnital : NonnegSpectrumClass ℂ A where
  quasispectrum_nonneg_of_nonneg a ha x
    hx := by
    rw [Unitization.quasispectrum_eq_spectrum_inr' ℂ ℂ a] at hx
    exact spectrum_nonneg_of_nonneg (Unitization.inr_nonneg_iff.mpr ha) hx

Похожие утверждения