English
For a commutative ring R and A an algebra, the quasispectrum of a equals the union of the spectrum of a and the set of nonunits of R.
Русский
Для коммутативного кольца R и алгебры A квазиспектр a равен объединению спектра a и множества неединичных элементов R.
LaTeX
$$$$ \operatorname{quasispectrum}(R,a) = \operatorname{spectrum}(R,a) \cup \{ r \in R \mid \neg \operatorname{IsUnit}(r) \} $$$$
Lean4
theorem quasispectrum_eq_spectrum_union (R : Type*) {A : Type*} [CommSemiring R] [Ring A] [Algebra R A] (a : A) :
quasispectrum R a = spectrum R a ∪ {r : R | ¬IsUnit r} :=
by
ext r
rw [quasispectrum]
simp only [Set.mem_setOf_eq, Set.mem_union, ← imp_iff_or_not, spectrum.mem_iff]
congr! 1 with hr
rw [not_iff_not, isQuasiregular_iff_isUnit, ← sub_eq_add_neg, Algebra.algebraMap_eq_smul_one]
exact (IsUnit.smul_sub_iff_sub_inv_smul hr.unit a).symm
