Localic maps given by series

Question

Maps between real numbers are often defined by convergent series. For example, to define the exponential map, we can just prove that series $$ \sum_{n = 0}^{\infty} \frac{x^n}{n!} $$ converges, which implies that there is a map to which it converges. Can we use this approach to define (constructively) localic maps between localic reals? If not, how do we define maps like these?

Answer 1

Here is a fairly general methods for this sort of thing :

Step 1) We give a constructive proof that for each (Dedekind) real $x$, the serie $\sum \frac{x^n}{n!}$ converge. We define $exp(x)$ as the limit.

Step 2) We show that $x \mapsto exp(x)$ is a geometric construction. That is if $f : \mathcal{E} \to \mathcal{S}$ is a geometric morphism and $x$ is a Dedekind real in $\mathcal{S}$ then $exp(f^*x) = f^*exp(x)$.

For limits of series this is relatively easy to do : The key point is that quantification over $\mathbb{N}$ is well behaved when it comes to pullback along a geometric morphism: if $P(n)$ denotes some proposition in $\mathbb{S}$ indexed by the NNO (so essentially a subobject of $\mathbb{N}_S$) then $$f^*(\exists n \in \mathbb{N}, P(n)) = \exists n \in \mathbb{N}, f^*(P(n))$$ and $$f^*(\forall n \in \mathbb{N}, P(n)) \Rightarrow \forall n \in \mathbb{N}, f^*(P(n))$$ and as the definition of limit can be written using only quantification over $\mathbb{N}$ that's enough.

Step 3) Just use the Yoneda lemma : the locale $\mathbb{R}$ represent the functor on the category of locale that sends a locale $X$ to the set of Dedekind real in $Sh(X)$, and the two points above shows that $exp$ is a natural transformation of this functor.

I think Step 2 alway work for things defined as limits of a series or sequence (at least I can't imagine a situation where it doesn't), and step 3) is completely formal, so in general, the only things you need to do to define this kind of functor is Step 1) (though you should quickly check step 2).