Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userFormal topology and constructive mathematics: the Gelfand and Stone-Yosida representation theorems
114
0
0.0
(
0
)
Ask ChatGPT about the research
No Arabic 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.
rate research
Read More
In Riesz space theory it is good practice to avoid representation theorems which depend on the axiom of choice. Here we present a general methodology to do this using pointfree topology. To illustrate the technique we show that almost f-algebras are commutative. The proof is obtained relatively straightforward from the proof by Buskes and van Rooij by using the pointfree Stone-Yosida representation theorem by Coquand and Spitters.
We present a constructive proof of Gelfand duality for C*-algebras by reducing the problem to Gelfand duality for real C*-algebras.
Let $X$ and $Y$ be completely regular spaces and $E$ and $F$ be Hausdorff topological vector spaces. We call a linear map $T$ from a subspace of $C(X,E)$ into $C(Y,F)$ a emph{Banach-Stone map} if it has the form $Tf(y) = S_{y}(f(h(y))$ for a family of linear operators $S_{y} : E to F$, $y in Y$, and a function $h: Y to X$. In this paper, we consider maps having the property: cap^{k}_{i=1}Z(f_{i}) eqemptysetiffcap^{k}_{i=1}Z(Tf_{i}) eq emptyset, where $Z(f) = {f = 0}$. We characterize linear bijections with property (Z) between spaces of continuous functions, respectively, spaces of differentiable functions (including $C^{infty}$), as Banach-Stone maps. In particular, we confirm a conjecture of Ercan and Onal: Suppose that $X$ and $Y$ are realcompact spaces and $E$ and $F$ are Hausdorff topological vector lattices (respectively, $C^{*}$-algebras). Let $T: C(X,E) to C(Y,F)$ be a vector lattice isomorphism (respectively, *-algebra isomorphism) such that Z(f) eqemptysetiff Z(Tf) eqemptyset. Then $X$ is homeomorphic to $Y$ and $E$ is lattice isomorphic (respectively, $C^{*}$-isomorphic) to $F$. Some results concerning the continuity of $T$ are also obtained.
We show that numerous distinctive concepts of constructive mathematics arise automatically from an antithesis translation of affine logic into intuitionistic logic via a Chu/Dialectica construction. This includes apartness relations, complemented subsets, anti-subgroups and anti-ideals, strict and non-strict order pairs, cut-valued metrics, and apartness spaces. We also explain the constructive bifurcation of some classical concepts using the choice between multiplicative and additive affine connectives. Affine logic and the antithesis construction thus systematically constructivize classical definitions, handling the resulting bookkeeping automatically.
Interactive theorem provers based on dependent type theory have the flexibility to support both constructive and classical reasoning. Constructive reasoning is supported natively by dependent type theory and classical reasoning is typically supported by adding additional non-constructive axioms. However, there is another perspective that views constructive logic as an extension of classical logic. This paper will illustrate how classical reasoning can be supported in a practical manner inside dependent type theory without additional axioms. We will see several examples of how classical results can be applied to constructive mathematics. Finally, we will see how to extend this perspective from logic to mathematics by representing classical function spaces using a weak value monad.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
