Spectrum and quasispectrum of products

This file contains results regarding the spectra and quasispectra of (indexed) products of elements of a (non-unital) ring. The main result is that the (quasi)spectrum of a product is the union of the (quasi)spectra.

Main declarations

• Pi.spectrum_eq: spectrum R a = ⋃ i, spectrum R (a i) for a : ∀ i, κ i
• Prod.spectrum_eq: spectrum R ⟨a, b⟩ = spectrum R a ∪ spectrum R b
• Pi.quasispectrum_eq: quasispectrum R a = ⋃ i, quasispectrum R (a i) for a : ∀ i, κ i
• Prod.quasispectrum_eq: quasispectrum R ⟨a, b⟩ = quasispectrum R a ∪ quasispectrum R b

TODO

• Apply these results to block matrices.

def PreQuasiregular.toPi {ι : Type u_1} (κ : ι → Type u_5) [(i : ι) → NonUnitalSemiring (κ i)] : PreQuasiregular ((i : ι) → κ i) ≃* ((i : ι) → PreQuasiregular (κ i))

The equivalence between pre-quasiregular elements of an indexed product and the indexed product of pre-quasiregular elements.

Equations

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

def PreQuasiregular.toProd (A : Type u_2) (B : Type u_3) [NonUnitalSemiring A] [NonUnitalSemiring B] : PreQuasiregular (A × B) ≃* PreQuasiregular A × PreQuasiregular B

The equivalence between pre-quasiregular elements of a product and the product of pre-quasiregular elements.

Equations

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

theorem isQuasiregular_pi_iff {ι : Type u_1} {κ : ι → Type u_5} [(i : ι) → NonUnitalSemiring (κ i)] (x : (i : ι) → κ i) : IsQuasiregular x ↔ ∀ (i : ι), IsQuasiregular (x i)

theorem isQuasiregular_prod_iff {A : Type u_2} {B : Type u_3} [NonUnitalSemiring A] [NonUnitalSemiring B] (a : A) (b : B) : IsQuasiregular (a, b) ↔ IsQuasiregular a ∧ IsQuasiregular b

theorem quasispectrum.mem_iff_of_isUnit {A : Type u_2} {R : Type u_4} [CommSemiring R] [NonUnitalRing A] [Module R A] {a : A} {r : R} (hr : IsUnit r) : r ∈ quasispectrum R a ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • a))

theorem Pi.spectrum_eq {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [CommSemiring R] [(i : ι) → Ring (κ i)] [(i : ι) → Algebra R (κ i)] (a : (i : ι) → κ i) : spectrum R a = ⋃ (i : ι), spectrum R (a i)

theorem Prod.spectrum_eq {A : Type u_2} {B : Type u_3} {R : Type u_4} [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (a : A) (b : B) : spectrum R (a, b) = spectrum R a ∪ spectrum R b

theorem Pi.quasispectrum_eq {ι : Type u_1} {R : Type u_4} {κ : ι → Type u_5} [Nonempty ι] [CommSemiring R] [(i : ι) → NonUnitalRing (κ i)] [(i : ι) → Module R (κ i)] (a : (i : ι) → κ i) : quasispectrum R a = ⋃ (i : ι), quasispectrum R (a i)

theorem Prod.quasispectrum_eq {A : Type u_2} {B : Type u_3} {R : Type u_4} [CommSemiring R] [NonUnitalRing A] [NonUnitalRing B] [Module R A] [Module R B] (a : A) (b : B) : quasispectrum R (a, b) = quasispectrum R a ∪ quasispectrum R b