Quasiregularity and quasispectrum

For a non-unital ring R, an element r : R is quasiregular if it is invertible in the monoid (R, ∘) where x ∘ y := y + x + x * y with identity 0 : R. We implement this both as a type synonym PreQuasiregular which has an associated Monoid instance (note: not an AddMonoid instance despite the fact that 0 : R is the identity in this monoid) so that one may access the quasiregular elements of R as (PreQuasiregular R)ˣ, but also as a predicate IsQuasiregular.

Quasiregularity is closely tied to invertibility. Indeed, (PreQuasiregular A)ˣ is isomorphic to the subgroup of Unitization R A whose scalar part is 1, whenever A is a non-unital R-algebra, and moreover this isomorphism is implemented by the map (x : A) ↦ (1 + x : Unitization R A). It is because of this isomorphism, and the associated ties with multiplicative invertibility, that we choose a Monoid (as opposed to an AddMonoid) structure on PreQuasiregular. In addition, in unital rings, we even have IsQuasiregular x ↔ IsUnit (1 + x).

The quasispectrum of a : A (with respect to R) is defined in terms of quasiregularity, and this is the natural analogue of the spectrum for non-unital rings. Indeed, it is true that quasispectrum R a = spectrum R a ∪ {0} when A is unital.

In Mathlib, the quasispectrum is the domain of the continuous functions associated to the non-unital continuous functional calculus.

Main definitions

• PreQuasiregular R: a structure wrapping R that inherits a distinct Monoid instance when R is a non-unital semiring.
• Unitization.unitsFstOne: the subgroup with carrier { x : (Unitization R A)ˣ | x.fst = 1 }.
• unitsFstOne_mulEquiv_quasiregular: the group isomorphism between Unitization.unitsFstOne and the units of PreQuasiregular (i.e., the quasiregular elements) which sends (1, x) ↦ x.
• IsQuasiregular x: the proposition that x : R is a unit with respect to the monoid structure on PreQuasiregular R, i.e., there is some u : (PreQuasiregular R)ˣ such that u.val is identified with x (via the natural equivalence between R and PreQuasiregular R).
• quasispectrum R a: in an algebra over the semifield R, this is the set {r : R | (hr : IsUnit r) → ¬ IsQuasiregular (-(hr.unit⁻¹ • a))}, which should be thought of as a version of the spectrum which is applicable in non-unital algebras.

Main theorems

• isQuasiregular_iff_isUnit: in a unital ring, x is quasiregular if and only if 1 + x is a unit.
• quasispectrum_eq_spectrum_union_zero: in a unital algebra A over a semifield R, the quasispectrum of a : A is the spectrum with zero added.
• Unitization.isQuasiregular_inr_iff: a : A is quasiregular if and only if it is quasiregular in Unitization R A (via the coercion Unitization.inr).
• Unitization.quasispectrum_eq_spectrum_inr: the quasispectrum of a in a non-unital R-algebra A is precisely the spectrum of a in the unitization. in Unitization R A (via the coercion Unitization.inr).

structure PreQuasiregular (R : Type u_1) : Type u_1

A type synonym for non-unital rings where an alternative monoid structure is introduced. If R is a non-unital semiring, then PreQuasiregular R is equipped with the monoid structure with binary operation fun x y ↦ y + x + x * y and identity 0. Elements of R which are invertible in this monoid satisfy the predicate IsQuasiregular.

• val : R

  The value wrapped into a term of PreQuasiregular.

def PreQuasiregular.equiv {R : Type u_1} : R ≃ PreQuasiregular R

The identity map between R and PreQuasiregular R.

@[simp]

theorem PreQuasiregular.equiv_apply_val {R : Type u_1} (val : R) : (equiv val).val = val

@[simp]

theorem PreQuasiregular.equiv_symm_apply {R : Type u_1} (self : PreQuasiregular R) : equiv.symm self = self.val

instance PreQuasiregular.instOne {R : Type u_1} [NonUnitalSemiring R] : One (PreQuasiregular R)

@[simp]

theorem PreQuasiregular.val_one {R : Type u_1} [NonUnitalSemiring R] : val 1 = 0

instance PreQuasiregular.instMul {R : Type u_1} [NonUnitalSemiring R] : Mul (PreQuasiregular R)

@[simp]

theorem PreQuasiregular.val_mul {R : Type u_1} [NonUnitalSemiring R] (x y : PreQuasiregular R) : (x * y).val = y.val + x.val + x.val * y.val

instance PreQuasiregular.instMonoid {R : Type u_1} [NonUnitalSemiring R] : Monoid (PreQuasiregular R)

@[simp]

theorem PreQuasiregular.inv_add_add_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ) : (↑u⁻¹).val + (↑u).val + (↑u).val * (↑u⁻¹).val = 0

@[simp]

theorem PreQuasiregular.add_inv_add_mul_eq_zero {R : Type u_1} [NonUnitalSemiring R] (u : (PreQuasiregular R)ˣ) : (↑u).val + (↑u⁻¹).val + (↑u⁻¹).val * (↑u).val = 0

def Unitization.unitsFstOne (R : Type u_1) (A : Type u_2) [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Subgroup (Unitization R A)ˣ

The subgroup of the units of Unitization R A whose scalar part is 1.

@[simp]

theorem Unitization.mem_unitsFstOne {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : (Unitization R A)ˣ} : x ∈ unitsFstOne R A ↔ (↑x).fst = 1

@[simp]

theorem Unitization.unitsFstOne_val_val_fst {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : ↥(unitsFstOne R A)) : (↑↑x).fst = 1

@[simp]

theorem Unitization.unitsFstOne_val_inv_val_fst {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : ↥(unitsFstOne R A)) : (↑(↑x)⁻¹).fst = 1

def Unitization.unitsFstOne_mulEquiv_quasiregular (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : ↥(unitsFstOne R A) ≃* (PreQuasiregular A)ˣ

If A is a non-unital R-algebra, then the subgroup of units of Unitization R A whose scalar part is 1 : R (i.e., Unitization.unitsFstOne) is isomorphic to the group of units of PreQuasiregular A.

@[simp]

theorem Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑(↑((unitsFstOne_mulEquiv_quasiregular R).symm x))⁻¹ = 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)

@[simp]

theorem Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : ↥(unitsFstOne R A)) : ↑((unitsFstOne_mulEquiv_quasiregular R) x)⁻¹ = PreQuasiregular.equiv (↑↑x⁻¹).snd

@[simp]

theorem Unitization.val_unitsFstOne_mulEquiv_quasiregular_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : ↥(unitsFstOne R A)) : ↑((unitsFstOne_mulEquiv_quasiregular R) x) = PreQuasiregular.equiv (↑↑x).snd

@[simp]

theorem Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : (PreQuasiregular A)ˣ) : ↑↑((unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)

def IsQuasiregular {R : Type u_1} [NonUnitalSemiring R] (x : R) : Prop

In a non-unital semiring R, an element x : R satisfies IsQuasiregular if it is a unit under the monoid operation fun x y ↦ y + x + x * y.

@[simp]

theorem isQuasiregular_zero : IsQuasiregular 0

theorem isQuasiregular_iff {R : Type u_1} [NonUnitalSemiring R] {x : R} : IsQuasiregular x ↔ ∃ (y : R), y + x + x * y = 0 ∧ x + y + y * x = 0

theorem isQuasiregular_iff' {R : Type u_1} [NonUnitalSemiring R] {x : R} : IsQuasiregular x ↔ IsUnit (PreQuasiregular.equiv x)

theorem IsQuasiregular.map {F : Type u_1} {R : Type u_2} {S : Type u_3} [NonUnitalSemiring R] [NonUnitalSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) {x : R} (hx : IsQuasiregular x) : IsQuasiregular (f x)

theorem IsQuasiregular.isUnit_one_add {R : Type u_1} [Semiring R] {x : R} (hx : IsQuasiregular x) : IsUnit (1 + x)

theorem isQuasiregular_iff_isUnit {R : Type u_1} [Ring R] {x : R} : IsQuasiregular x ↔ IsUnit (1 + x)

theorem isQuasiregular_iff_isUnit' (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalSemiring A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : A} : IsQuasiregular x ↔ IsUnit (1 + ↑x)

def quasispectrum (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) : Set R

If A is a non-unital R-algebra, the R-quasispectrum of a : A consists of those r : R such that if r is invertible (in R), then -(r⁻¹ • a) is not quasiregular.

The quasispectrum is precisely the spectrum in the unitization when R is a commutative ring. See Unitization.quasispectrum_eq_spectrum_inr.

theorem quasispectrum.not_isUnit_mem {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) {r : R} (hr : ¬IsUnit r) : r ∈ quasispectrum R a

@[simp]

theorem quasispectrum.zero_mem (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) : 0 ∈ quasispectrum R a

theorem quasispectrum.nonempty (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) : (quasispectrum R a).Nonempty

instance quasispectrum.instZero (R : Type u_1) {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) : Zero ↑(quasispectrum R a)

theorem NonUnitalAlgHom.quasispectrum_apply_subset' {F : Type u_3} {R : Type u_4} (S : Type u_5) {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring S] [NonUnitalRing A] [NonUnitalRing B] [Module R S] [Module S A] [Module R A] [Module S B] [Module R B] [IsScalarTower R S A] [IsScalarTower R S B] [FunLike F A B] [NonUnitalAlgHomClass F S A B] (φ : F) (a : A) : quasispectrum R (φ a) ⊆ quasispectrum R a

A version of NonUnitalAlgHom.quasispectrum_apply_subset which allows for quasispectrum R, where R is a semiring, but φ must still function over a scalar ring S. In this case, we need S to be explicit. The primary use case is, for instance, R := ℝ≥0 and S := ℝ or S := ℂ.

theorem NonUnitalAlgHom.quasispectrum_apply_subset {F : Type u_3} {R : Type u_4} {A : Type u_5} {B : Type u_6} [CommRing R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] [FunLike F A B] [NonUnitalAlgHomClass F R A B] (φ : F) (a : A) : quasispectrum R (φ a) ⊆ quasispectrum R a

If φ is non-unital algebra homomorphism over a scalar ring R, then quasispectrum R (φ a) ⊆ quasispectrum R a.

@[simp]

theorem quasispectrum.coe_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [Nontrivial R] (a : A) : ↑0 = 0

theorem quasispectrum.mem_of_not_quasiregular {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] (a : A) {r : Rˣ} (hr : ¬IsQuasiregular (-(r⁻¹ • a))) : ↑r ∈ quasispectrum R a

theorem quasispectrum_eq_spectrum_union (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {r : R | ¬IsUnit r}

theorem spectrum_subset_quasispectrum (R : Type u_3) {A : Type u_4} [CommSemiring R] [Ring A] [Algebra R A] (a : A) : spectrum R a ⊆ quasispectrum R a

theorem quasispectrum_eq_spectrum_union_zero (R : Type u_3) {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {0}

theorem mem_quasispectrum_iff {R : Type u_3} {A : Type u_4} [Semifield R] [Ring A] [Algebra R A] {a : A} {x : R} : x ∈ quasispectrum R a ↔ x = 0 ∨ x ∈ spectrum R a

theorem Unitization.isQuasiregular_inr_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : IsQuasiregular ↑a ↔ IsQuasiregular a

theorem Unitization.zero_mem_spectrum_inr (R : Type u_3) (S : Type u_4) {A : Type u_5} [CommSemiring R] [CommRing S] [Nontrivial S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : 0 ∈ spectrum R ↑a

theorem Unitization.mem_spectrum_inr_of_not_isUnit {R : Type u_3} {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) (r : R) (hr : ¬IsUnit r) : r ∈ spectrum R ↑a

theorem Unitization.quasispectrum_eq_spectrum_inr (R : Type u_3) {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a : A) : quasispectrum R a = spectrum R ↑a

theorem Unitization.quasispectrum_eq_spectrum_inr' (R : Type u_3) (S : Type u_4) {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : quasispectrum R a = spectrum R ↑a

theorem Unitization.quasispectrum_inr_eq (R : Type u_3) (S : Type u_4) {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) : quasispectrum R ↑a = quasispectrum R a

theorem quasispectrum.mul_comm {R : Type u_3} {A : Type u_4} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (a b : A) : quasispectrum R (a * b) = quasispectrum R (b * a)

class NonnegSpectrumClass (𝕜 : Type u_3) (A : Type u_4) [CommSemiring 𝕜] [PartialOrder 𝕜] [NonUnitalRing A] [PartialOrder A] [Module 𝕜 A] : Prop

A class for 𝕜-algebras with a partial order where the ordering is compatible with the (quasi)spectrum.

• quasispectrum_nonneg_of_nonneg (a : A) : 0 ≤ a → ∀ x ∈ quasispectrum 𝕜 a, 0 ≤ x

theorem NonnegSpectrumClass.iff_spectrum_nonneg {𝕜 : Type u_3} {A : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] : NonnegSpectrumClass 𝕜 A ↔ ∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x

theorem NonnegSpectrumClass.of_spectrum_nonneg {𝕜 : Type u_3} {A : Type u_4} [Semifield 𝕜] [LinearOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] : (∀ (a : A), 0 ≤ a → ∀ x ∈ spectrum 𝕜 a, 0 ≤ x) → NonnegSpectrumClass 𝕜 A

Alias of the reverse direction of NonnegSpectrumClass.iff_spectrum_nonneg.

theorem spectrum_nonneg_of_nonneg {𝕜 : Type u_3} {A : Type u_4} [CommSemiring 𝕜] [PartialOrder 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄ (ha : 0 ≤ a) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) : 0 ≤ x

Restriction of the spectrum

structure QuasispectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] (a : A) (f : S → R) : Prop

Given an element a : A of an S-algebra, where S is itself an R-algebra, we say that the spectrum of a restricts via a function f : S → R if f is a left inverse of algebraMap R S, and f is a right inverse of algebraMap R S on spectrum S a.

For example, when f = Complex.re (so S := ℂ and R := ℝ), SpectrumRestricts a f means that the ℂ-spectrum of a is contained within ℝ. This arises naturally when a is selfadjoint and A is a C⋆-algebra.

This is the property allows us to restrict a continuous functional calculus over S to a continuous functional calculus over R.

• rightInvOn : Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a)

  f is a right inverse of algebraMap R S when restricted to quasispectrum S a.

• left_inv : Function.LeftInverse f ⇑(algebraMap R S)

  f is a left inverse of algebraMap R S.

theorem quasispectrumRestricts_iff {R : Type u_3} {S : Type u_4} {A : Type u_5} [CommSemiring R] [CommSemiring S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] (a : A) (f : S → R) : QuasispectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)

@[simp]

theorem quasispectrum.algebraMap_mem_iff (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

theorem quasispectrum.algebraMap_mem (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} : r ∈ quasispectrum R a → (algebraMap R S) r ∈ quasispectrum S a

Alias of the reverse direction of quasispectrum.algebraMap_mem_iff.

theorem quasispectrum.of_algebraMap_mem (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} {r : R} : (algebraMap R S) r ∈ quasispectrum S a → r ∈ quasispectrum R a

Alias of the forward direction of quasispectrum.algebraMap_mem_iff.

@[simp]

theorem quasispectrum.preimage_algebraMap (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] {a : A} : ⇑(algebraMap R S) ⁻¹' quasispectrum S a = quasispectrum R a

theorem QuasispectrumRestricts.map_zero {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} (h : QuasispectrumRestricts a f) : f 0 = 0

theorem QuasispectrumRestricts.of_subset_range_algebraMap {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} (hf : Function.LeftInverse f ⇑(algebraMap R S)) (h : quasispectrum S a ⊆ Set.range ⇑(algebraMap R S)) : QuasispectrumRestricts a f

theorem QuasispectrumRestricts.of_quasispectrum_eq {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a b : A} {f : S → R} (ha : QuasispectrumRestricts a f) (h : quasispectrum S a = quasispectrum S b) : QuasispectrumRestricts b f

theorem QuasispectrumRestricts.mul_comm_iff {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] [IsScalarTower S A A] [SMulCommClass S A A] {f : S → R} {a b : A} : QuasispectrumRestricts (a * b) f ↔ QuasispectrumRestricts (b * a) f

theorem QuasispectrumRestricts.mul_comm {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] [IsScalarTower S A A] [SMulCommClass S A A] {f : S → R} {a b : A} : QuasispectrumRestricts (a * b) f → QuasispectrumRestricts (b * a) f

Alias of the forward direction of QuasispectrumRestricts.mul_comm_iff.

theorem QuasispectrumRestricts.algebraMap_image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) : ⇑(algebraMap R S) '' quasispectrum R a = quasispectrum S a

theorem QuasispectrumRestricts.image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) : f '' quasispectrum S a = quasispectrum R a

theorem QuasispectrumRestricts.apply_mem {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) {s : S} (hs : s ∈ quasispectrum S a) : f s ∈ quasispectrum R a

theorem QuasispectrumRestricts.subset_preimage {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Module R A] [Module S A] [Algebra R S] {a : A} {f : S → R} [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] (h : QuasispectrumRestricts a f) : quasispectrum S a ⊆ f ⁻¹' quasispectrum R a

theorem QuasispectrumRestricts.comp {R₁ : Type u_6} {R₂ : Type u_7} {R₃ : Type u_8} {A : Type u_9} [Semifield R₁] [Field R₂] [Field R₃] [NonUnitalRing A] [Module R₁ A] [Module R₂ A] [Module R₃ A] [Algebra R₁ R₂] [Algebra R₂ R₃] [Algebra R₁ R₃] [IsScalarTower R₁ R₂ R₃] [IsScalarTower R₂ R₃ A] [IsScalarTower R₃ A A] [SMulCommClass R₃ A A] {a : A} {f : R₃ → R₂} {g : R₂ → R₁} {e : R₃ → R₁} (hfge : g ∘ f = e) (hf : QuasispectrumRestricts a f) (hg : QuasispectrumRestricts a g) : QuasispectrumRestricts a e

@[reducible]

def SpectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R A] [Algebra S A] [Algebra R S] (a : A) (f : S → R) : Prop

A (reducible) alias of QuasispectrumRestricts which enforces stronger type class assumptions on the types involved, as it's really intended for the spectrum. The separate definition also allows for dot notation.

theorem SpectrumRestricts.rightInvOn {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (h : SpectrumRestricts a f) : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)

theorem SpectrumRestricts.of_rightInvOn {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (h₁ : Function.LeftInverse f ⇑(algebraMap R S)) (h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)) : SpectrumRestricts a f

theorem spectrumRestricts_iff {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} : SpectrumRestricts a f ↔ Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)

theorem SpectrumRestricts.of_subset_range_algebraMap {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} (hf : Function.LeftInverse f ⇑(algebraMap R S)) (h : spectrum S a ⊆ Set.range ⇑(algebraMap R S)) : SpectrumRestricts a f

theorem SpectrumRestricts.of_spectrum_eq {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a b : A} {f : S → R} (ha : SpectrumRestricts a f) (h : spectrum S a = spectrum S b) : SpectrumRestricts b f

theorem SpectrumRestricts.mul_comm_iff {R : Type u_6} {S : Type u_7} {A : Type u_8} [Semifield R] [Field S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a b : A} {f : S → R} : SpectrumRestricts (a * b) f ↔ SpectrumRestricts (b * a) f

theorem SpectrumRestricts.mul_comm {R : Type u_6} {S : Type u_7} {A : Type u_8} [Semifield R] [Field S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a b : A} {f : S → R} : SpectrumRestricts (a * b) f → SpectrumRestricts (b * a) f

Alias of the forward direction of SpectrumRestricts.mul_comm_iff.

theorem SpectrumRestricts.algebraMap_image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : ⇑(algebraMap R S) '' spectrum R a = spectrum S a

theorem SpectrumRestricts.image {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : f '' spectrum S a = spectrum R a

theorem SpectrumRestricts.apply_mem {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) {s : S} (hs : s ∈ spectrum S a) : f s ∈ spectrum R a

theorem SpectrumRestricts.subset_preimage {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} [IsScalarTower R S A] (h : SpectrumRestricts a f) : spectrum S a ⊆ f ⁻¹' spectrum R a

theorem quasispectrumRestricts_iff_spectrumRestricts_inr (S : Type u_3) {R : Type u_4} {A : Type u_5} [Semifield R] [Field S] [NonUnitalRing A] [Algebra R S] [Module R A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [IsScalarTower R S A] {a : A} {f : S → R} : QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

theorem quasispectrumRestricts_iff_spectrumRestricts_inr' {R : Type u_3} {S' : Type u_4} {A : Type u_5} (S : Type u_6) [Semifield R] [Semifield S'] [Field S] [NonUnitalRing A] [Module R A] [Module S' A] [Module S A] [IsScalarTower S A A] [SMulCommClass S A A] [Algebra R S'] [Algebra S' S] [Algebra R S] [IsScalarTower S' S A] [IsScalarTower R S A] {a : A} {f : S' → R} : QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f

The difference from quasispectrumRestricts_iff_spectrumRestricts_inr is that the Unitization may be taken with respect to a different scalar field.

theorem quasispectrumRestricts_iff_spectrumRestricts {R : Type u_3} {S : Type u_4} {A : Type u_5} [Semifield R] [Semifield S] [Ring A] [Algebra R S] [Algebra R A] [Algebra S A] {a : A} {f : S → R} : QuasispectrumRestricts a f ↔ SpectrumRestricts a f