The upper semi-continuous rank of a module sheaf

Question

The article "Intuitionistic algebra and representations of rings" is fantastic; it develops the language, logic etc. for the topos $Sh(X)$, where $X$ is a fixed topological space, from scratch and thereby illuminating most of the known (and more) notions of sheaf theory in the sense that they become more natural. Thanks again Peter Arndt for this reference.

On page 37, the rank of a module $M$ is introduced as a upper Dedekind cut in the sheaf $\mathbb{N}$, or equivalently as a upper semi-continuous function $r : X \to \mathbb{N} \cup \{\infty\}$. Now it is claimed that it is given explicitely by mapping $x$ to the minimal number of generators needed for the stalks $M_x$. However, I don't see why this should be upper semi-continuous. I can show that only in the case that $M$ is locally of finite type. In fact, when I track back the constructions I get, that $r(x)$ is the infimum of numbers of sections which generate $M|_U$, where $U$ varies over the open neighborhoods of $x$.

Is this the correct definition of the rank?

Basically the same question applies to the definition of the independence $i(x)$, which is claimed to be the maximal number of linearly independent elements in $M_x$. Again, I don't see why this should be lower semi-continuous.

Answer 1

This ought to be a comment, but I don't have the necessary reputation. I believe the claim is indeed false unless $M$ is locally of finite type. Here's a bit of context:

1. It's always the case that an internal upper Dedekind cut $A$ in $\mathrm{Sh}(X)$ induces an upper semi-continuous function $X \to \mathbb{N} \cup \{ \infty \}$, by mapping $x \in X$ to $\inf\{ n \in \mathbb{N} | \exists \text{open} V \subseteq X, x \in V: V \models (n \in A) \}$. This function takes values in $\mathbb{N}$ iff the cut is inhabited (in the internal sense).

2. The internally defined cut $A = \{ n \in \mathbb{N} | \text{there exists a generating family for $M$ consisting of $n$ elements} \}$ is inhabited iff $M$ is in the internal sense a finitely generated module, i.e. in the usual external sense locally of finite type.

3. Let $r$ be the function induced by this cut. It's easy to prove that the stalk $M_x$ can be generated by $r(x)$ elements. The reverse implication, that if $M_x$ can be generated by $n$ elements then $r(x) \leq n$, can be proven if $M$ locally of finite type.

So $r(x)$ coincides with the minimal number of generators needed for the stalk $M_x$ if $M$ is locally of finite type (at least in an open neighbourhood of $x$). If $M$ is not locally of finite type, $r$ will still be upper semi-continuous, but might not coincide with the minimal number of generators.

I don't know the "correct" definition of the rank if the module is not locally of finite type.