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 wrappingR
that inherits a distinctMonoid
instance whenR
is a non-unital semiring.Unitization.unitsFstOne
: the subgroup with carrier{ x : (Unitization R A)ˣ | x.fst = 1 }
.unitsFstOne_mulEquiv_quasiregular
: the group isomorphism betweenUnitization.unitsFstOne
and the units ofPreQuasiregular
(i.e., the quasiregular elements) which sends(1, x) ↦ x
.IsQuasiregular x
: the proposition thatx : R
is a unit with respect to the monoid structure onPreQuasiregular R
, i.e., there is someu : (PreQuasiregular R)ˣ
such thatu.val
is identified withx
(via the natural equivalence betweenR
andPreQuasiregular R
).quasispectrum R a
: in an algebra over the semifieldR
, this is the set{r : R | (hr : IsUnit r) → ¬ IsQuasiregular (-(hr.unit⁻¹ • a))}
, which should be thought of as a version of thespectrum
which is applicable in non-unital algebras.
Main theorems #
isQuasiregular_iff_isUnit
: in a unital ring,x
is quasiregular if and only if1 + x
is a unit.quasispectrum_eq_spectrum_union_zero
: in a unital algebraA
over a semifieldR
, the quasispectrum ofa : A
is thespectrum
with zero added.Unitization.isQuasiregular_inr_iff
:a : A
is quasiregular if and only if it is quasiregular inUnitization R A
(via the coercionUnitization.inr
).Unitization.quasispectrum_eq_spectrum_inr
: the quasispectrum ofa
in a non-unitalR
-algebraA
is precisely the spectrum ofa
in the unitization. inUnitization R A
(via the coercionUnitization.inr
).
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
The identity map between R
and PreQuasiregular R
.
Equations
- PreQuasiregular.equiv = { toFun := PreQuasiregular.mk, invFun := PreQuasiregular.val, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- PreQuasiregular.instOne = { one := PreQuasiregular.equiv 0 }
Equations
- PreQuasiregular.instMul = { mul := fun (x y : PreQuasiregular R) => { val := y.val + x.val + x.val * y.val } }
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
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
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
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
Equations
- quasispectrum.instZero R a = { zero := ⟨0, ⋯⟩ }
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 := ℂ
.
If φ
is non-unital algebra homomorphism over a scalar ring R
, then
quasispectrum R (φ a) ⊆ quasispectrum R a
.
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
Alias of the reverse direction of NonnegSpectrumClass.iff_spectrum_nonneg
.
Restriction of the spectrum #
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 ofalgebraMap R S
when restricted toquasispectrum S a
. - left_inv : Function.LeftInverse f ⇑(algebraMap R S)
f
is a left inverse ofalgebraMap R S
.
Instances For
f
is a right inverse of algebraMap R S
when restricted to quasispectrum S a
.
f
is a left inverse of algebraMap R S
.
Alias of the reverse direction of quasispectrum.algebraMap_mem_iff
.
Alias of the forward direction of quasispectrum.algebraMap_mem_iff
.
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