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.

Holomorphic spectral mapping and composition

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $A$ be a unital complex Banach algebra and let $a \in A$ . Let $f$ be holomorphic on an open set $U \supseteq σ_{A} (a)$ , so that $f (a)$ is defined (Holomorphic functional calculus). Then:

spectral mapping: $σ_{A} (f (a)) = f (σ_{A} (a)) = {f (λ) : λ \in σ_{A} (a)}$ ;
composition: if $V$ is an open set with $f [U] \subseteq V$ and $g : V \to C$ is holomorphic, then $g (f (a)) = (g \circ f) (a),$ where $(g \circ f) (a)$ is computed from the holomorphic function $g \circ f : U \to C$ by the calculus on $A$ .

Clause 1 includes locally constant functions: if $f$ is constant on a component of $σ_{A} (a)$ its image there is a single point, and no connectedness of $U$ or of $σ_{A} (a)$ is assumed.

Facts & Assumptions

Given: An assumed Axiom of Choice, a unital complex Banach algebra $A$ , an element $a \in A$ , an open $U \supseteq σ_{A} (a)$ , a holomorphic $f : U \to C$ , and for clause 2 an open $V \supseteq f [U]$ with a holomorphic $g : V \to C$ .

[L1]

The calculus $h \mapsto h (a)$ is linear, multiplicative, unital, sends the coordinate function to $a$ and satisfies $h (a)^{- 1} = (1 / h) (a)$ for nowhere vanishing holomorphic $h$ (Holomorphic functional calculus homomorphism, Holomorphic functional calculus).

[L2]

For holomorphic $f$ and fixed $z$ the filled difference quotient $ζ \mapsto g (ζ, z) : = (f (ζ) - f (z)) / (ζ - z)$ for $ζ \neq z$ , extended by $f^{'} (z)$ at $ζ = z$ , is holomorphic in each variable on $U$ ; in particular $h_{λ} (ζ) : = g (ζ, λ)$ is holomorphic on $U$ with $f (ζ) - f (λ) = (ζ - λ) h_{λ} (ζ)$ (The filled difference quotient is holomorphic in each variable separately).

[L3]

If $u, v$ commute in $A$ and $u v$ is invertible then so are $u$ and $v$ : with $w : = (u v)^{- 1}$ one has $u (v w) = 1 = (v w) u$ , and symmetrically for $v$ (Spectrum and resolvent set in a Banach algebra).

[L4]

Nested and encircling cycles exist as in Admissible cycle around a compact plane set: for compact $K$ inside open $W$ there is a cycle with index $1$ on $K$ and $0$ outside $W$ , and two such with disjoint traces and nesting. For a cycle $Γ$ of this kind the set $K_{Γ} : = Γ^{*} \cup {w \in C : n (Γ, w) \neq 0}$ is compact: it is closed and bounded because the index vanishes far from the trace (The index of a cycle is locally constant off its trace and vanishes far from it).

[L5]

Cauchy formula on a cycle: for holomorphic $h$ on open $Ω$ and a cycle $Γ$ with trace in $Ω$ null-homologous in $Ω$ , $n (Γ, p) h (p) = \frac{1}{2 π i} \int_{Γ} h (ζ) / (ζ - p) d ζ$ for $p \in Ω ∖ Γ^{*}$ , and the double integral of a continuous integrand over two such cycles may be iterated in either order (Cauchy's integral formula for a null-homologous cycle, Resolvent identity, the mesh estimate of Banach algebra valued contour integral).

Proof

technique · direct

1.1L2L1algebra

Factorization at a spectral point: for $λ \in σ_{A} (a)$ the function $h_{λ}$ of [L2] is holomorphic on $U$ and $f (z) - f (λ) = (z - λ) h_{λ} (z)$ on $U$ ; applying the calculus and its multiplicative and affine laws [L1] gives $f (a) - f (λ) 1 = (a - λ 1) h_{λ} (a)$ , a product of two commuting elements.

1.2L1algebra

Reverse inclusion: if $μ \notin f (σ_{A} (a))$ then $f (z) - μ \neq 0$ for every $z \in σ_{A} (a)$ , so $1 / (f - μ)$ is holomorphic on some neighbourhood of $σ_{A} (a)$ ; by [L1] applied to the two functions $f - μ$ and $1 / (f - μ)$ , whose product is the constant function $1$ , one has $(f (a) - μ 1) \cdot (1 / (f - μ)) (a) = 1 = (1 / (f - μ)) (a) (f (a) - μ 1)$ , so $μ \notin σ_{A} (f (a))$ .

2.1step 1.1L3

Forward inclusion: let $λ \in σ_{A} (a)$ . If $f (a) - f (λ) 1$ were invertible, then by [step 1.1] the commuting product $(a - λ 1) h_{λ} (a)$ would be invertible, so [L3] would make $a - λ 1$ invertible, contradicting $λ \in σ_{A} (a)$ ; hence $f (λ) \in σ_{A} (f (a))$ .

3.1step 1.2step 2.1algebra

Clause 1 follows from [step 1.2] and [step 2.1]: $f (σ_{A} (a)) \subseteq σ_{A} (f (a)) \subseteq f (σ_{A} (a))$ .

4.1step 3.1L4L1algebra

Setup for clause 2: choose a cycle $β$ with trace in $U ∖ σ_{A} (a)$ and index $1$ on $σ_{A} (a)$ , $0$ outside $U$ , by [L4]; then $K : = K_{β}$ is a compact subset of $U$ containing $σ_{A} (a)$ , and $f [K] \subseteq V$ is compact. Since $σ_{A} (f (a)) = f (σ_{A} (a)) \subseteq f [K]$ by [step 3.1], the calculus applies to $g$ at $f (a)$ .

5.1step 4.1L1L2algebra

The resolvent identity in integral form: for every $z \notin f [K]$ the function $w \mapsto \frac{1}{z - f (w)}$ is holomorphic on a neighbourhood of $σ_{A} (a)$ (namely on $U ∖ f^{- 1} ({z})$ , which contains $K$ and hence $σ_{A} (a)$ ), and $z - f (w) \neq 0$ there; by [L1] applied to $w \mapsto \frac{1}{z - f (w)}$ and the affine function $z - f$ , one has $(z 1 - f (a))^{- 1} = \frac{1}{2 π i} \int_{β} \frac{R (w, a)}{z - f (w)} d w$ : both sides are the calculus of reciprocal functions whose product with $z - f$ is $1$ .

5.2step 4.1L5algebra

Choice of the outer cycle and Cauchy evaluation: apply [L4] to the compact set $f [K]$ inside $V$ , obtaining a cycle $γ$ with index $1$ on $f [K]$ and $0$ outside $V$ ; then for every $w \in β^{*}$ (so $f (w) \in f [K]$ ) the Cauchy formula [L5] applied to $g$ on $V$ along $γ$ gives $\frac{1}{2 π i} \int_{γ} \frac{g (z)}{z - f (w)} d z = n (γ, f (w)) g (f (w)) = g (f (w))$ .

6.1step 5.1step 5.2L5L1

Composition: using the definition of the calculus, [step 5.1] inside the outer integral, and the iterated-integral identity of [L5], $g (f (a)) = \frac{1}{2 π i} \int_{γ} g (z) (z 1 - f (a))^{- 1} d z = (\frac{1}{2 π i})^{2} \int_{γ} \int_{β} \frac{g (z) R (w, a)}{z - f (w)} d w d z = \frac{1}{2 π i} \int_{β} (\frac{1}{2 π i} \int_{γ} \frac{g (z)}{z - f (w)} d z) R (w, a) d w = \frac{1}{2 π i} \int_{β} g (f (w)) R (w, a) d w = (g \circ f) (a)$ , where the second-to-last equality is [step 5.2] and the last is the calculus of $g \circ f$ along $β$ .

7.1step 3.1step 6.1∎

Both clauses are proved: clause 1 by [step 3.1] and clause 2 by [step 6.1].

Remarks

The composition clause is the coverage's inline obligation. The composition law $g (f (a)) = (g \circ f) (a)$ is the second half of Bühler–Salamon Theorem 5.25(v) and of Shirbisheh Theorem 2.5.5; it is proved here, after the spectral mapping statement it needs, and not merely cited. The proof requires cycles around the compact image $f [K]$ of a bounded spectral neighbourhood, not the whole preimage of an outer contour.
Local constancy of $f$ on spectral components is allowed. Nothing in the argument uses that $f$ separates points of $σ_{A} (a)$ : the factorization of [step 1.1] is carried out at the single spectral point $λ$ , and the reverse inclusion tests values of $f$ on the spectrum pointwise.

Depends on

Used by

Dependency tree · two levels

67 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 — Theorem 5.25(iv)–(v), printed pp. 228 and 230–232 (standard reference, not scraped)
Vahid Shirbisheh, Lectures on C-star Algebras, v2 — Theorem 2.5.5, printed pp. 49–50 (standard reference, not scraped)