The spectral theory of commutative C&#42-algebras: the constructive Gelfand-Mazur theorem

Abstract

It is shown, for a commutative C*-algebra in any Grothendieck topos E, that the locale MFnA of multiplicative linear functionals on A is isomorphic to the locale MaxA of maximal ideals of A, extending the classical result that the space of C*-algebra homomorphisms from A to the field of complex numbers is isomorphic to the maximal ideal space of A, that is, the Gelfand-Mazur theorem, to the constructive context of any Grothendieck topos. The technique is to present MaxA, in analogy with our earlier definition of MFnA, by means of a propositional theory which expresses one's natural intuition of the notion involved, and then to establish various properties, leading up to the final result, by formal reasoning within these theories.

Keywords: locale; commutative C*-algebra; spectrum; propositional geometric theory; constructive; Gelfand duality; Gelfand-Mazur theorem

Quaestiones Mathematicae 23(2000), 465–488