Out of curiosity I started to go through an introductory course on schemes and to convince myself that I could prove every result (after an appropriate reformulation if necessary) constructively, i.e. without use of the law of excluded middle. See here for a nice explanation of how to avoid the use of the law of excluded middle (and hence the existence of prime ideals!) by defining schemes as certain locally ringed locales. This project is going quite well, but there is one thing that is leaving me a bit puzzled.
There are some well known technical statements in algebraic geometry of the form $\newcommand{\sheaf}{\mathcal}\newcommand{\from}{\colon}\newcommand{\into}{\hookrightarrow}$
Proposition 1: Let $X$ be a scheme and let $\sheaf{F}$ be a quasi-coherent sheaf of modules on $X$. If $\sheaf{F}$ is finitely generated then the support $\{ x \in X \mid \sheaf{F}_x \neq 0\}$ is a closed subset of $X$.
Proposition 2: Let $S$ be a scheme. Let $f \from X \to S$ be a morphism which is locally of finite presentation. Let $\sheaf{F}$ be a quasi-coherent $\sheaf{O}_X$-module which is locally of finite presentation. Then $\{ x \in X \mid \sheaf{F}_x \text{ is flat over } \sheaf{O}_{S,f(x)}\}$ is an open subset of $X$.
There are also the corresponding affine statements
Proposition 1a: Let $A$ be a commutative ring and $M$ finitely generated $A$-module. Then the set of all prime ideals of $A$ such that $M_\mathfrak{p} \neq 0$ is closed in the prime spectrum of $A$ (and coincides with $V(\mathrm{Ann}(M))$).
Proposition 2a: Let $f \from A \to B$ be a ring homomorphism of finite presentation and let $M$ be a finitely presented $B$-module. Then the set of all prime ideals $\mathfrak{p}$ of $B$ such that $M_\mathfrak{p}$ is flat as an $A$-module is open in the prime spectrum of $B$.
There are of course other such statements concerning the smooth locus of a morphism etc. My problem is that I don't even know how to state these propositions constructively. Schemes as locales do not have underlying sets of points which one could test on whether the stalk of a sheaf at that point satisfies some condition.
Regarding the first proposition (closedness of the support), one could try to define the support of a finitely generated module as the closed subscheme $V(\mathrm{Ann}(M)) \into \mathrm{Spec}(A)$ and for the global case one can maybe show that these subschemes can be glued together sensibly.
However the radical ideal definig the open subset in Prop. 2a cannot be described as easily. The proof certainly makes the impression that something nontrivial is going on and my question is how to capture the constructive content of these arguments. I assume a constructive proof won't be easy (in some way or another some $\mathrm{Tor}$ groups will be involved and already the definition of these groups is a bit problematic in constructive mathematics (see here)). Therefore for now I will be happy with a formulation of the statement which is sensible in a constructive setting.
