This question was [posted](https://math.stackexchange.com/posts/4199651/edit) on Math Stack Exchange, but did not attract an answer. Here is the question:


Informal Description
====================


Let me start with an example. Let $X$ be the set $\{a, b, c, d, e\}$ and $E$ be the set $\{a, b, c\}$. Let $f$ be a function with domain $X$.
Then the mapping that sends $E$ to $\{f(a), f(b), f(c) \}$ is called the direct image of $E$ under $f$, denoted by $f\_\*(E)$.


Now, let $W$ be the set $\{\{a, b\}, \{c\}\}$. What do you call the mapping that sends $W$ to $\{\{f(a), f(b)\}, \{f(c)\}\}$ ?


Informally, this mapping replaces every element of $X$ *"inside"* $W$ with its image under $f$.


Slightly More Formal Description
================================


Let us assume the [ZFA-axiomatisation](https://ncatlab.org/nlab/show/ZFA#:%7E:text=ZFA%20is%20a%20variant%20of,made%20up%20of%20other%20elements.) of Set Theory, a variant of ZF that allows non-set objects called atoms. Let $A$ be a set of atoms.


Define $P^0(A)$ = A.


And for all $n \in \mathbb{N} \colon$ define $P^n(A)= \mathscr{P}(P^{n-1}(A)) \cup A $ ,


where $\mathscr{P}(-)$ denotes the powerset of a set.


And define $P^{\infty}(A)$ as $\bigcup\_{n \in \mathbb{N}} P^{n}(A)$


Let $X$ be a set of atoms. Let $f$ be a function with domain $X$. We could then inductively define a function $f\_{\*\*}$ such that $dom(f\_{\*\*}) = P^{\infty}(X) \backslash X$ , and $f\_{\*\*}$ has the property that for all $Z \in dom(f\_{\*\*}) \colon f\_{\*\*}(Z) = \{f\_{\*\*}(T) | T \in Z \backslash X \} \cup \{f(x) | x \in Z \cap X \}$.


Examples
--------


* Let $X = \{a, b, c, d, e\}$ be a set of atoms. Then $\{a, \{b\}\} \in P^{\infty}(X) \backslash X$ and $f\_{\*\*}(\{a, \{b\}\}) = \{f(a), \{f(b)\}\}$
* Let $X = \{a, b, c, d, e\}$ be a set of atoms. Then $\{\{ \{c \} \}\} \in P^{\infty}(X) \backslash X$ and $f\_{\*\*}(\{\{\{c \} \}\}) = \{\{\{f(c) \} \}\}$


So $f\_{\*\*}$ can, in a sense, be thought of as a generalisation of the direct image. My quesiton is, what do you call this concept? And can you point me towards any resources regarding it? I would prefer if the resource makes use of the ZFA-axiomatisation, but I would also accept any other resource.


Sidenote
--------


I am aware that this concept comes up in [Permutation Models](https://en.m.wikipedia.org/wiki/Permutation_model#CITEREFFraenkel1922) for the case when $f$ is a bijective endofunction.



What do you call the generalisation of the direct image?
This idea is commonly used in set theory with atoms. I'm not sure whether it has a standard name, but I would be inclined to call it the *natural extension* of $f$ to sets.


There is no need to stop the iteration at $\omega$ as you do, for one can continue the cumulative hierarchy through the ordinals. If $A$ is any class of atoms, you can define the well-founded cumulative hierarchy over $A$ by transfinite recursion, just like the ordinary cumulative hierarchy, like this:


$\newcommand{\WF}{{\rm WF}}$
$$\WF\_0(A)=A,$$
$$\WF\_{\alpha+1}(A)=\mathcal P(\WF\_\alpha(A)),$$
$$\WF\_\lambda(A)=\bigcup\_{\alpha<\lambda}\WF\_\alpha(A)$$


Specifically, we start with just the atoms, and then iteratively add all subsets of what we've got so far.


It is straightforward to see that every function $\sigma:A\to V$ defined on the atoms extends naturally to a function $\bar\sigma$ defined on the entire hierarchy over those atoms by the following recursion:


$$\bar\sigma(x)=\begin{cases}
 \sigma(x)&\text{if $x\in A$,}\\
 \bar\sigma[x]&\text{otherwise}
\end{cases}$$


You can view this as a $\in$-recursion or alternatively as a recursion on ordinals, defining $\bar\sigma$ on each $\WF\_\alpha(A)$. This definition agrees with yours (on finite levels), since we apply the original function to the atoms, and otherwise apply the pointwise image recursively.


Another way to think about the natural extension is that every set is having the atoms in its hereditary membership replaced with their values as specified by the original function. So this is a kind of hereditary application of the original function.


You asked for references, and so let me mention that we use exactly this idea in our paper:


* *Daghighi, Ali Sadegh; Golshani, Mohammad; Hamkins, Joel David; Jeřábek, Emil*, [**The foundation axiom and elementary self-embeddings of the universe**](http://www.arxiv.org/abs/1311.0814), Geschke, Stefan (ed.) et al., Infinity, computability and metamathematics. Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch. London: College Publications (ISBN 978-1-84890-130-8/hbk). 89-112 (2014). [ZBL1358.03070](https://zbmath.org/?q=an:1358.03070).


In the proof of theorem 2, for example, we have a function $\sigma$ defined on the atoms (for us it is Quine atoms, but ZFA urelements would work the same), and then extend this to all of $\WF(A)$ by recursion.


In the case that the original map was a permutation of the atoms, then the natural extension of it is an automorphism of the cumulative hiearchy over those atoms.


Another application of the idea arises in the Jech-Sochor embedding theorem, which can be found in Jech's book Set Theory.


