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.

@[simp]

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

@[simp]

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

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 := ⋯ }

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

Equations

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

@[simp]

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

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 } }

@[simp]

theorem PreQuasiregular.val_mul {R : Type u_1} [NonUnitalSemiring R] (x : PreQuasiregular R) (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)

Equations

• PreQuasiregular.instMonoid = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

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

Equations

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

@[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 ∈ Unitization.unitsFstOne R A ↔ Unitization.fst ↑x = 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 : ↥(Unitization.unitsFstOne R A)) : Unitization.fst ↑↑x = 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 : ↥(Unitization.unitsFstOne R A)) : Unitization.fst ↑(↑x)⁻¹ = 1

@[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)ˣ) : ↑(↑((MulEquiv.symm (Unitization.unitsFstOne_mulEquiv_quasiregular R)) 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 : ↥(Unitization.unitsFstOne R A)) : ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x)⁻¹ = PreQuasiregular.equiv (Unitization.snd ↑↑x⁻¹)

@[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)ˣ) : ↑↑((MulEquiv.symm (Unitization.unitsFstOne_mulEquiv_quasiregular R)) x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)

@[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 : ↥(Unitization.unitsFstOne R A)) : ↑((Unitization.unitsFstOne_mulEquiv_quasiregular R) x) = PreQuasiregular.equiv (Unitization.snd ↑↑x)

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] : ↥(Unitization.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.

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

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

Equations

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

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

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 := { val := 0, property := ⋯ } }

@[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 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] [Ring A] [Algebra R 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

class NonnegSpectrumClass (𝕜 : Type u_3) (A : Type u_4) [OrderedCommSemiring 𝕜] [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} [LinearOrderedSemifield 𝕜] [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} [LinearOrderedSemifield 𝕜] [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} [OrderedCommSemiring 𝕜] [Ring A] [PartialOrder A] [Algebra 𝕜 A] [NonnegSpectrumClass 𝕜 A] ⦃a : A⦄ (ha : 0 ≤ a) ⦃x : 𝕜⦄ (hx : x ∈ spectrum 𝕜 a) : 0 ≤ x