This page consider the very general concept of embeddings. For the special cases traditionally considered see at embedding of topological spaces or embedding of smooth manifolds.
An embedding is, generally, a morphism which in some sense is an isomorphism onto its image
For this to make sense in a given category $C$, we not only need a good notion of image. Note that it is not enough to have the image of $f\colon X \to Y$ as a subobject $\im f$ of $Y$; we also need to be able to interpret $f$ as a morphism from $X$ to $\im f$, because it is this morphism that we are asking to be an isomorphism.
effective epimorphism$\Rightarrow$ regular epimorphism $\Leftrightarrow$ covering
effective monomorphism$\Rightarrow$ regular monomorphism $\Leftrightarrow$ embedding .
One general abstract way to define an embedding morphism is to say that this is equivalently a regular monomorphism.
If the ambient category has finite limits and colimits, then this is equivalently an effective monomorphism. In terms of this we recover a formalization of the above idea, that an embedding is an iso onto its image :
For a morphism $f : X \to Y$ in $C$ the definition of image as an equalizer says that the image of $f$ is
In particular we have a factorization of $f$ as
where the morphism on the right is a monomorphism.
The morphism $f$ being an effective monomorphism means that $\tilde f$ is an isomorphism, hence that $f$ is an “isomomorphism onto its image”.
Assume that the dependent type theory has identity types, dependent identity types, and uniqueness quantifiers. Then a family of elements $x:A \vdash f(x):B$ is an embedding if there is a family of elements
which states that for all identities $q:f(x) =_B f(y)$ there is a unique identity $p:x =_A y$ up to identity such that $ap_f(x, y, p) =_{f(x) =_B f(y)} q$.
Equivalently, if the dependent type theory also has existential quantifiers, then $x:A \vdash f(x):B$ is an embedding if there is a family of elements
which states that for all $y:B$, if there exists an element $x:A$ such that $f(x) =_B y$, then that element is unique up to identity.
A morphism $U \to X$ of topological spaces is a regular monomorphism precisely if this is an injection such that the topology on $U$ is the induced topology. This is an embedding of topological spaces.
Last revised on July 6, 2023 at 20:31:16. See the history of this page for a list of all contributions to it.