Alphabeta Math
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 functional calculus homomorphism

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let A be a unital complex Banach algebra and let a∈A. Write f(a) for the holomorphic functional calculus value of Holomorphic functional calculus, with the contour independence of Holomorphic functional calculus is contour independent in force. Let f,g be holomorphic on open sets Uf,Ug⊇σA(a) and let α,β∈C. Then:

  1. (αf+βg)(a)=αf(a)+βg(a), computed on Uf∩Ug;
  2. (fg)(a)=f(a)g(a), computed on Uf∩Ug;
  3. 1(a)=1 for the constant function 1, and id(a)=a for the coordinate function id(z)=z, computed on any open set containing σA(a);
  4. for every polynomial p(z)=∑k=0nckzk one has p(a)=∑k=0nckak, the sum in the Banach algebra A;
  5. if h is holomorphic and nowhere zero on Uh⊇σA(a), then h(a) is invertible with h(a)−1=(1/h)(a), where 1/h is holomorphic on Uh.

Thus f↦f(a) is a unital algebra homomorphism from the algebra of germs of functions holomorphic near σA(a) to A, and it reproduces polynomials and reciprocals of nonvanishing functions.

Facts & Assumptions

Given: An assumed Axiom of Choice, a unital complex Banach algebra A, an element a∈A, an open set U⊇σA(a), a holomorphic f:U→C, and an admissible cycle Γ in U∖σA(a) with index 1 on σA(a) and index 0 outside U.

[L1]

f(a)=12πi∫Γf(z)R(z,a) dz, independent of the admissible cycle, and the chain integral is additive over sums of contours with the norm bound ∥∫Γh dz∥≤L(Γ)sup⁡Γ∗∥h∥ for continuous h (Holomorphic functional calculus, Holomorphic functional calculus is contour independent, Banach algebra valued contour integral, Contour integral commutes with bounded linear maps).

[L9]

The spectrum is contained in the closed disc of radius ∥a∥ (Spectrum is nonempty compact and norm bounded).

[L2]

Resolvent identity: R(w,a)R(z,a)=(R(w,a)−R(z,a))/(z−w) for distinct w,z∈ρA(a); all resolvents and the element a commute with one another (Resolvent identity, Spectrum and resolvent set in a Banach algebra).

[L3]

Cauchy formula on a cycle: if g is holomorphic on an open Ω and Γ is a cycle with trace in Ω null-homologous in Ω, then n(Γ,p)g(p)=12πi∫Γg(ζ)/(ζ−p) dζ for every p∈Ω∖Γ∗ (Cauchy's integral formula for a null-homologous cycle).

[L4]

Vanishing Cauchy theorem: if h is holomorphic on an open Ω and Γ is a cycle with trace in Ω null-homologous in Ω, then ∫Γh dz=0 (Cauchy's theorem for a null-homologous cycle).

[L5]

Nested cycles: for compact K⊆U with U open there are cycles β,γ with traces in U∖K, disjoint, with n(β,⋅)=n(γ,⋅)=1 on K, n(γ,w)=1 for w∈β∗ and n(β,z)=0 for z∈γ∗; each is a finite chain of directed line segments whose boundary function vanishes, although its constituent contours need not be closed (Admissible cycle around a compact plane set).

[L6]

For a cycle Γ and 0∉Γ∗, ∫Γz−1 dz=2πi n(Γ,0) by the definition of index (Integration over a complex chain and the index of a chain). For n≥1, the function z−n−1 has the primitive −z−n/n on C∖{0}, so its integral over Γ vanishes (The integral of a continuous derivative over a cycle is zero). Also ∫Γc dz=0 for every constant c, by summing endpoint increments over the cycle (The contour integral of a constant c is c times the endpoint displacement, Complex chains, their traces, and cycles).

[L7]

∥y∥<1 implies (1−y)−1=∑n≥0yn with the series converging in norm, and every convergent series on a compact C∞ contour may be integrated termwise: if hN→h uniformly on the trace then ∫ΓhN dz→∫Γh dz by the norm bound of [L1] (Neumann series).

Proof

technique · direct
1.1L1algebra

Linearity: for a common admissible cycle Γ in Uf∩Ug one has (αf+βg)(a)=12πi∫Γ(αf(z)+βg(z))R(z,a) dz=α f(a)+β g(a), because the chain integral is C-linear in the integrand.

1.2L1L5L9algebra

Unit law, cycle choice: choose r>∥a∥ and apply [L5] to the compact closed disc K={z:∣z∣≤r} inside C. It gives a finite polygonal cycle Γr whose trace lies outside K and whose index is 1 on K. Since σA(a)⊆K and the constant function 1 is entire, Γr is admissible for its calculus value; by contour independence [L1], 1(a) may be computed on Γr.

1.3L1L6algebra

Coordinate identity: for every admissible cycle Γ and the function id(z)=z one has the pointwise identity zR(z,a)=1+aR(z,a) on Γ∗, hence id(a)=12πi∫Γdz+a⋅12πi∫ΓR(z,a)dz=0+a 1(a) by [L6] and [L1].

1.4L5algebra

Nested cycles: apply [L5] to the compact set K:=σA(a) and the open set Uf∩Ug; this produces cycles β,γ with disjoint traces in (Uf∩Ug)∖σA(a), both admissible for f and for g, with n(γ,w)=1 for every w∈β∗ and n(β,z)=0 for every z∈γ∗.

2.1step 1.4L3

First Cauchy integral: for each fixed w∈β∗ the scalar function g is holomorphic on Ug, and γ is a cycle with trace in Ug that is null-homologous in Ug because its index vanishes outside Ug by admissibility; [L3] gives 12πi∫γg(z)z−wdz=n(γ,w)g(w)=g(w).

2.2step 1.4L4algebra

Second Cauchy integral: for each fixed z∈γ∗ the function w↦f(w)z−w is holomorphic on Uf∖{z}, a neighbourhood of β∗; and β is null-homologous in Uf∖{z}, because n(β,p)=0 for every p∉Uf by admissibility and n(β,z)=0 by the nesting; hence [L4] gives 12πi∫βf(w)z−wdw=0.

2.3step 1.2L6L7algebra

Unit law, value: the compact trace of Γr lies in the open set {∣z∣>r}, so q:=max⁡z∈Γr∗∥a∥/∣z∣<1. Hence R(z,a)=1z(1−a/z)−1=∑n≥0anz−n−1 uniformly on the trace. Integrating termwise by [L7], [L6] gives ∫Γrz−1dz=2πi n(Γr,0)=2πi and ∫Γrz−n−1dz=0 for n≥1. Thus 12πi∫ΓrR(z,a)dz=1 and 1(a)=1.

3.1step 1.4step 2.1L1algebra

The double integral: the function H(w,z):=f(w)g(z)R(w,a)R(z,a) is continuous on the compact product β∗×γ∗; the two-dimensional tagged Riemann sums of H over refined partitions of β and γ converge in A, by the uniform-continuity mesh estimate underlying the Banach-valued contour integral in [L1] applied in both variables, so the two iterated integrals 12πi∫β(12πi∫γH dz)dw and 12πi∫γ(12πi∫βH dw)dz exist and agree.

3.2step 1.3step 2.3algebra

Coordinate law, value: combining [step 1.3] with [step 2.3] gives id(a)=a⋅1=a.

4.1step 2.1step 2.2step 3.1L2algebra

Splitting the double integral: by the resolvent identity [L2], R(w,a)R(z,a)=(R(w,a)−R(z,a))/(z−w) for w∈β∗, z∈γ∗, so the double integral of [step 3.1] splits into the sum of the iterated integrals of f(w)g(z)R(w,a)/(z−w) and of −f(w)g(z)R(z,a)/(z−w); the first inner integral over γ equals g(w)R(w,a) by [step 2.1], and the second inner integral over β equals 0 by [step 2.2].

5.1step 2.1step 2.2step 4.1L1

Multiplicativity: using [step 4.1], f(a)g(a)=12πi∫βf(w)R(w,a)(12πi∫γg(z)z−wdz)dw−12πi∫γg(z)R(z,a)(12πi∫βf(w)z−wdw)dz=12πi∫βf(w)g(w)R(w,a)dw=(fg)(a); here each resolvent factor commutes with the scalar coefficient in front of it. This is claim 2.

6.1step 2.3step 5.1algebra

Inverse compatibility: for h holomorphic and nowhere zero on Uh⊇σA(a) the reciprocal 1/h is holomorphic on Uh and h⋅(1/h)=1 there; by [step 5.1] and [step 2.3], h(a)(1/h)(a)=1(a)=1 and symmetrically (1/h)(a)h(a)=1, so h(a) is invertible with h(a)−1=(1/h)(a); this is claim 5.

7.1step 1.1step 2.3step 3.2step 5.1step 6.1∎

Polynomials and conclusion: a constant function z↦c is c⋅1, so its calculus value is c 1(a)=c1 by [step 1.1] and [step 2.3]; the coordinate function has value a by [step 3.2]; multiplicativity [step 5.1], linearity [step 1.1] and induction on the degree therefore assemble p(a)=∑k=0nckak for every polynomial, which is claim 4. Claims 1, 2, 3 and 5 were proved in [step 1.1], [step 5.1], [step 2.3], [step 3.2] and [step 6.1].

Depends on

Used by

Dependency tree · two levels

70 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