spectrum.map_pow_of_nonempty
theorem spectrum.map_pow_of_nonempty :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : IsAlgClosed 𝕜]
{a : A}, (spectrum 𝕜 a).Nonempty → ∀ (n : ℕ), spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
The theorem `spectrum.map_pow_of_nonempty` states that for a given field `𝕜`, a ring `A`, and any element `a` from `A`, if the spectrum of `a` with respect to `𝕜` is non-empty, then for any natural number `n`, the spectrum of `a` powered by `n` is equal to the image of the spectrum of `a` under the function that takes each element to its `n`th power. This is a specialization of a more general theorem `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials, and it requires that the given field `𝕜` is algebraically closed.
More concisely: If `𝕜` is an algebraically closed field, and the spectrum of `a` in `A` over `𝕜` is non-empty, then the spectrum of `a^n` in `A` is equal to the set of `𝕜`-valued roots of the polynomial `x -> x^n - a^n`.
|
spectrum.map_polynomial_aeval_of_degree_pos
theorem spectrum.map_polynomial_aeval_of_degree_pos :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : IsAlgClosed 𝕜]
(a : A) (p : Polynomial 𝕜),
0 < p.degree → spectrum 𝕜 ((Polynomial.aeval a) p) = (fun x => Polynomial.eval x p) '' spectrum 𝕜 a
The *spectral mapping theorem* for polynomials in Lean 4 states that for any field `𝕜`, ring `A`, and `𝕜`-algebra structure on `A` with `𝕜` being algebraically closed, given an element `a` of `A` and a polynomial `p` over `𝕜` with positive degree, the spectrum of the result of applying the algebra homomorphism induced by `a` on `p` (i.e., `(Polynomial.aeval a) p`) is equal to the image of the spectrum of `a` under the function that evaluates `p` at each point of the spectrum (i.e., `(fun x => Polynomial.eval x p) '' spectrum 𝕜 a`). Concretely, this theorem connects the spectrum of a polynomial evaluated at an algebra element with the polynomial evaluated at the spectrum of the algebra element, with the condition that the polynomial has a positive degree.
More concisely: For any algebraically closed field `𝕜`, `𝕜`-algebra `A`, and `a` in `A` with positive degree polynomial `p` over `𝕜`, the spectra of `p` evaluated at `a` and `a` evaluated at the spectrum of `p` are equal.
|
spectrum.pow_image_subset
theorem spectrum.pow_image_subset :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (n : ℕ),
(fun x => x ^ n) '' spectrum 𝕜 a ⊆ spectrum 𝕜 (a ^ n)
This theorem states that for any field `𝕜`, ring `A`, and `𝕜`-algebra structure on `A`, any element `a` of `A` and any natural number `n`, the image of the function `x ↦ x^n` applied to the spectrum of `a` is a subset of the spectrum of `a^n`. In other words, if `r` is an element of the spectrum of `a`, then `r^n` is in the spectrum of `a^n`. This is a specialization of the theorem `spectrum.subset_polynomial_aeval` to monic polynomials that are also monomials.
More concisely: For any field `𝕜`, ring `A`, `𝕜`-algebra structure on `A`, element `a` of `A`, and natural number `n`, the spectrum of `a^n` contains the `n`-th power of every element in the spectrum of `a`.
|
spectrum.subset_polynomial_aeval
theorem spectrum.subset_polynomial_aeval :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜),
(fun x => Polynomial.eval x p) '' spectrum 𝕜 a ⊆ spectrum 𝕜 ((Polynomial.aeval a) p)
The theorem `spectrum.subset_polynomial_aeval` states that for any field `𝕜`, ring `A` and algebra `𝕜 A`, for any element `a` from `A` and any polynomial `p` over `𝕜`, the image of the spectrum of `a` under the polynomial evaluation function with polynomial `p` is a subset of the spectrum of the algebra homomorphism from `𝕜[X]` to `A`, sending `X` to `a`, applied to `p`. In other words, for any valuation `x` in the spectrum of `a`, if we evaluate the polynomial `p` at `x`, the result is in the spectrum of the evaluation of polynomial `p` at `a` in the algebra `𝕜 A`. This is a component of the spectral mapping theorem for polynomials and holds for any field, unlike some other parts of the theorem that require the field to be algebraically closed.
More concisely: For any field 𝕜, ring A and algebra 𝕜 A, if a ∈ A and p is a polynomial over 𝕜, then the set of valuations in the spectrum of a that map p to an element in the spectrum of the evaluation homomorphism of p at a is non-empty.
|
spectrum.map_polynomial_aeval_of_nonempty
theorem spectrum.map_polynomial_aeval_of_nonempty :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : IsAlgClosed 𝕜]
(a : A) (p : Polynomial 𝕜),
(spectrum 𝕜 a).Nonempty → spectrum 𝕜 ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum 𝕜 a
This theorem, known as a variant of the spectral mapping theorem, states that for any field `𝕜`, any `𝕜`-algebra `A`, any element `a` of `A`, and any polynomial `p` over `𝕜`, if the spectrum of `a` is nonempty, then the spectrum of `p` evaluated at `a` is the image of evaluating `p` at each element of the spectrum of `a`. Here, evaluation is defined by the unique algebra homomorphism from `𝕜[X]` to `A` that sends `X` to `a`. The field `𝕜` is assumed to be algebraically closed.
The spectrum of `a` is defined as the set of elements in `𝕜` for which `r•1 - a` is not a unit of the algebra `A`.
More concisely: Given a field `𝕜`, an `𝕜`-algebra `A`, an element `a` of `A`, a polynomial `p` over `𝕜`, and an algebraically closed `𝕜`, if `a` has nonempty spectrum, then the set of roots of `p(X)` in `𝕜` is equal to the set of evaluations of `p` at the elements in the spectrum of `a` in `A`.
|
spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
theorem spectrum.nonempty_of_isAlgClosed_of_finiteDimensional :
∀ (𝕜 : Type u) {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : IsAlgClosed 𝕜]
[inst_4 : Nontrivial A] [I : FiniteDimensional 𝕜 A] (a : A), (spectrum 𝕜 a).Nonempty
The theorem states that for every element `a` in a nontrivial finite-dimensional algebra `A` over an algebraically closed field `𝕜`, the spectrum of `a` is non-empty. In mathematical terms, if `𝕜` is an algebraically closed field, `A` is a nontrivial finite-dimensional `𝕜`-algebra, and `a` is an element of `A`, then there exists at least one `𝕜` such that `k•1 - a` is not a unit in `A`. The non-empty spectrum indicates that there is at least one scalar from the base field that, when subtracted from our element scaled by one, doesn't yield an invertible element of the algebra.
More concisely: In an algebraically closed field `𝕜`, every non-invertible element `a` in a finite-dimensional `𝕜`-algebra `A` has a non-zero eigenvalue in `𝕜`, i.e., there exists `k ∈ 𝕜` such that `k•1 - a` is not invertible in `A`.
|
spectrum.map_pow_of_pos
theorem spectrum.map_pow_of_pos :
∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [inst_3 : IsAlgClosed 𝕜]
(a : A) {n : ℕ}, 0 < n → spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
This theorem, named `spectrum.map_pow_of_pos`, is a specialization of another theorem, `spectrum.map_polynomial_aeval_of_nonempty`, and it is provided for convenience. The theorem applies to a field `𝕜`, a ring `A`, and an algebra structure of `𝕜` over `A`. The theorem also assumes that `𝕜` is an algebraically closed field. Given an element `a` of `A` and a natural number `n` greater than zero, this theorem states that the spectrum of `a^n` in `𝕜` is equal to the image of the function `x ↦ x^n` on the spectrum of `a` in `𝕜`. In other words, every element in the spectrum of `a^n` is the n-th power of some element in the spectrum of `a`.
More concisely: The theorem asserts that the spectrum of an algebraic element's n-th power in an algebraically closed field is the set of n-th powers of elements in the spectrum of the element.
|