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.
Banach-Stone
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be or , let and be nonempty compact Hausdorff spaces, and let be a surjective linear isometry, where both spaces carry the supremum norm. Then there are a homeomorphism and a continuous function with for all , such that
Conversely, for every homeomorphism and every continuous with , the formula defines a surjective linear isometry . The representation is by a pair that is unique: is determined by and . The conclusion does not say that a general linear isometry is multiplicative or unital.
Facts & Assumptions
Given: An assumed Axiom of Choice, nonempty compact Hausdorff spaces , and a surjective linear isometry over .
The extreme points of the dual unit ball of are exactly the normalized evaluations: (Extreme points of the dual ball of C(K), The Axiom of Choice).
The transpose is bounded linear with , , and ; consequently for a bijective isometry one has (The transpose of a bounded operator, The transpose is bounded with the same norm, Transposition reverses composition).
A surjective linear isometry maps the unit ball onto the unit ball and preserves extreme points: if is extreme and with in the target unit ball, applying writes as the corresponding convex combination of and .
For a nonempty compact Hausdorff space , the evaluation map is a homeomorphism, and the family separates points from closed sets, so the evaluation map into the product over is an embedding (Characters of continuous functions are evaluations, The evaluation map of a point–closed-set separating family is a topological embedding).
Under Dependent Choice — which follows from the Axiom of Choice — the Urysohn lemma holds in normal spaces, so in a compact Hausdorff space two distinct points are separated by a continuous function into (Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into , and conversely such a space is normal, The Axiom of Choice).
Proof
is linear and isometric, because for all ; hence by [L2] the transpose is a bounded linear bijection with , and .
For every the point evaluation is an extreme point of of the form , so by [L1] and [L3] its image is an extreme point of ; by [L1] there are unique and with and . This defines functions and .
Conversely, let be a homeomorphism and continuous with , and set . Then is -linear, because is surjective, and is surjective with inverse .
Evaluating at the constant function gives , so is continuous, and for all by [step 1.2].
For and : , using the definition of the transpose in [L2] and [step 1.2].
The map is continuous: for every the function is continuous, since is continuous and is continuous with so is continuous; the family therefore consists of continuous functions and the evaluation embedding of into the product over has continuous composition , whence is continuous because is an embedding by [L4].
Applying [step 1.2] and [step 2.2] to the surjective isometry (which is a surjective linear isometry by [step 1.1]) produces continuous and with such that for all .
From : for and one computes by [step 2.2] and [step 3.2], with ; if then [L5] gives with , contradicting the displayed identity; so , and the same argument with the roles reversed gives . Hence is a bijection with continuous inverse , that is, a homeomorphism.
By [step 2.2] and [step 4.1] every surjective linear isometry has the asserted form with a homeomorphism and ; by [step 1.3] every pair of that form defines a surjective linear isometry; and the pair is unique since by [step 2.1] and then is recovered from by the formula.
Remarks
- Nonemptiness is a hypothesis. For or the space is the zero algebra and the conclusion is vacuous; the argument above uses nonemptiness to have a point evaluation to transpose.
- The weight is forced. Step 2.1 identifies with , so the isometry is unital precisely when ; nothing in the theorem requires this.
Depends on
- Extreme points of the dual ball of C(K)
- Characters of continuous functions are evaluations
- The transpose of a bounded operator
- The transpose is bounded with the same norm
- Transposition reverses composition
- The evaluation map of a point–closed-set separating family is a topological embedding
- Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into $[0,1]$, and conversely such a space is normal
- AC supplies the countable and dependent choices used in Banach integration
- The Axiom of Choice
Used by
Dependency tree · two levels
41 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
- Orr Shalit, Advanced Analysis Notes 14: the isometric structure of C(K) — Theorem 2 and Exercises B–C, HTML lines 38–54; the adjoint and extreme-point inputs are supplied locally (standard reference, not scraped)
- Theo Bühler and Dietmar A. Salamon, Functional Analysis — §5.5.1, printed pp. 258–267 (standard reference, not scraped)