Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Characters of continuous functions are evaluations

Statement

Assume the Axiom of Dependent Choice (The axiom of dependent choice: a relation in which every element is related to something admits an N-indexed chain). Let K be a nonempty compact Hausdorff space and let C(K)=C(K,C) be the complex Banach algebra of continuous functions with pointwise operations and the supremum norm (Compact support, Cc(X), and C0(X) for the notation C(K)). Then:

  1. every character of C(K) is the evaluation evx(f)=f(x) at a unique point x∈K;
  2. the map e:K→Δ(C(K)), e(x):=evx, is a homeomorphism onto Δ(C(K)) with the pointwise-evaluation topology (Character and maximal ideal space).

For K=∅ the algebra C(K)={0} is the zero algebra and Δ(C(K))=∅, since the only linear map {0}→C is zero; the empty case is therefore consistent with the same formula and is recorded here rather than proved as part of claim 2, whose proof uses nonemptiness.

Facts & Assumptions

Given: Dependent Choice, a nonempty compact Hausdorff space K, and the algebra C(K) of continuous complex functions on K with pointwise operations and the supremum norm.

[L1]

A uniformly Cauchy sequence of complex-valued functions on a set converges uniformly to a function (A sequence of complex-valued functions converges uniformly if and only if it is uniformly Cauchy). If the domain is any topological space and all the functions are continuous, the uniform limit is continuous: at a point, approximate the limit uniformly by one function and apply that function's continuity.

[L2]

C is complete, and a sequence in C converges if and only if it is Cauchy (The complex plane is complete, and convergence is equivalent to convergence of real and imaginary parts).

[L3]

Every character of a nonzero unital complex Banach algebra is unital and contractive: χ(1)=1 and ∣χ(f)∣≤∥f∥ (Characters on a unital Banach algebra are continuous).

[L6]

Every compact Hausdorff space is normal and T1 (A compact Hausdorff space is regular and normal, hence T3 and T4).

[L5]

A continuous real function on a nonempty compact space attains a finite maximum; a continuous bijection from a compact space onto a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

Proof

technique · direct
1.1L1L2L5algebra

For f∈C(K), continuity of ∣f∣ and compactness give a finite maximum by [L5], so the supremum norm is well-defined. C(K) is a nonzero commutative unital complex Banach algebra: pointwise operations give an associative commutative bilinear product and the constant function 1 is a unit with ∥1∥=1; the supremum norm is submultiplicative and satisfies the triangle inequality; and C(K) is complete, because a Cauchy sequence (fn) in the supremum norm is uniformly Cauchy, so its pointwise limit f exists by [L2] and is continuous by [L1], and ∥fn−f∥∞→0 by the definition of uniform Cauchyness. Nonzero: since K≠∅, the constant function 1 is not the zero function.

1.2algebra

For every x∈K the evaluation evx(f):=f(x) is a character of C(K): it is complex-linear, multiplicative, and nonzero since evx(1)=1≠0.

1.3algebra

For any characters χ≠ψ of C(K) there is f with χ(f)≠ψ(f), so the evaluation-open sets {φ:∣φ(f)−χ(f)∣<ε} and {φ:∣φ(f)−ψ(f)∣<ε} with ε=∣χ(f)−ψ(f)∣/2 are disjoint; hence Δ(C(K)) is Hausdorff in the pointwise-evaluation topology.

1.41.2algebra

The map e:K→Δ(C(K)), e(x)=evx, is continuous, because for each f∈C(K) the composition x↦evx(f)=f(x) is continuous by the continuity of f.

1.5L4L6algebra

The evaluations are pairwise distinct: if x≠y in K, then {x} and {y} are disjoint closed subsets of the normal space K by [L6], so by [L4] there is a continuous f:K→[0,1] with f(x)=0 and f(y)=1; then evx(f)=0≠1=evy(f).

2.11.1L3algebra

Let χ be a character of C(K) and suppose the common zero set of ker⁡χ is empty. The family {Uf:f∈ker⁡χ}, where Uf={x:f(x)≠0}, is an open cover of K formed without choosing a function for each point. Compactness gives a finite subcover; choosing a witnessing function for each of its finitely many members gives f1,…,fn∈ker⁡χ with no common zero. Here n≥1 since K is nonempty. Then g=∑i=1nfi‾fi is in ker⁡χ: each fi‾ is continuous and the kernel is an ideal, without any assumption that χ preserves conjugation. Also g>0 everywhere, so 1/g is continuous and 1=g(1/g)∈ker⁡χ. This contradicts χ(1)=1 from [L3] applied using [step 1.1]. Thus there is x∈K at which every member of ker⁡χ vanishes.

3.11.2step 2.1algebra

With x as in [step 2.1], ker⁡χ⊆ker⁡evx. Both are kernels of nonzero multiplicative linear functionals, hence both are maximal ideals: if f∉ker⁡χ then every h∈C(K) has h−(χ(h)/χ(f))f∈ker⁡χ, so any ideal strictly containing ker⁡χ contains f and hence equals C(K). Therefore ker⁡χ=ker⁡evx.

4.11.5step 3.1L3algebra

Hence for every f∈C(K) one has f−f(x)1∈ker⁡evx=ker⁡χ, so χ(f)=f(x)χ(1)=f(x), using χ(1)=1 from [L3]; thus χ=evx, and by [step 1.5] the point x is unique.

5.1step 1.2step 1.3step 1.4step 1.5step 4.1L5∎

By [step 1.2], [step 1.5] and [step 4.1] the map e is a bijection from K onto Δ(C(K)); by [step 1.4] it is continuous, K is compact, and by [step 1.3] Δ(C(K)) is Hausdorff, so [L5] makes e a homeomorphism.

Remarks

  • Dependent Choice is inherited from Urysohn. It is used for the separation of distinct points in [step 1.5], and nowhere else; the common-zero argument is choice-free once finitely many functions are chosen by compactness.
  • The empty case. If K=∅ then C(K)={0} and there is no character, so Δ(C(K))=∅=e[K], and claim 2 holds trivially with the empty map; the proof above uses K≠∅ only to know that 1≠0 in C(K).

Depends on

Dependency tree · 2 levels

Sources