preimage

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

Given a function $f: X \to Y$ and a subset $S$ of $Y$, the **preimage** (sometimes also called the **inverse image**, though that may mean something different) of $T$ under $f$ is a subset of $S$, consisting of those arguments whose values belong to $S$.

That is,

$f^*(S) = \{ a: X \;|\; f(a) \in S \} .$

The traditional notation for $f^*$ is $f^{-1}$, but this can conflict the notation for an inverse function of $f$ (which indeed might not even exist). This then suggests $f_*$ for the image of $f$.

We borrow $f^*$ from a notation for pullbacks, and indeed a preimage is an example of a pullback:

$\array {
f^*(S) & \hookrightarrow & X \\
\downarrow & & \downarrow f \\
S & \hookrightarrow & Y
}$

For a generalisation to sheaves, see inverse image.

Revised on May 20, 2017 13:22:16
by Urs Schreiber
(92.218.150.85)