1.Introduction

This paper illustrates the relevance of locale theory for constructive mathematics. We present a constructive proof of the Stone-Yosida representation theorem for Riesz spaces motivated by considerations from formal topology. This theorem is used to derive a representation theorem for f-algebras. In turn, this theorem implies the Gelfand representation theorem for C*-algebras of operators on Hilbert spaces as formulated by Bishop and Bridges [BB85]. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues.

The article is organized as follows. After dealing with some preliminaries we prove a pointfree Stone-Yosida representation theorem for Riesz spaces. In the next section this is used to obtain a representation theorem for f-algebras, which in turn is used to prove the Gelfand representation theorem. Next we discuss the similarity between Bishop's notion of compactness, i.e. complete and totally bounded, and compact overt spaces in formal topology. Finally we show that the axiom of dependent choice is needed to construct points in the formal spectrum.

We would like to stress that the present theory needs few foundational commitments, we work within Bishop-style mathematics. Moreover, the mathematics is predicative, even finitary, and we will not use the axiom of choice, even countable choice, unless explicitly stated.

2.Riesz spaces

We present a Stone-Yosida representation theorem for Riesz spaces. This theorem states that a Riesz space with a strong unit may be represented as a Riesz space of functions. In fact, one can even start with an l-group, or lattice ordered group, with a strong unit and construct a Riesz space from this, see [Coq05](sec. 3).

2.1.General definitions

Definition 1. A Riesz space R is a Q vector space with a compatible binary sup operation — that is, such that a + (b∨c) = (a + b)∨(a + c) and, moreover, λa⩾0 and - a⩽0, whenever a in R, λ in Q, a⩾0 and λ⩾0. One can prove that A Riesz space (or vector lattice) is a partially ordered linear space which is a distributive lattice.

As usual we define a ⁺ ≔a∨0, a ^- ≔( - a)∨0, |a|≔a ⁺ + a ^- and a∧b≔ - ( - a∨ - b). One can prove that a Riesz space is a lattice and that the lattice operations are compatible with the vector space operations, see [Bir67][LZ71][Bou64].

Definition 2. A strong unit 1 in an ordered vector space R is a positive

We will now consider a Riesz space R with a strong unit. When q is a rational number, we will often write a⩽q to mean a⩽q⋅1.

Definition 3. A representation of R is a linear map σ:R→R such that σ(1) = 1 and σ(a∨b) = σ(a)∨σ(b).

Such a representation automatically preserves all the Riesz space structure.

Example 4. If X is a compact space, then C(X), its space of continuous functions, is a Riesz space where the supremum is taken pointwise. Each point of x defines a representation σ_x(f)≔f(x).

In Example 19 we show that a complete commutative algebra of Hermitian operators on a Hilbert space is a Riesz space.

2.2.Spectrum

Given a Riesz space R, we will define a lattice that may be used to define the spectrum of R as a formal space, the points of which are then precisely the representations of R.

Let P denote the set of positive elements of a Riesz space R. For a,b in P we define a≼b to mean that there exists n such that a≤n b. We write a≈b for a≼b and a≽b. The following proposition is proved in [Coq05] and involves only elementary considerations on Riesz spaces.

Proposition 5. We write L(R) for the quotient of P by ≈. Then L(R) is a distributive lattice. In fact, if we define D:R→L(R) by D(a)≔[a ⁺ ], then L(R) is the free lattice generated by {D(a) | a∈R} subject to the following relations:

1. D(a) = 0, if a≤0;
2. D(1) = 1;
3. D(a)∧D( - a) = 0;
4. D(a + b)⩽D(a)∨D(b);
5. D(a∨b) = D(a)∨D(b).

We have D(a)⩽D(b) if and only if a ⁺ ≼b ⁺ and D(a) = 0 if and only if a⩽0.

For a in R and rational numbers p,q, we write a∈(p,q)≔(a - p)∧(q - a). Notice that this is an element of R by our convention that (a - q) means (a - q⋅1).

Lemma 6. a∈(p,q)≼a∈(p,s)∨a∈(t,q), whenever t,s are rational numbers such that t<s. Since our Riesz space has a strong unit, for each a, there exists p and q such that p<q and a∈(p,q) = 1. Moreover, if I₀,…,I_n are open intervals covering (p,q), then veea∈I_i≈1.

Proof. We may assume that p<t<s<q.

We claim that (( a - t )∨( s - a ))⩾

Lemma 7. If D(b₁)∨…∨D(b_n) = 1, then there exists r>0 such that D(b₁ - r)∨…∨D(b_n - r) = 1.

Proof. Since

The previous lemma is used to prove the following result, which can be found as Theorem 1.11 in [Coq05]. We will not need this, but only state it as a motivation.

Theorem 8. Define Σ, the spectrum of R, to be the locale generated by the elements D(a) and the relations in Proposition 5 together with the relation D(a) = vee_r>0D(a - r). Then Σ is a compact completely regular locale.

Compact completely regular locales are the pointfree analogues of compact Hausdorff spaces. Moreover, the points of Σ can be identified with representations of R. In fact, if a representation σ is given, then σ∈D(a) if and only if σ(a)>0.

2.3.Normable elements

Dedekind cuts may be used to define real numbers, but it should be noted that constructively one needs to require that such cuts (L,U) are located, i.e. either p∈L or q∈U, whenever p<q. Upper cuts in the rational numbers may be conveniently used to deal with certain objects that classically would also be real numbers, we call them upper real numbers, see [Ric98][Vic03]. In general, such a cut does not have a greatest lower bound in R. If it does the upper real number is called located or simply a real number. Define the upper real U(a)≔{q∈Q|∃q'<q. a≤q'⋅1} for each element of the Riesz space. If it is located a is said to be normable and the greatest lower bound is denoted by sup a. Then we have sup a<q if and only if q∈U(a).

Proposition 9. If all elements of R are normable, then the predicate Pos(a)≔sup a>0 has the following properties:

1. If Pos(a) and D(a)⩽D(b), then Pos(b);
2. If Pos(a∨b), then Pos(a) or Pos(b);
3. If r is a strictly positive rational number, then Pos(a) or D(a - r) = 0.

We note that Pos(a) if and only if Pos(a ⁺ ).

In fact, in localic terms this shows that Σ is open, or overt, see [Joh84], but we will not need this. In formal topology one would say that the formal space has a positivity predicate.

We remark that the standard terminologies from the two different fields seem to conflict. Clearly, it is not the case that Pos(a) as soon as a is positive, i.e. a⩾0. In particular, 0 is positive, but Pos(0) does not hold.

In order to prove Proposition 9 we first need three lemmas.

Lemma 10. sup (a∨b) = sup a∨sup b.

Proof.

Lemma 11. Let r be a rational number. If sup b<r and r<sup(b∨c), then r<sup c.

Proof. If sup b<r, then b⩽r'<r, for some rational number r'. So, using Lemma 10

Lemma 12. If 0<sup (b₁∨b₂), then sup b₁>0 or sup b₂>0.

Proof. [of Proposition 9]

Property 1 is clear.

Property 2 is Lemma 12.

Corollary 13. If D(a₁)∨…∨D(a_n) = 1, we can find i₁<…<i_k such that D(a_i1)∨…∨D(a_ik) = 1 and Pos(a_i1),…,Pos(a_ik).

Lemma 14. Let I: = (p,q), J≔(r,s). Define I + J≔(p + r,q + s) and I∨J≔(p∨r,q∨s). If |a + b - c|⩽ε and Pos(a∈I∧b∈J∧c∈K), then the distance between I + J and K is bounded by ε. If |a∨b - c|⩽ε and Pos(a∈I∧b∈J∧c∈K), then the distance between I∨J and K is bounded by ε.

Finally, if |a - b|⩽ε and Pos(a∈I∧b∈J), then the distance between I and J is bounded by ε.

Definition 15. A Riesz space R is separable if there exists a sequence a_n such that for all a and ε>0, there exists n such that |a - a_n|⩽ε.

Theorem 16. [DC] Let R be a separable Riesz space all elements of which are normable. Assume that Pos(a), then there exists a representation σ such that σ(a)>0.

Proof. We write ε_n≔2 ^{- n}. Using dependent choice and Lemma 6 we define a sequence (q_n) of rationals such that

A suggestive way to state that σ(a)>0 is to say that σ is a point in D(a).

Let Σ be the set of representations of R. We call Σ the spectrum of R. Each representation is a bounded linear functional. Each element a of R defines a pseudo norm ρ_a(φ)≔|φ(a)| on the space of bounded linear functionals. If R is separable and a_n is a dense sequence in {a∈R : |a|⩽1}, we can collect, like Bishop, all the pseudo-norms into one norm ρ(φ)≔∑_n2 ^{- n}|φ(a_n)|.

We have the following Stone-Yosida representation theorem, see [Sto41][Yos42].

Theorem 17. [DC] Let R is a separable Riesz space all elements of which are normable. The spectrum Σ is a complete totally bounded metric space. For a in R, we define a^{^}:Σ→R by a^{^}(σ)≔σ(a) and ‖a ‖≔sup(|a|). Then sup_σ|a^{^}(σ)| = ‖a‖. Finally, the set of functions a^{^} is dense in C(Σ).

Proof. We define U_{a r s} ≔D(a∈(r,s)) as an element of the lattice L(R). Intuitively, such an element may be thought of as the set {σ : σ(a)∈(r,s)} = {σ : ρ_a(σ)<s - r}. Let ε>0. Using Lemma 6 one may find finitely many U_{a r s} such that s - r<ε, the supremum of which equals 1 in the lattice L(R). By Corollary 13 one can assume all these elements to be positive. Each of them contains a point by Theorem 16. The collection of these points forms an ε-net. Consequently, Σ is totally bounded.

It is straightforward to show that Σ is also complete as a uniform space.

For each σ∈Σ we have |σ(a)|⩽‖a‖. To see this suppose that σ(a)>‖a‖. Then there exists ε>0 such that σ(a) - a⩾ε1, however σ(σ(a) - a) = 0. If r< ‖a‖, then by Theorem 16, there exists σ such that r<|σ(a)|.

Notice the interplay between the pointwise and pointfree framework. From a formal covering, in the lattice L ( R ), it is possible to deduce that Σ, a metric space, is totally bounded. This is remarkable since there are examples of Riesz spaces R such that in a recursive interpretation of Bishop's mathematics Σ does not have enough points. For instance, consider the Riesz space R of continuous real functions on Cantor space (2 ^ω ). The spectrum of R is precisely Cantor space and the representations are its points

3.f-algebras

In this section we apply the results of the previous section to f-algebras.

Definition 18. An f-algebra is a Riesz space with a strong unit and a commutative

3.1.f-algebra of operators

Example 19. If R is a complete commutative algebra of normable self-adjoint operators on a Hilbert space H, then R is a Riesz space with the order ⩽ defined by 0⩽A if and only if (A u, u)⩾0 for all u in H.

In the rest of this subsection we prove that if A,B⩾0, then A B⩾0.

We have now defined two notions of boundedness on the algebra of operators. One as a bounded operator: A is bounded by a if for all x, ‖A x‖²⩽a‖x‖². The other from the ordering: A is bounded by a if A⩽a I, where I is the identity operator.

Lemma 20. The two notions of boundedness coincide — that is, for all x, (A x,x)⩽(a x,x) if and only if for all x, ‖A x‖²⩽a²‖x‖². Consequently, ‖A²‖ = ‖A‖².

Since (A B ²x,x) = (A (B x),(B x)), we see that A B²⩾0, whenever A⩾0. This suffices to prove that R is an ordered ring.

Lemma 21. [Rie32] (p33, footnote 9) Let R be a as above. Then every positive element is the uniform limit of a sum of squares.

Corollary 22. A B⩾0, whenever A,B⩾0.

The following lemma shows that one can construct the square root

Lemma 23. For all A⩾0 we can build a Cauchy sequence (A_n) of positive elements such that A

Proof. We can assume 0≤A≤I. We define the two sequences A_n∈[0,I] and r_n∈[0,1] defined by A₀ = 0 and r₀ = 0 and

Clearly, we have A_n≤r_n for all n.

We claim that we have for all n

This is proved by induction from the equalities

It follows that we have

In order to conclude, all is left is to show that (r_n) has limit 1. We know that 0≤r_n≤r_{n + 1}≤1 and we have

3.2.Gelfand representation

Any f-algebra is a Riesz space so we have a Gelfand representation of the f-algebra qua Riesz space, see Theorem 17.

Theorem 24. The Gelfand transform ⋅^{^} preserves multiplication.

Proof. Since 2a b = (a + b)² - a² - b². We need to prove that ⋅^{^} preserves squares — that is σ(a²) = σ(a)². For this we first prove: σ(a b)>0, whenever σ(a),σ(b)>0.

If σ( a )⩾ r >0, then σ( a - r )>0. By Lemma 6.3 in [ Coq05 ], ( a - r ) ⁺ ∧ b ⁺ ⩽

We have proved the following representation theorem for f-algebras which explains the name f-algebra: an f-algebra is an abstract function algebra.

Theorem 25. [DC]Let A be a separable f-algebra of normable elements, then the spectrum Σ is a compact metric space and there exists an f-algebra embedding of A into C(Σ).

We now specialize this theorem to the f-algebra in Example 19 and obtain Bishop's version of the Gelfand representation theorem. In fact, like Bishop we first prove the theorem for Hermitian operators. As a corollary we obtain the Gelfand duality theorem for a separable Abelian C*-algebra, exactly as stated by Bishop [BB85] Cor.8.28 by considering its self-adjoint part which is an f-algebra.

Corollary 26. [DC]Let A be a separable f-algebra of normable Hermitian operators on a Hilbert space, then the spectrum is a compact metric space and there exists an f-algebra embedding of A into C(Σ).

Theorem 27. [DC]Let R be an Abelian C*-algebra of operators on a Hilbert space. Then there exists a C*-algebra embedding φ of R into C(Σ,C), where Σ is a compact metric space. Moreover, φ(1) = 1 and R is norm-dense.

Bishop's Gelfand representation theorem states that for any commutative algebra of normable operators on a separable Hilbert space there exists a norm-preserving isomorphism to the algebra of continuous functions on its spectrum. To prove that this map is norm-preserving Bishop proves that certain ε eigenvectors can be computed. In fact, the computational information of the ε eigenvectors is used only to prove the non-computational statement that the map is norm-preserving. In contrast, we work directly on the approximations so that we can avoid these unused computational steps.

3.3.Peter-Weyl

For a typical application, we let G be a compact group and R be the algebra of operators over L₂(G) generated by the unit operator and the operators T(f)(g)≔f∗g, where ∗ denotes the convolution product. Each operator T(f) is compact and hence normable. The non-trivial representations of R are then exactly the characters of the group G. This gives a reduction of the Peter-Weyl theorem to the Gelfand representation theorem, see [CS05b].

4.Compact overt locales

Bishop defines a metric space to be compact if it is complete and totally bounded and proves that all uniformly continuous functions defined on such a metric space are normable. In contrast, in the framework of locale theory it is not true in general that all functions on a compact regular locale are normable, i.e. the norm is only defined as an upper real which may not be a located.

However, the locale considered in Theorem 8 is not only compact completely regular, but also overt — that is, has a positivity predicate — as shown by Proposition 9. In this case all the continuous functions are normable. This is a general fact.

Theorem 28. If X is a compact completely regular locale, then X is overt if and only if for any f∈C(X) there exists sup f∈R such that sup f<s if and only if f ^{- 1}( - ∞,s) = X.

The previous facts suggest a similarity between Bishop's compact metric spaces and the compact overt spaces in formal topology.

Clearly this requires further developments building on ideas in [ML70][Joh84]. However, we postpone this to further work.

It is interesting to note that Paul Taylor has independently found a similar relation between Bishop compact and compact overt in the context context of his abstract Stone duality [Tay05]. He also introduced the term overt.

We would like to conclude this discussion with the following comparison between the three following frameworks: classical mathematics with the axiom of choice, Bishop's mathematics and our framework, predicative constructive mathematics without dependent choice

Our conclusion is that the best formulation of the representation theorem is the pointfree one, since, besides being neutral on the use of the axiom of choice and classical logic, it implies the usual formulations both in Bishop's framework and in classical mathematics.

5.Choice

5.1.No points

As mentioned before, when all the elements of the algebra are normable, one can construct points in the spectrum using dependent choice. We claim that dependent choice is needed for this. In fact, it is known that there exist compact overt locales for which we need countable choice to construct a point. Thus it suffices to consider the space of continuous functions on such a locale. We think that a nice example can be extracted from [Ric00].

Richman [Ric00](p.5) gave an informal argument that indicates that one can not construct the zeroes of the complex polynomial X² - a unless one knows whether a = 0 or not. To a in C we can associate the locale Y_a of roots of X² - a. The existence of a point in Y_a requires dependent choice. On the other hand using results from [Vic03] it should be possible to show that Y_a is compact overt as an element of the completion of the metric space n-multisets in C. The metric on this space is the usual Hausdorff metric on compact subsets of C.

Finally, we remark that this leaves open the question whether it is possible to construct the points of the spectrum of a discrete countable Riesz space over the rationals, or more generally, to construct the points of the spectrum of a separable Riesz space.

5.2.Spreads

It is interesting to note that Richman [Ric02] proposes to use spreads to avoid dependent choice. We suggest to use formal spaces instead. One motivation of formal topology [ML70][Sam87] was precisely to give a direct treatment of Brouwer's spreads by working with trees of finite sequences. Formal topology may be seen as a predicative and constructive version of locale theory. Johnstone [Joh82] stresses that one may avoid the use of the axiom of choice in topology by using locale theory and dealing directly with the opens. In this light it may not be so surprising that Richman uses spreads to avoid choice.

Richman's definition of spread differs in two respects from Heyting's definition. The branching of the tree is arbitrary, i.e. not necessarily indexed by the natural numbers, and it is not decidable whether or not a branch can be continued. This may be compared to the present situation where we study the maximal spectrum Σ. When Σ has a countable base, we may define it as a finitely branching tree. When furthermore Σ is overt, every positive branch can be continued in a positive way. One difference between Richman's spreads and our approach is that Richman requires the infinite branches to be elements of a metric space.

6.Conclusion

We gave a constructive proof of the Stone-Yosida representation theorem for Riesz spaces. This theorem was used to prove a representation theorem for f-algebras, from which we derived the Gelfand representation theorem for commutative C*-algebras of operators on a Hilbert space. This constructive theorem generalizes the one by Bishop and Bridges. In a similar way one may prove a generalization of Bishop's spectral theorem, see [Spi05].

It should be noted that we have used normability and separability hypothesis in the statements of the main theorems and used the axiom of dependent choice. In fact, without these hypothesis we can still obtain the spectrum as a compact locale. The normability is necessary to show that the spectrum is overt. The separability hypothesis is used to obtain a metric space instead of a uniform space. Finally, the axiom of dependent choice is used in Theorem 16 to construct a point in each positive open, and thus obtain a metric space in the sense of Bishop.

In this context, we would like to mention a problem for both constructive versions of the Gelfand representation theorem: can it be applied to construct the Bohr compactification of, say, the real line, like Loomis [Loo53]? Considering that the Stone-Čech compactification has been successfully treated in locale theory [Joh82], one would hope that a similar treatment is possible. Since the almost periodic functions do not form an algebra constructively, we may consider the f-algebra of functions generated by them. However, in this algebra not all elements are normable. Any element of the group determines a point in the spectrum. However, it is not possible to extend the group operation to the spectrum and obtain a localic group, since every compact localic group has a positivity predicate [Wra90] and since, moreover, the spectrum is compact this would imply that all the functions in the f-algebra are normable. This, as we stated before, is not the case. See Spitters [Spied] and the references therein for a constructive theory of almost periodic functions.

Bibliography