How do we externalize an element of a model of ZFC? Let $\mathbf{Z} =(V^\mathbf{Z},\in^\mathbf{Z})$ denote a model of ZFC (not necessarily well-founded; but, its a set).
Question 0. If $\mathbf{G} \in V^\mathbf{Z}$ has the property that "$\mathbf{Z} \models \mathbf{G}\; \mbox{is a group},$" how do we obtain an actual group from $
\mathbf{G}$? More generally, how do we externalize an element of a model of ZFC?
Question 1. I get the feeling that we can only externalize $\mathbf{G} \in V^\mathbf{Z}$ if, letting $D \subseteq V^\mathbf{Z}$ denote the transitive closure of $\mathbf{G}$ with respect to $\in^\mathbf{Z},$ we have that $(D,\in^\mathbf{Z} \restriction D)$ is a well-founded structure (in the ambient universe). Is this feeling correct? If so, would it be fair to say that the significance of well-founded models of ZFC is that they're precisely those models whose every element is externalizable?
 A: The group (or at least isomorprphic copy) is already a group on the outside. To elaborate. 
So let say that $(V, \in)$ is your base universe of set theory. Let $(Z, E)$ be a $\{\in\}$-structure such that $(Z, E) \in V$, i.e. $(Z, E)$ is a set in $V$. 
So by the assumption there is some $G \in^V Z$ such that $(Z,E) \models G$ is a group. More precisely there is a set $\cdot \in^V Z$ such that $(Z,E) \models (G, \cdot)$ is a group. 
As $G, \cdot \in V$, you may want to guess that $V \models (G, \cdot)$ is a group already. However this is not true since there is no reason $\cdot$ is a binary relation on $G$ (as $\in$ and $E$ may not agree since $E$ may not equal $\in$).
Therefore let $\tilde G = \{x \in Z : x \ E \ G\}$ which exists by comprehension in $V$. Let $\times = \{(a,b) \in Z : (a,b) \ E \ \cdot\}$. 
Now to just check that $V \models (\tilde G, \times)$ is a group. I will just check that there is an identity. Since $(Z,E) \models (G, \cdot)$ is a group. $(Z,E)$ proves that there is some $e \ E \ G$ such that for all $a \ E \ G$, $a \cdot e = e \cdot a$. By how $\tilde G$ is defined, $e \in G$. By how $\times$ is defined, $e \times a = a \times e$. So $e$ is the identity in $(\tilde G, \times)$ as viewed in $V$. The other axiom should be similar. 
