<\body> >>>>>>>>>>>>>>()>>>)>>>>>>>(> : }>>> <\doc-data||<\doc-note> This is an expanded version of our paper[CS05a]. For the convenience of the reader we have included more details and added a few clarifications. There are no new results. We are grateful to Bob Lubarsky and Fred Richman for suggesting improvements in the presentation. ||||<\author-address> Chalmers University,\ Sweden |>|||<\author-address> Radboud University Nijmegen,\ the Netherlands ||<\author-note> This author was supported by the Netherlands Organization for Scientific Research (NWO). >|> \; \; <\abstract> 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. Our proof is shorter, clearer, and we avoid the use of approximate eigenvalues. 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. 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. 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(sec. 3). <\definition> A is a vector space with a compatible binary sup operation that is, such that c)=(a+b)\(a+c)> and, moreover, a\0> and 0>, whenever in , > in >, 0> and \0>. One can prove that A Riesz space (or ) is a partially ordered linear space which is a distributive lattice. As usual we define \a\0>, \(-a)\0>, a+a> and 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.\ <\definition> A in an ordered vector space is a positive<\footnote> We follow the standard terminology using `positive' to mean non-negative. element such that for all R> there exists a natural number such that n\1>. We will now consider a Riesz space with a strong unit. When is a rational number, we will often write q> to mean q\1>. <\definition> A of is a linear map :R\> such that (1)=1> and (a\b)=\(a)\\(b)>. Such a representation automatically preserves all the Riesz space structure. <\example> If is a compact space, then , its space of continuous functions, is a Riesz space where the supremum is taken pointwise. Each point of defines a representation (f)\f(x).> In Example we show that a complete commutative algebra of Hermitian operators on a Hilbert space is a Riesz space. Given a Riesz space , we will define a lattice that may be used to define the spectrum of as a formal space, the points of which are then precisely the representations of . Let denote the set of positive elements of a Riesz space . For in we define b> to mean that there exists such that n*b>. We write b> for b> and b>. The following proposition is proved in and involves only elementary considerations on Riesz spaces. <\proposition> We write for the quotient of by >. Then is a distributive lattice. In fact, if we define L(R)> by [a]>, then is the free lattice generated by R}> subject to the following relations: <\enumerate-numeric> , if 0>; ; D(-a)=0>; D(a)\D(b)>; b)=D(a)\D(b)>. We have D(b)> if and only if \b> and if and only if 0>.\ For in and rational numbers , we write (p,q)\(a-p)\(q-a)>. Notice that this is an element of by our convention that means 1)>. <\lemma> (p,q)\a\(p,s)\a\(t,q)>, whenever are rational numbers such that s>. Since our Riesz space has a strong unit, for each , there exists and such that q> and (p,q)=1>. Moreover, if ,\,I> are open intervals covering , then a\I\1>. <\proof> We may assume that t\s\q>. <\eqnarray> (p,s)\a\(t,q)>||(s-a))\((a-t)\(q-a))>>|||(a-t)) \ \ ((a-t)\(s-a))\>>|||(q-a))\((q-a)\(s-a))>>|||((a-t)\(s-a))\>>|||(q-a))\(q-a)>>||>|(q-a))\((a-t)\(s-a)).>>>> We claim that (s-a))\>. To show this we write >. Then\ <\equation*> (a-s) \ (t-a) =(a-m + (m-s)) \ (t-m - (a-m)) = + ((a-m) \ -(a-m))\. The proof is finished by the observation that c> whenever for some >, \1\b\c>. <\lemma> If )\\\D(b)=1>, then there exists 0> such that -r)\\\D(b-r)=1>. <\proof> Since \b\\\b> we see that\ <\eqnarray*> >|>|\\\b)->>|||-)\\\(b-)>>||>|-)\\\(b-).>>>> The previous lemma is used to prove the following result, which can be found as Theorem1.11 in. We will not need this, but only state it as a motivation. <\theorem> Define >, the of , to be the locale generated by the elements and the relations in Proposition together with the relation 0>D(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 . In fact, if a representation > is given, then \D(a)> if and only if (a)\0>. Dedekind cuts may be used to define real numbers, but it should be noted that constructively one needs to require that such cuts are , i.e.either L> or U>, whenever 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 numbers, see. In general, such a cut does not have a greatest lower bound in . If it does the upper real number is called or simply a real number. Define the upper real {q\\|\q\q. a\q\1}> for each element of the Riesz space. If it is located is said to be and the greatest lower bound is denoted by . Then we have q> if and only if U(a)>. <\proposition> If all elements of are normable, then the predicate \sup a\0> has the following properties: <\enumerate-numeric> If and D(b)>, then >; If b>, then > or >; If is a strictly positive rational number, then > or . We note that > if and only if >>. In fact, in localic terms this shows that > is , or , see, 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 > as soon as is positive, i.e.0>. In particular, 0 is positive, but > does not hold.\ In order to prove Proposition we first need three lemmas. <\lemma> b)=sup a\sup b>. <\proof> \; <\description-compact> >>Suppose that b\q\q>, then q>, so both q> and q>. Thus \sup a\sup b>. >>If \a,b>, then \a\b> and hence b\sup a\sup b>. <\lemma> Let be a rational number. If r> and sup(b\c)>, then sup c.> <\proof> If r>, then r\r>, for some rational number >. So, using Lemma\ <\equation*> r\sup (b\c)=sup b\sup c\r\sup c. Consequently, sup c>. <\lemma> If sup (b\b)>, then \0> or \0>. <\proof> Suppose that r\sup( b\b)>. Either \r> or \0>. In latter case we are done. In the former case \r> by Lemma. <\proof> ]>\ Property 1 is clear. Property 2 is Lemma. Finally, to prove property 3 we decide whether 0> or r>. In the former case >. In the latter case . <\corollary> If )\\\D(a)=1>, we can find \\\i> such that >)\\\D(a>)=1> and >>,\,>>>. <\proof> By Lemma there exists 0> such that -r)\\\D(a-r)=1>. By Proposition for all , -r)=0> or >>. From this the result follows. <\lemma> Let , (r,s)>. Define (p+r,q+s)> and J\(p\r,q\s)>. If \> and I\b\J\c\K>>, then the distance between and is bounded by >. If b-c\|\\> and I\b\J\c\K>>, then the distance between J> and is bounded by >. Finally, if \> and I\b\J>>, then the distance between and is bounded by >. <\proof> We only prove the last fact. If the distance between and is bigger than >, than \> or \>. Consequently, b-r)=0> or s-b)=0>. Both cases imply that I\b\J)=0>. <\definition> A Riesz space is if there exists a sequence > such that for all and \ \0>, there exists such that \|\\>. <\theorem> Let be a separable Riesz space all elements of which are normable. Assume that , then there exists a representation > such that (a)\0.> <\proof> We write \2>. Using dependent choice and Lemma we define a sequence )> of rationals such that <\equation*> (, sup a)\a\(q-\,q+\)\\\a\(q-\,q+\)>. If R>, we can find a sequence of elements >> such that for any \0> we have >\|\\> when is large enough. Then >> is a Cauchy sequence and we define (b)\limq>>. By Lemma this definition does not depend on the choice of the sequence >>. The map > is a representation such that (a)\0> and (a)\(q-\,q+\)> for all . A suggestive way to state that (a)\0> is to say that > is a in . Let > be the set of representations of . We call > the of . Each representation is a bounded linear functional. Each element of defines a pseudo norm (\)\\|\(a)\|> on the space of bounded linear functionals. If is separable and > is a dense sequence in R|\|a\|\1>>, we can collect, like Bishop, all the pseudo-norms into one norm (\)\2\|\(a)\|>. We have the following Stone-Yosida representation theorem, see. <\theorem> [DC]> Let is a separable Riesz space all elements of which are normable. The spectrum > is a complete totally bounded metric space. For in , we define :\\> by (\)\\(a)> and a \<\|\|\>\sup(\|a\|)>. Then >\|(\)\| =\<\|\|\>a\<\|\|\>.> Finally, the set of functions > is dense in )>. <\proof> We define \D(a\(r,s))> as an element of the lattice . Intuitively, such an element may be thought of as the set |\(a)\(r,s)>=|\(\)\s-r>>. Let \0>. Using Lemma one may find finitely many \ > such that \>, the supremum of which equals 1 in the lattice . By Corollary one can assume all these elements to be positive. Each of them contains a point by Theorem. 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 \<\|\|\>a\<\|\|\>>, then by Theorem, there exists > such that \|\(a)\|>. Finally, the density follows from Proposition3.1 in. Its proof involves only elementary properties of Riesz spaces. Notice the interplay between the and framework. From a formal covering, in the lattice , it is possible to deduce that >, a metric space, is totally bounded. This is remarkable since there are examples of Riesz spaces such that in a recursive interpretation of Bishop's mathematics > does not have enough points. For instance, consider the Riesz space of continuous real functions on Cantor space (>>). The spectrum of is precisely Cantor space and the representations are its points<\footnote> To see this, note that the characteristic function > of any basic open is continuous. So, given a representation >, (\\(1-\))=0> and (\\(1-\))=1>. Consequently, (\)> is either 0 or 1. It follows that the representations can be identified with the points. , which is known not to have enough points in a recursive interpretation. In particular, this means that we have a collection of open sets which covers all the recursive points, but does not allow a finite subcover. This is possible since this collection does not cover the space in the usual terminology of formal topology. \ In this section we apply the results of the previous section to f-algebras. <\definition> An is a Riesz space with a strong unit and a commutative<\footnote> multiplication such that a*b>, whenever a> and b>. <\example> If is a complete commutative algebra of normable self-adjoint operators on a Hilbert space , then is a Riesz space with the order > defined by A > if and only if 0> for all in .\ In the rest of this subsection we prove that if 0,> then 0>. We have now defined two notions of boundedness on the algebra of operators. One as a bounded operator: is bounded by if for all , A x\<\|\|\>\a\<\|\|\>x\<\|\|\>>. The other from the ordering: is bounded by if a I>, where is the identity operator. <\lemma> The two notions of boundedness coincide that is, for all , (a x,x)> if and only if for all , A x\<\|\|\>\a\<\|\|\>x\<\|\|\>>. Consequently, A\<\|\|\>=\<\|\|\>A\<\|\|\>>. <\proof> The usual proof, for instance in using the polarization identity, is constructive. \ Since x,x)=(A*(B x),(B x))>, we see that \0>, whenever 0>. This suffices to prove that is an ordered ring. <\lemma> \ (p33, footnote 9)>> Let be a as above. Then every positive element is the uniform limit of a sum of squares. <\proof> We can assume that A\1.> Define :=A> and :=A-A>. Then A\1,> since =A(1-A)+(1-A)A\0> and =1-A+A>. Moreover, =A-A\A>. Since +\+A+A,> we have \1/n\0>. By Lemma this implies that \0>. <\corollary> 0>, whenever 0>. <\proof> If 0>, then (A Bx,Bx)\0>, where > is a sequence such that B> converges to .\ The following lemma shows that one can construct the square root admits square root of positive elements if is complete. Notice that the proof is directly constructive, and it corresponds to the usual Taylor expansion of >.> when is complete and thus one can define the absolute value as >>. From the absolute value one first defines \(\|A\|+A)/2> and then B\A+(B-A)>. Consequently, the algebra is a Riesz space and an f-algebra. <\lemma> For all 0> we can build a Cauchy sequence )> of positive elements such that \A>. <\proof> We can assume A\I>. We define the two sequences \[0,I]> and \[0,1]> defined by =0> and =0> and <\equation*> A=(1-A+A)r=(1+r) Clearly, we have \r> for all . We claim that we have for all <\equation*> A\Ar\rA-A\r-r This is proved by induction from the equalities <\equation*> A-A=(A+A)(A-A)r-r=(r+r)(r-r) It follows that we have <\equation*> (I-A)-A=2(A-A)\2(r-r) In order to conclude, all is left is to show that )> has limit . We know that r\r\1> and we have <\equation*> 1-r=(1-r)=(1-r)(1+r)\(1-r)(1-|2>) if \1-\>. This shows that if |2>)\\> we have \\> for all N>. Any f-algebra is a Riesz space so we have a Gelfand representation of the f-algebra qua Riesz space, see Theorem. <\theorem> The Gelfand transform |^>> preserves multiplication. <\proof> Since -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 Lemma6.3 in, \b\(a*b)>, so (a*b)\r(\(b)\\(a-r))\0>, which was to be proved. Suppose that (a)\| \q>. Then \(a)> and so (q-a)\0>. Similarly, (q+a)\0>. Consequently, (q-a)=\((q-a)(q+a))\0>. By a similar argument we see that if (a)\|\q>, then (a)\|\q>. We conclude that (a)=\(a)>. 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> [DC]>Let > be a separable f-algebra of normable elements, then the spectrum > is a compact metric space and there exists an f-algebra embedding of > into )>. We now specialize this theorem to the f-algebra in Example 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 Cor.8.28 by considering its self-adjoint part which is an f-algebra. <\corollary> Let > 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 > into )>. <\theorem> [DC]>Let be an Abelian C*-algebra of operators on a Hilbert space. Then there exists a C*-algebra embedding >of into ,)>, where > is a compact metric space. Moreover, (1)=1> and 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. For a typical application, we let be a compact group and be the algebra of operators over (G)> generated by the unit operator and the operators f\g>, where > denotes the convolution product. Each operator is compact and hence normable. The non-trivial representations of are then exactly the characters of the group . This gives a reduction of the Peter-Weyl theorem to the Gelfand representation theorem, see. 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 is not only compact completely regular, but also that is, has a positivity predicate as shown by Proposition. In this case all the continuous functions are normable. This is a general fact. <\theorem> If is a compact completely regular locale, then is overt if and only if for any C(X)> there exists > such that s> if and only if (-\,s)=X.> <\proof> We prove only the `only if' part. If is overt and C(X)>, then an approximation of the supremum can be found by considering a finite covering of by positive opens of the form (r,s)>, where is small. The previous facts suggest a similarity between Bishop's compact metric spaces and the compact overt spaces in formal topology. ||||> compact overt>>>>>> Clearly this requires further developments building on ideas in. 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. He also introduced the term . 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<\footnote> This framework is related to Richman's proposal to develop constructive mathematics without using countable choice, see. . Using classical logic and the axiom of choice one can show that the spectrum defined in Theorem has enough points. Thus in this setting the pointfree and pointwise description of the space coincide. In a recursive interpretation of Bishop's framework these descriptions differ. However, using dependent choice, normability and separability assumptions, we have shown how to deduce that > is totally bounded from the pointfree description of >.\ 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. 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.\ Richman(p.5) gave an informal argument that indicates that one can not construct the zeroes of the complex polynomial -a> unless one knows whether or not. To in we can associate the locale > of roots of -a>. The existence of a point in > requires dependent choice. On the other hand using results from it should be possible to show that > is compact overt as an element of the completion of the metric space -multisets in . The metric on this space is the usual Hausdorff metric on compact subsets of >.\ 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. It is interesting to note that Richman proposes to use spreads to avoid dependent choice. We suggest to use formal spaces instead. One motivation of formal topology 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 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.\ 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. 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 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? Considering that the Stone-ƒech compactification has been successfully treated in locale theory, 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 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 and the references therein for a constructive theory of almost periodic functions. \; <\bibliography|bib|alpha|douglas.bib,StoneYosida.bib,expanded.bib> <\bib-list|Wra90> Errett Bishop and Douglas Bridges. , volume 279 of . Springer-Verlag, 1985. Garrett Birkhoff. . Third edition. American Mathematical Society Colloquium Publications, Vol. XXV. American Mathematical Society, Providence, R.I., 1967. N.Bourbaki. Hermann, 1964. Thierry Coquand. About Stone's notion of spectrum. , 197(1-3):141--158, 2005. T.Coquand and B.Spitters. Formal Topology and Constructive Mathematics: the Gelfand and Stone-Yosida Representation Theorems. , 11(12):1932--1944, 2005. . Thierry Coquand and Bas Spitters. A constructive proof of the Peter-Weyl theorem. , 4:351--359, 2005. PeterT. Johnstone. . Number3 in Cambridge studies in advanced mathematics. Cambridge University press, 1982. PeterT. Johnstone. Open locales and exponentiation. In , volume30 of , pages 84--116. Amer. Math. Soc., Providence, RI, 1984. Serge Lang. . Addison-Wesley Publishing Company Advanced Book Program, Reading, MA, second edition, 1983. LynnH. Loomis. . University Series in Higher Mathematics. van Nostrand, New York, 1953. W.A.J. Luxemburg and A.C. Zaanen. . North-Holland Publishing Co., Amsterdam, 1971. North-Holland Mathematical Library. Per Martin-Löf. . Almqvist & Wiksell, Stockholm, 1970. Fred Richman. Generalized real numbers in constructive mathematics. , 9:595--606, 1998. Fred Richman. The fundamental theorem of algebra: a constructive development without choice. , 196:213--230, 2000. Fred Richman. Spreads and choice in constructive mathematics. , 13:259--267, 2002. F.Riesz. Ueber die linearen Transformationen des komplexen Hilbertschen Raumes. , 5:23--54, 1930-32. Giovanni Sambin. Intuitionistic formal spaces - a first communication. In D.Skordev, editor, , pages 187--204. Plenum, 1987. Bas Spitters. Constructive algebraic integration theory without choice. , 2005. Bas Spitters. Almost periodic functions, constructively. , accepted. M.H. Stone. A general theory of spectra. II. , 27:83--87, 1941. Paul Taylor. A lambda calculus for real analysis. , August 2005. Steven Vickers. Localic completion of generalized metric spaces I. submitted for publication, draft available on web at , 2003. G.C. Wraith. Unsurprising results on localic groups. , 67(1):95--100, 1990. Kôsaku Yosida. On the representation of the vector lattice. , 18:339--342, 1942. <\initial> <\collection> <\references> <\collection> |1>> > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > <\auxiliary> <\collection> <\associate|bib> Coquand:jucs_11_12:formal_topotoly_and_constructive Bishop/Bridges:1985 Coquand:obs Birkhoff LuxemburgZaanen Bourbaki Coquand:obs Coquand:obs Richman:cuts Vickers:locAA Johnstone:open Stone:spectrum2 Yosida Coquand:obs Lang Riesz:1930 Coquand:obs Bishop/Bridges:1985 CoquandSpittersPW MartinLof:NCM Johnstone:open Taylor Richman:fta johnstone:stone Richman:fta Richman:fta Vickers:locAA Richman:spreads MartinLof:NCM Sambin:1987 johnstone:stone spitters:obs Loomis:AHA johnstone:stone Wraith:groups Spitters:ap <\associate|toc> |math-font-series||1.Introduction> |.>>>>|> |math-font-series||2.Riesz spaces> |.>>>>|> |2.1.General definitions |.>>>>|> > |2.2.Spectrum |.>>>>|> > |2.3.Normable elements |.>>>>|> > |math-font-series||3.f-algebras> |.>>>>|> |3.1.f-algebra of operators |.>>>>|> > |3.2.Gelfand representation |.>>>>|> > |3.3.Peter-Weyl |.>>>>|> > |math-font-series||4.Compact overt locales> |.>>>>|> |math-font-series||5.Choice> |.>>>>|> |5.1.No points |.>>>>|> > |5.2.Spreads |.>>>>|> > |math-font-series||6.Conclusion> |.>>>>|> |math-font-series||Bibliography> |.>>>>|>