instNonnegSpectrumClass' — Mathlib

English

Another instance variant for nonunital C*-algebras ensuring nonnegative spectrum via unitization.

Русский

Еще один вариант экземпляра для неединичных C*-алгебр через единичизацию.

LaTeX

$$NonnegSpectrumClass' Real A$$

Lean4

instance instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where
  quasispectrum_nonneg_of_nonneg a
    ha :=
    by
    rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ]
      -- should this actually be an instance on the `Unitization`? (probably scoped)

    let _ := CStarAlgebra.spectralOrder A⁺¹
    have := CStarAlgebra.spectralOrderedRing A⁺¹
    apply spectrum_nonneg_of_nonneg
    rw [StarOrderedRing.nonneg_iff] at ha ⊢
    have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha
    rw [AddMonoidHom.map_mclosure, ← Set.range_comp] at this
    apply AddSubmonoid.closure_mono ?_ this
    rintro _ ⟨s, rfl⟩
    exact ⟨s, by simp⟩

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