# 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 `Unitization R A` (via the coercion `Unitization.inr`).

source
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`.

Instances For

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

The identity map between `R` and `PreQuasiregular R`.

Equations

- PreQuasiregular.equiv = { toFun := PreQuasiregular.mk, invFun := PreQuasiregular.val, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem PreQuasiregular.equiv_apply_val {R : Type u_1} (val : R) :
(equiv val).val = val
source
@[simp]
theorem PreQuasiregular.equiv_symm_apply {R : Type u_1} (self : PreQuasiregular R) :
equiv.symm self = self.val
source
instance PreQuasiregular.instOne {R : Type u_1} [NonUnitalSemiring R] :
One (PreQuasiregular R)
Equations

- PreQuasiregular.instOne = { one := PreQuasiregular.equiv 0 }

source
@[simp]
theorem PreQuasiregular.val_one {R : Type u_1} [NonUnitalSemiring R] :
val 1 = 0
source
instance PreQuasiregular.instMul {R : Type u_1} [NonUnitalSemiring R] :
Mul (PreQuasiregular R)
Equations

- PreQuasiregular.instMul = { mul := fun (x y : PreQuasiregular R) => { val := y.val + x.val + x.val * y.val } }

source
@[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
source
instance PreQuasiregular.instMonoid {R : Type u_1} [NonUnitalSemiring R] :
Monoid (PreQuasiregular R)
Equations

- One or more equations did not get rendered due to their size.

source
@[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
source
@[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
source
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`.

Equations

- Unitization.unitsFstOne R A = { carrier := {x : (Unitization R A)ˣ | (↑x).fst = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source
@[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
source
@[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
source
@[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
source
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`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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⁻¹)
source
@[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
source
@[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
source
@[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)
source
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`.

Equations

- IsQuasiregular x = ∃ (u : (PreQuasiregular R)ˣ), PreQuasiregular.equiv.symm ↑u = x

Instances For

source
@[simp]
theorem isQuasiregular_zero :
IsQuasiregular 0
source
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
source
theorem isQuasiregular_iff' {R : Type u_1} [NonUnitalSemiring R] {x : R} :
IsQuasiregular x ↔ IsUnit (PreQuasiregular.equiv x)
source
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)
source
theorem IsQuasiregular.isUnit_one_add {R : Type u_1} [Semiring R] {x : R} (hx : IsQuasiregular x) :
IsUnit (1 + x)
source
theorem isQuasiregular_iff_isUnit {R : Type u_1} [Ring R] {x : R} :
IsQuasiregular x ↔ IsUnit (1 + x)
source
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)
source
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`.

Equations

- quasispectrum R a = {r : R | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))}

Instances For

source
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
source
@[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
source
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
source
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)
Equations

- quasispectrum.instZero R a = { zero := ⟨0, ⋯⟩ }

source
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 := ℂ`.

source
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`.

source
@[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
source
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
source
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}
source
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
source
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}
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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)
source
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

Instances

source
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
source
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`.

source
theorem NonnegSpectrumClass.nonneg_of_mem_quasispectrum {A : Type u_2} [NonUnitalRing A] {𝕜 : Type u_3} [CommSemiring 𝕜] [PartialOrder 𝕜] [PartialOrder A] [Module 𝕜 A] [NonnegSpectrumClass 𝕜 A] {a : A} (ha : 0 ≤ a) {x : 𝕜} (hx : x ∈ quasispectrum 𝕜 a) :
0 ≤ x
source
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 #

source
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`.

Instances For

source
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)
source
@[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
source
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`.

source
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`.

source
@[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
source
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
source
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
source
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
source
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
source
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`.

source
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
source
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
source
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
source
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
source
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
source
@[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.

Equations

- SpectrumRestricts a f = QuasispectrumRestricts a f

Instances For

source
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)
source
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
source
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)
source
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
source
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
source
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
source
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`.

source
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
source
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
source
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
source
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
source
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
source
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.

source
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