I have a general question about techniques used in @Emerton's proof, sketched below, in the answer to $\mathbb{P}^n$ is simply connected.
Given a finite étale map $\pi: Y \to \mathbb P^n$ (we regard all involved schemes as $k$-schemes for some fixed base field $k$), a base point $x \in \mathbb P^n$ and a point $y \in Y$ lying over $x$. Then naïvely/on the level of sets we construct a map $ \mathbb P^n \setminus \{x\} \to Y \setminus \{y\}$, $x' \mapsto y'$ by taking a unique line $L$ joining $x'$ with $x$, choosing the unique component $L'$ of the preimage $ \pi^{-1}(L)$ which contains $y$ and letting $y' \in Y'$ be the point lying over $x'$.
Now the funny thing is that $x' \mapsto y'$ is algebraic, i.e., a morphism in the category of schemes and that sounds quite surprising to me at first glance.
Emerton's argument was to observe that this map is realized as the composition of three maps, which can presumably be recognized as morphisms on their own:
$x' \mapsto \pi^{-1}(L)$, which is a map from $\mathbb P^n \setminus \{x\}$ to the Hilbert scheme of $Y$
picking out of $L' \subset \pi^{-1}(L)$ the component containing $y$, which should be a morphism from a locally closed subset of the Hilbert scheme of $Y$ to the Hilbert scheme of $Y$ itself and finally
mapping $L'$ to $L' \cap \pi^{-1}(x')$.
My naïve question is why the steps 1–3 are all morphisms in sense of algebraic geometry?
There are two standard ways in algebraic geometry to specify a morphism $f: X \to Y$ between schemes: ‘old school style’ by writing down an explicit polynomial equations with variables living in projective spaces which implicitly contain $X $ and $Y$.
The more modern functorial approach is to constuct a natural transformation between the functors $F_X= \operatorname{Hom}(-,X)$ and $F_Y= \operatorname{Hom}(-,Y)$ which the schemes $X$, $Y$ represent. That amounts to associating a family a $(f_S: F_X(S) \to F_Y(S)_{S \in (\mathrm{Sch}/k)}$ of maps indexed by the class $(\mathrm{Sch}/k)$ of $k$-schemes which commute with morphisms $m: S \to T$ in compatible way (= natural transform).
Seemingly morphisms 1–3 above were specified via the second approach. But the aspect which irritates me is that seemingly all three maps were only specified on the level of $k$-points,
for example the first map was seemingly specified just as a map $(\mathbb P^n \setminus \{x\})(k) \to \operatorname{Hilb}_Y(k)$, but in the spirit of the functorial construction above it is expected to specify this map as a family of maps $(\mathbb P^n \setminus \{x\})(S) \to \operatorname{Hilb}_Y(S)$ for all $k$-schemes $S$.
Or is it in this special situation sufficient to specify everything on level of $k$-points only? E.g., naïvely one could be tempted to interpret $ x'$ not as a $ k $-point, but an $ S $-point etc. But on the other hand it seems to make no sense to talk about a line between a $ k $-point (= $x$) and an $ S $-point, so I'm a bit skeptical if the construction can be ‘prolonged’ naturally to $ S $-points….
Update: as Marsault Chabat pointed out the constructions go through fine as long as $ S $ are spectra of fields, but I am not sure why these should work for arbitrary $ S $. Clearly it's wrong that a morphism is already determined by what it does on finite field extensions of ground field (“geometric points”).