quasispectrum_eq_spectrum_inr — Mathlib

English

For a ∈ A, quasispectrum(R, a) equals spectrum(R, a viewed in unitization via inr).

Русский

Для a ∈ A квази-спектр равен спектру через встраивание вinr в единичную конструкцию.

LaTeX

$$quasispectrum(R, a) = spectrum(R, (a : Unitization.inr A))$$

Lean4

theorem quasispectrum_eq_spectrum_inr (R : Type*) {A : Type*} [CommRing R] [NonUnitalRing A] [Module R A]
    [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : quasispectrum R a = spectrum R (a : Unitization R A) :=
  by
  ext r
  have : {r | ¬IsUnit r} ⊆ spectrum R _ := mem_spectrum_inr_of_not_isUnit a
  rw [← Set.union_eq_left.mpr this, ← quasispectrum_eq_spectrum_union]
  apply forall_congr' fun hr ↦ ?_
  rw [not_iff_not, Units.smul_def, Units.smul_def, ← inr_smul, ← inr_neg, isQuasiregular_inr_iff]

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