Mathlib.Algebra.Algebra.Spectrum._auxLemma.2
theorem Mathlib.Algebra.Algebra.Spectrum._auxLemma.2 :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
(r ∈ spectrum R a) = ¬IsUnit ((algebraMap R A) r - a)
The theorem `Mathlib.Algebra.Algebra.Spectrum._auxLemma.2` states that for any commutative semiring `R`, any ring `A` that is also an `R`-algebra, and any elements `r` of `R` and `a` of `A`, `r` is in the spectrum of `a` if and only if the difference between the image of `r` under the algebra structure map and `a` itself is not a unit in the algebra `A`. In the context of the algebra, a unit is an element that has a multiplicative inverse. Essentially, it details the relationship between the spectrum of an element of an `R`-algebra and the set of non-unit elements in the algebra.
More concisely: For any commutative semiring R, an R-algebra A, and elements r in R and a in A, r is in the spectrum of a if and only if r \* a \*-1 is not defined in A.
|
spectrum.isUnit_of_zero_not_mem
theorem spectrum.isUnit_of_zero_not_mem :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
0 ∉ spectrum R a → IsUnit a
The theorem `spectrum.isUnit_of_zero_not_mem` states that for any given commutative semiring `R`, a ring `A`, and an `R`-algebra structure on `A`, if the number zero is not an element of the spectrum of any element `a : A`, then `a` is a unit in the ring `A`. In other words, if for every ring element `a`, zero does not belong to the set of scalars `r : R` for which `r•1 - a` is not a unit of the algebra `A`, then `a` itself has a multiplicative inverse in `A`.
More concisely: If in a commutative semiring `R` and an `R`-algebra `A`, the zero element is not in the spectrum of any element `a` in `A`, then `a` is a unit in `A`.
|
spectrum.zero_not_mem
theorem spectrum.zero_not_mem :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
IsUnit a → 0 ∉ spectrum R a
This theorem states that for any commutative semiring `R`, ring `A` and an `R`-algebra structure on `A`, if an element `a` of `A` is a unit, then zero is not an element of the spectrum of `a`. In other words, if we have an element `a` in `A` that has a two-sided inverse, then zero doesn't belong to the set of `r` in `R` for which `r•1 - a` is not a unit of the algebra `A`. This is the reverse direction of the theorem `spectrum.zero_not_mem_iff`.
More concisely: If `a` is a unit in the `R-`algebra `A` over the commutative semiring `R`, then zero is not in the spectrum of `a`.
|
SpectrumRestricts.algebraMap_image
theorem SpectrumRestricts.algebraMap_image :
∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Ring A]
[inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {a : A}
{f : S → R}, SpectrumRestricts a f → ⇑(algebraMap R S) '' spectrum R a = spectrum S a
The theorem `SpectrumRestricts.algebraMap_image` asserts that for any commutative semirings `R` and `S`, a ring `A`, algebra structures from `R` to `S`, `R` to `A`, and `S` to `A`, a scalar tower structure for `R`, `S`, and `A`, a given element `a` of `A`, and a function from `S` to `R` that restricts the spectrum of `a`, the image of the spectrum of `a` (from the algebra of `R` to `A`) under the algebra mapping from `R` to `S` is equal to the spectrum of `a` in the algebra of `S` to `A`. In mathematical terms, if `f` restricts the spectrum of `a`, then the image of the spectrum of `a` under the algebra map `R → S` is exactly the spectrum of `a` with respect to `S`.
More concisely: For any commutative semirings R, S, a ring A, algebra structures and scalar towers, if an element a of A has spectrum s in the algebra of R to A, and the function restricting the spectrum of a to S is f, then the image of s under the algebra map R → S equals the spectrum of a in the algebra of S to A.
|
spectrum.not_isUnit_of_zero_mem
theorem spectrum.not_isUnit_of_zero_mem :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
0 ∈ spectrum R a → ¬IsUnit a
The theorem `spectrum.not_isUnit_of_zero_mem` states that for any commutative semiring `R`, any `R`-algebra `A`, and any element `a` of `A`, if zero is in the spectrum of `a`, then `a` is not a unit in `A`. In other words, if the scalar multiple of one minus `a` fails to have a multiplicative inverse (i.e., zero is in the spectrum of `a`), then `a` itself also fails to have a multiplicative inverse (i.e., `a` is not a unit).
More concisely: If an element `a` of a commutative `R`-algebra `A` has zero in its spectrum, then `a` is not a unit in `A`.
|
spectrum.scalar_eq
theorem spectrum.scalar_eq :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : Nontrivial A]
(k : 𝕜), spectrum 𝕜 ((algebraMap 𝕜 A) k) = {k}
The theorem `spectrum.scalar_eq` states that for any field `𝕜`, a ring `A`, and given an algebra structure on `A` over `𝕜`, and assuming `A` is nontrivial (i.e., `A` contains at least two distinct elements), then the spectrum of the image under the algebra map of any scalar `k` from `𝕜` is simply the singleton set containing `k`. In other words, the only element in the field `𝕜` for which `k•1 - (algebraMap 𝕜 A k)` is not a unit in the algebra `A`, is `k` itself.
More concisely: For any field `𝕜`, ring `A` with an algebra structure over `𝕜`, and non-trivial `A`, the spectrum of the algebra map of any scalar `k` from `𝕜` is a singleton set containing `k`.
|
spectrum.mem_iff
theorem spectrum.mem_iff :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
r ∈ spectrum R a ↔ ¬IsUnit ((algebraMap R A) r - a)
This theorem states that for any commutative semiring `R`, any ring `A`, and an algebra structure over `R` and `A`, for any elements `r` of `R` and `a` of `A`, `r` is in the spectrum of `a` if and only if the difference between the image of `r` under the algebra map from `R` to `A` and `a` is not a unit in the algebra. In other words, it describes a property of a ring element's spectrum in terms of unit elements. The spectrum here refers to the set of elements for which subtracting the given element gives a non-unit element in the algebra.
More concisely: For any commutative semiring `R`, ring `A`, and algebra structure over `R` and `A`, an element `r` in `R` is in the spectrum of an element `a` in `A` if and only if the image of `r` under the algebra map from `R` to `A` minus `a` is not a unit in `A`.
|
Mathlib.Algebra.Algebra.Spectrum._auxLemma.5
theorem Mathlib.Algebra.Algebra.Spectrum._auxLemma.5 :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
(r ∈ resolventSet R a) = IsUnit ((algebraMap R A) r - a)
This theorem states that for any commutative semi-ring `R`, any ring `A` where `A` is an `R`-algebra, any element `r` from `R` and any element `a` from `A`, `r` is in the resolvent set of `a` if and only if the result of subtracting `a` from the image of `r` under the algebra map (which maps `R` to `A`) is a unit in the algebra `A`. In other words, `r` is in the resolvent set of `a` exactly when `r•1 - a` is invertible in the algebra `A`. The resolvent set is thus characterized by invertibility under subtraction.
More concisely: For any commutative semi-ring `R`, `R-`algebra `A`, `r` in `R`, and `a` in `A`, `r` is in the resolvent set of `a` if and only if `r•1 - a` is invertible in `A`.
|
spectrum.zero_mem
theorem spectrum.zero_mem :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
¬IsUnit a → 0 ∈ spectrum R a
This theorem is an alias of the reverse direction of `spectrum.zero_mem_iff`. It states that for any commutative semiring `R`, any `R`-algebra `A`, and any element `a` of `A`, if `a` is not a unit of the algebra `A`, then the number zero is in the spectrum of `a`. The spectrum of `a` is the set of elements `r` of `R` for which `r•1 - a` is not a unit of the algebra `A`.
More concisely: If `a` is a non-unit in the `R`-algebra `A` over the commutative semiring `R`, then zero belongs to the spectrum of `a`.
|
AlgHom.apply_mem_spectrum
theorem AlgHom.apply_mem_spectrum :
∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
[inst_3 : FunLike F A R] [inst_4 : AlgHomClass F R A R] [inst_5 : Nontrivial R] (φ : F) (a : A),
φ a ∈ spectrum R a
This theorem, `AlgHom.apply_mem_spectrum`, asserts that for any commutative ring `R`, ring `A`, algebra structure on `A` over `R`, function of type `F` that behaves like a function from `A` to `R` (denoted by the `FunLike` typeclass), and given the `AlgHomClass` typeclass which represents an algebra homomorphism of `F` from `R` to `A` to `R`, then for any algebra homomorphism `φ` of type `F` and for any element `a` of `A`, the image of `a` under `φ` is in the spectrum of `a` in `R`.
In mathematical terms, if `φ: A → R` is an algebra homomorphism, and `a ∈ A`, then `φ(a)` lies in the spectrum of `a`. The spectrum of `a` is the set of all `r` in `R` such that `r•1 - a` is not a unit in `A`.
More concisely: For any commutative ring `R`, ring `A`, algebra structure on `A` over `R`, `FunLike` function `F` from `A` to `R`, and given an algebra homomorphism `φ: A → R` of type `AlgHomClass R A F`, the image of any element `a` in `A` under `φ` lies in the spectrum of `a` in `R`.
|
spectrum.isUnit_resolvent
theorem spectrum.isUnit_resolvent :
∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
r ∈ resolventSet R a ↔ IsUnit (resolvent a r)
This theorem states that for any commutative semiring `R`, ring `A`, and algebra of `R` over `A`, and for any elements `r` of `R` and `a` of `A`, `r` belongs to the resolvent set of `a` if and only if the resolvent of `a` at `r` is a unit. In other words, a scalar `r` is in the resolvent set of an algebra element `a` exactly when the algebraic object formed by subtracting `a` from the multiple of the unit element by `r` (i.e., `r•1 - a`) has a multiplicative inverse in the algebra `A`.
More concisely: For a commutative semiring `R`, ring `A`, and algebra of `R` over `A`, an element `r` in `R` belongs to the resolvent set of an element `a` in `A` if and only if `r•1 - a` has a multiplicative inverse in `A`.
|
spectrum.singleton_add_eq
theorem spectrum.singleton_add_eq :
∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
{r} + spectrum R a = spectrum R ((algebraMap R A) r + a)
This theorem states that for any commutative ring `R`, any `R`-algebra `A`, any element `a` from `A`, and any element `r` from `R`, the set obtained by adding the singleton set `{r}` to the spectrum of `a` in `R` is equal to the spectrum of the sum of `a` and the image of `r` under the algebraic embedding from `R` to `A`. In other words, shifting the spectrum by a fixed element in the base ring corresponds to adding that element's image under the algebraic embedding to the original element in the algebra.
More concisely: For any commutative ring `R`, `R`-algebra `A`, element `a` in `A`, and element `r` in `R`, the spectrum of `a + r • a` in `A` equals the set obtained by adding `{r}` to the spectrum of `a` in `R`.
|
spectrum.zero_eq
theorem spectrum.zero_eq :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : Nontrivial A],
spectrum 𝕜 0 = {0}
This theorem states that for any field '𝕜' and ring 'A' that also has a '𝕜'-algebra structure and a nontriviality condition, the spectrum of the zero element in 'A' is precisely the set containing only the zero element of '𝕜'. In other words, the only element 'r' from '𝕜' which makes 'r•1 - 0' non-invertible in the algebra 'A' is the zero element of '𝕜'. The nontriviality condition on 'A' is necessary to prevent the zero element in 'A' from being invertible.
More concisely: For any field '𝕜' and '𝕜'-algebra 'A' satisfying a nontriviality condition, the spectrum of the zero element in 'A' equals {0}. Hence, only the zero element of '𝕜' makes the corresponding multiplicative identity in 'A' non-invertible.
|
spectrum.zero_mem_iff
theorem spectrum.zero_mem_iff :
∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {a : A},
0 ∈ spectrum R a ↔ ¬IsUnit a
The theorem `spectrum.zero_mem_iff` states that for any commutative semiring `R` and any `R`-algebra `A`, zero is in the spectrum of an element `a` of `A` if and only if `a` is not a unit (i.e., it does not have a two-sided inverse) in the algebra `A`. In mathematical terms, 0 belongs to the set of `r` in `R` such that `r•1 - a` is not a unit in the algebra `A`, if and only if `a` itself is not a unit.
More concisely: The theorem `spectrum.zero_mem_iff` asserts that an element `a` of an `R`-algebra `A` over a commutative semiring `R` is not a unit if and only if zero is in the spectrum of `a` in `A`.
|
spectrum.smul_eq_smul
theorem spectrum.smul_eq_smul :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : Nontrivial A]
(k : 𝕜) (a : A), (spectrum 𝕜 a).Nonempty → spectrum 𝕜 (k • a) = k • spectrum 𝕜 a
This theorem, `spectrum.smul_eq_smul`, states that for any field `𝕜`, ring `A`, algebra structure on `A` over `𝕜`, a nontrivial ring `A`, a scalar `k` in `𝕜`, and an element `a` of `A`, if the spectrum of `a` with respect to `𝕜` is nonempty, then the spectrum of the scalar multiplication `k • a` is equal to the scalar multiplication `k` of the spectrum of `a`. The condition that the spectrum of `a` is nonempty is essential and can't be removed without imposing additional conditions on the algebra `A` and the scalar field `𝕜`.
More concisely: If `𝕜` is a field, `A` is a nontrivial `𝕜`-algebra, `k` is an element of `𝕜`, and `a` is an element of `A` with nonempty spectrum, then the spectrum of `k • a` is equal to the scalar multiplication `k` of the spectrum of `a`.
|