Definition:Embedding (Model Theory)

This page is about embedding in the context of Model Theory. For other uses, see embedding.

This page has been identified as a candidate for refactoring of basic complexity. In particular: Preferably hold off till at least one source is identified, to avoid rework Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. 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$.

Sources

There are no source works cited for this page. Source citations are highly desirable, and mandatory for all definition pages. Definition pages whose content is wholly or partly unsourced are in danger of having such content deleted. To discuss this page in more detail, feel free to use the talk page.