The spectral theory of commutative C*-algebras: The constructive Gelfand-Mazur theorem

摘要

It is shown, for a commutative C*-algebra in any Grothendieck topos E, that the locale MFnAof multiplicative linear functionals onAis isomorphic to the locale MaxAof maximal ideals ofA, extending the classical result that the space of C*-algebra homomorphisms fromAto the field of complex numbers is isomorphic to the maximal ideal space ofA, 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.