I'm asking specifically about a proof given in Edward Nelson's "Internal Set Theory: A New Approach to Nonstandard Analysis".
Here's the theorem statement:
If every finite subset of a graph admits a k-coloring, then the graph admits a k-coloring.
Here's Nelson's proof:
Wlog, let $G = (V, E)$ and $k$ be standard. Then, let $F\subset V$ be a finite subset containing all standard points in $V$. By hypothesis, $F$ has a $k$-coloring $f$. By (S) there is a standard function $g$ with domain $V$ such that $g$ agrees with $f$ on all standard inputs. By transfer, $g$ is a $k$-coloring for $G$.
Here's my question: how does standardization imply the existence of an extension $g$ of $f$ that has domain $V$?
My initial approach was to use standardization to construct the set $g$ generated by all standard elements of $f$, i.e. $g := \{(x,y)\in V \times k: (x, y)\in f \}$. However, while it's fairly straightforward to prove that $g$ is single-valued with domain included by $V$, I don't see how $dom(g) \supseteq V$.
In particular, I fail to see why it isn't possible for there to be some standard $x\in V$ such that $f(x)$ is not standard, allowing $(x, f(x))$ to not be contained in $g$. Is there some application of an axiom in IST that disallows this or otherwise lets us work around it?
There is no such element, because $f(x)$ belongs to the set $k$. And since $k$ is a standard finite set, all of its elements are standard. I'm sure you've already proved this fact at this point, but if not, you can refer to Theorem 1.2.5 in the introduction of my PhD thesis for a short and easy argument.
So in fact to all standard vertices of $G$, the function $f$ assigns a unique standard color. By Transfer, its standardization $g$ is then a function from the vertices of $G$ to $k$. This answers your question from the post.
Finiteness of the codomain $k$ is essential here. Pick a nonstandard natural $\omega \in \mathbb{N}$. The constant function $x \mapsto \omega$ then takes the standard number $0$ to the nonstandard $\omega$, which answers your titular question in the negative: in IST, nonstandard functions can take standard objects to nonstandard objects.
It's also not true that "if a function $f$ takes every standard value to some standard value, then $f$ is standard": for example, the map $x \mapsto H(x - \omega)$, where $H$ denotes the Heaviside step function, has this property, but is nonstandard.