# Definition:Embedding (Model Theory)

This page has been identified as a candidate for refactoring.Until this has been finished, please leave
`{{Refactor}}` in the code.
Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$.To discuss this page in more detail, feel free to use the talk page.When this work has been completed, you may remove this instance of `{{Refactor}}` from the code. |

## Definition

Let $\MM$ and $\NN$ be $\LL$-structures with universes $M$ and $N$ respectively.

$j: \MM \to \NN$ is an **$\LL$-embedding** if and only if it is an injective map $M \to N$ which preserves interpretations of all symbols in $\LL$; that is, such that:

- $\map j {\map {f^\MM} {a_1, \dots, a_{n_f} } } = \map {f^\NN} {\map j {a_1}, \ldots, \map j {a_{n_f} } }$ for all function symbols $f$ in $\LL$ and $a_1, \dots, a_{n_f}$ in $M$
- $\tuple {a_1, \ldots, a_{n_R} } \in R^\MM \iff \tuple {\map j {a_1}, \dots, \map j {a_{n_R} } } \in R^\NN$ for all relation symbols $R$ in $\LL$ and $a_1, \dots, a_{n_R}$ in $M$
- $\map j {c^\MM} = c^\NN$ for all constant symbols $c$ in $\LL$.

### Partial Embedding

A common method of constructing isomorphisms and elementary embeddings in proofs is to recursively define them a finite number of elements at a time. For this purpose, it is useful to have a definition of embeddings using functions which are only defined on a subset of $M$:

Let $A \subseteq M$ be a subset of $M$.

$j: A \to \NN$ is a **partial $\LL$-embedding** if and only if it is an injective map $A \to N$ which preserves interpretations of all symbols in $\LL$ applied to elements of $A$; that is, such that:

- $\map j {\map {f^\MM} {a_1, \dots, a_{n_f} } } = \map {f^\NN} {\map j {a_1}, \ldots, \map j {a_{n_f} } }$ for all function symbols $f$ in $\LL$ and $a_1, \dots, a_{n_f}$ in $A$
- $\tuple {a_1, \ldots, a_{n_R} } \in R^\MM \iff \tuple {\map j {a_1}, \dots, \map j {a_{n_R} } } \in R^\NN$ for all relation symbols $R$ in $\LL$ and $a_1, \dots, a_{n_R}$ in $A$
- $\map j {c^\MM} = c^\NN$ for all constant symbols $c$ in $\LL$.

### Isomorphism

$j: \MM \to \NN$ is an **$\LL$-isomorphism** if and only if it is a bijective $\LL$-embedding.

### Automorphism

$j: \MM \to \NN$ is an **$\LL$-automorphism** if and only if it is an $\LL$-isomorphism and $\MM = \NN$.

It is often useful to talk about automorphisms which are constant on subsets of $M$. So, there is a definition and a notation for doing so:

Let $A \subseteq M$ be a subset of $M$, and let $b \in M$.

An $\LL$-automorphism $j$ is an **$A$-automorphism** if and only if $\map j a = a$ for all $a\in A$.

An $\LL$-automorphism $j$ is an **$A, b$-automorphism** if and only if it is an $\paren {A \cup \set b}$-automorphism; that is: $\map j a = a$ for all $a \in A$ and also $\map j b = b$.