English
A quasispectrum inclusion holds after applying a non-unital algebra homomorphism with explicit scalar-tower relations, i.e., φ preserves the relevant quasispectrum inclusion.
Русский
После применения не-юнит-гомоморфизма сохраняется включение квазиспектра, при явном отношении к каскадам скаляров.
LaTeX
$$$$ \operatorname{quasispectrum}(R, \phi(a)) \subseteq \operatorname{quasispectrum}(R, a) $$$$
Lean4
theorem isQuasiregular_iff_isUnit' (R : Type*) {A : Type*} [CommSemiring R] [NonUnitalSemiring A] [Module R A]
[IsScalarTower R A A] [SMulCommClass R A A] {x : A} : IsQuasiregular x ↔ IsUnit (1 + x : Unitization R A) :=
by
refine ⟨?_, fun hx ↦ ?_⟩
· rintro ⟨u, rfl⟩
exact (Unitization.unitsFstOne_mulEquiv_quasiregular R).symm u |>.val.isUnit
· exact ⟨(Unitization.unitsFstOne_mulEquiv_quasiregular R) ⟨hx.unit, by simp⟩, by simp⟩
