From Engelking's book on general topology (slightly rephrased):
Definition: We say that the net $S': \Sigma' \to X$ is finer than the net $S: \Sigma \to X$ if
1. there exists a function $f: \Sigma' \to \Sigma$ such that for any $\sigma'_0 \in \Sigma'$ there exists a $\sigma_0 \in \Sigma$ such that for any $\sigma' \in \Sigma'$ $\sigma'_0 \leq \sigma'$ implies $\sigma_0 \leq f(\sigma')$,
2. $S \circ f = S'$.
We call such an $f$ a refinement.
Now the most obvious definition of a net morphism is a preorder morphism of the underlying directed sets satisfying (2). My question: is there any need to consider refinements which are not morphisms?
To be more precise:
Conjecture: For any refinement $f$ between $S': \Sigma' \to X$ and $S: \Sigma \to X$ there exists a morphism $\hat f: S' \to S$ such that $\hat f$ is a refinement, and $\hat f(\Sigma') \subset f(\Sigma')$.
In plain words, this means that any refinement can be refined further using a morphism from the same net.
I can't quite get a knack of how to prove this conjecture or construct a counterexample. Also it may be that I'm overcomplicating matters and refinements can be reduced to refinement morphisms in a simpler manner. Any tips?
