TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Polynomial spectral mapping

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $A$ be a unital complex Banach algebra, let $a \in A$ , and let $p \in C [z]$ be a complex polynomial with constant term $c_{0}$ and degree at most $n$ . Form $p (a) : = \sum_{k = 0}^{n} c_{k} a^{k} \in A$ , with $a^{0} : = 1$ . Then

$σ_{A} (p (a)) = p (σ_{A} (a)) = {p (λ) : λ \in σ_{A} (a)},$

where spectra are taken in the ambient algebra $A$ (Spectrum and resolvent set in a Banach algebra). The identity holds for constant polynomials as well: if $p \equiv c$ then $p (a) = c 1$ and both sides equal ${c}$ .

Facts & Assumptions

Given: The Axiom of Choice, a unital complex Banach algebra $A$ , an element $a \in A$ , and a complex polynomial $p$ ; write $p (a) = \sum_{k} c_{k} a^{k}$ , a finite sum of scalar multiples of powers of $a$ .

[L1]

The algebra $A$ is associative, the multiplication is bilinear and $1 u = u 1 = u$ ; every polynomial in $a$ commutes with $a$ , and powers of $a$ satisfy the usual index laws (Unital Banach algebra).

[L2]

For $u \in A$ the element $z 1 - u$ is invertible exactly when $z \in ρ_{A} (u)$ , and invertibility is a two-sided condition; commuting invertible elements have commuting inverses (Spectrum and resolvent set in a Banach algebra, Invertible element and general linear group of a Banach algebra).

[L3]

If $u, v \in A$ commute and $u v$ is invertible, then $u$ and $v$ are invertible: with $w : = (u v)^{- 1}$ one has $u (v w) = u v w = 1$ and $(v w) u = v w u = v u w = u v w = 1$ , so $u^{- 1} = v w$ ; symmetrically $v^{- 1} = w u$ . [L1, L2, algebra]

[L4]

Every nonconstant complex polynomial of degree $d$ has a factorisation $q (z) = c \prod_{j = 1}^{d} (z - λ_{j})$ with $c \neq 0$ and $λ_{j} \in C$ the roots of $q$ (Fundamental theorem of algebra by Liouville's theorem).

[L5]

Under the Axiom of Choice, the spectrum of every element of a nonzero unital complex Banach algebra is nonempty (Spectrum is nonempty compact and norm bounded).

Proof

technique · direct

1.1

Constant case: if $p \equiv c$ then $p (a) = c 1$ and, for $z \in C$ , the element $z 1 - c 1 = (z - c) 1$ is invertible exactly when $z \neq c$ — its inverse is then $(z - c)^{- 1} 1$ — while at $z = c$ it is $0$ , which is not invertible in a nonzero algebra. Hence $σ_{A} (c 1) = {c}$ ; and $σ_{A} (a)$ is nonempty by [L5], so $p (σ_{A} (a)) = {c}$ as well.

L1L2L5algebra

1.2

Nonconstant case, factor step: for $λ \in C$ the polynomial $q (z) : = p (z) - p (λ)$ vanishes at $λ$ , so $q (z) = (z - λ) r (z)$ for a polynomial $r$ of degree $\deg p - 1$ ; evaluating at $a$ gives $p (a) - p (λ) 1 = (a - λ 1) r (a)$ .

L1algebra

1.3

Root factorisation of the translated polynomial: for $μ \in C$ the polynomial $z \mapsto p (z) - μ$ has degree $\deg p \geq 1$ and a leading coefficient $c_{\deg p} \neq 0$ , so by [L4] there are $λ_{1}, \dots, λ_{d} \in C$ with $p (z) - μ = c_{\deg p} \prod_{j = 1}^{d} (z - λ_{j})$ ; evaluating at $a$ gives $p (a) - μ 1 = c_{\deg p} \prod_{j = 1}^{d} (a - λ_{j} 1)$ , a product of commuting elements.

L4L1algebra

2.1

Forward inclusion: if $μ \in σ_{A} (p (a))$ then $μ \in p (σ_{A} (a))$ . Indeed, suppose $p (z) - μ$ has no zero in $σ_{A} (a)$ ; by [step 1.3] the roots $λ_{j}$ of $p (z) - μ$ satisfy $p (λ_{j}) = μ$ , so $λ_{j} \notin σ_{A} (a)$ and each $a - λ_{j} 1$ is invertible; the product $p (a) - μ 1 = c_{\deg p} \prod_{j} (a - λ_{j} 1)$ of commuting invertible elements is invertible, so $μ \notin σ_{A} (p (a))$ .

step 1.3L2algebra

2.2

Reverse inclusion: if $λ \in σ_{A} (a)$ then $p (λ) \in σ_{A} (p (a))$ . For if $p (a) - p (λ) 1$ were invertible, then by [step 1.2] the commuting product $(a - λ 1) r (a)$ would be invertible, so [L3] would make $a - λ 1$ invertible, contradicting $λ \in σ_{A} (a)$ .

step 1.2L3L2

3.1

Combining [step 2.1] and [step 2.2] with [step 1.1] gives $σ_{A} (p (a)) = p (σ_{A} (a))$ in the nonconstant case and $σ_{A} (c 1) = {c} = p (σ_{A} (a))$ in the constant case, which is the assertion.

step 1.1step 2.1step 2.2∎

Remarks

Where the fundamental theorem of algebra is used. The forward inclusion [step 2.1] needs the existence of all roots of $p (z) - μ$ , which is Fundamental theorem of algebra by Liouville's theorem. The reverse inclusion needs only polynomial division by the known linear factor $z - λ$ .
The statement is about the ambient algebra. Both spectra in the theorem are computed in the same unital Banach algebra $A$ ; the identity can fail for spectra taken in different algebras, since spectra may shrink in a larger algebra (cex-spectrum-can-shrink-in-a-larger-banach-algebra).
Reading order. The example items named by ID above are homed on later pages of the plan, so they are named rather than hyperlinked: a body link to later material must be declared as a forward reference, and Step-5b closure removes every such declaration. Rehoming those items to an earlier page (an owner-only reading-order change) would make the citations backward and restore the links.

Depends on

Used by

Polynomial calculus is isometric for self adjoint operators Lemma
Spectral radius formula Theorem

Dependency tree · two levels

20 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Theo Bühler and Dietmar A. Salamon, Functional Analysis — §5.2.1 and the Jordan-form computation of spectra, printed pp. 219–222 (standard reference, not scraped)
Vahid Shirbisheh, Lectures on C-star Algebras, v2 — §2.3, printed pp. 30–33 (standard reference, not scraped)