preimage (changes) in nLab
Showing changes from revision #11 to #12: Added | Removed | Changed
Context
Type theory
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = \linebreak propositions as types +programs as proofs +relation type theory/category theory
Contents
Definition
Given a function f:X→Yf: X \to Y and a subset SS of YY, the preimage (sometimes also called the inverse image, though that may mean something different) of SS under ff is a subset of XX, consisting of those arguments whose values belong to SS.
That is,
f *(S)={a:X|f(a)∈S}. f^*(S) = \{ a: X \;|\; f(a) \in S \} .
A traditional notation for f *f^* is f −1f^{-1}, but this can conflict with the notation for an inverse function of ff (which indeed might not even exist). In fact f *f^\ast is borrowed from a notation for pullbacks; indeed, a preimage is an example of a pullback:
f *(S) ↪ X ↓ (pb) ↓f S ↪ Y\array{ f^\ast(S) & \hookrightarrow & X \\ \downarrow & (pb) & \downarrow \mathrlap{f} \\ S & \hookrightarrow & Y }
Notice also that f *f^\ast may be regarded as an operator P(Y)→P(X)P(Y) \to P(X) between power sets. Power sets P(X)P(X) are exponential objects 2 X2^X in the topos SetSet; under this identification the pre-image operator f *f^\ast is thereby identified with the map 2 f:2 Y→2 X2^f: 2^Y \to 2^X (variously called “pulling back along ff or substituting along ff) obtained by currying the composite map
2 Y×X→1×f2 Y×Y→eval2.2^Y \times X \stackrel{1 \times f}{\to} 2^Y \times Y \stackrel{eval}{\to} 2.
The appearance of the asterisk as a superscript in f *f^\ast serves as a reminder of the contravariance of the map f↦f *=2 ff \mapsto f^\ast = 2^f. Similarly, one uses a subscript notation such as f *f_* (or sometimes f !f_!) for the direct image, considered as an operator f *:2 X→2 Yf_\ast: 2^X \to 2^Y in the covariant direction.
Naturally all of this generalizes to the context of toposes, where the set 22 is replaced by the subobject classifier Ω\Omega and f *=Ω ff^\ast = \Omega^f, with a pullback description similar to the above.
Properties
-
interactions of images and pre-images with unions and intersections:
- pre-images preserve unions and intersections (a general reason for this being that unions are colimits, intersections are limits, and f *f^\ast is simultaneously a left- and a right-adjoint: f *f^\ast is right-adjoint to the existential quantifier ∃ f\exists_f and left-adjoint to the universal quantifier ∀ f\forall_f)
As emphasized by Lawvere, the quantifiers ∃ f,∀ f\exists_f, \forall_f are vastly generalized by the concept of enriched Kan extensions which provide left and right adjoints to pulling-back operators V f:V D→V CV^f: V^D \to V^C for VV-enriched functors f:C→Df: C \to D.
Iterated preimages
For partial endofunctions, one could also consider iterating the construction of the preimage of the partial endofunction.
For every set TT and subset S⊆TS \subseteq T, let f:S→Tf:S \to T be a function from the subset SS to TT. Given any subset R⊆TR \subseteq T, the preimage f −1(R)f^{-1}(R) by definition is a subset of SS and thus a subset of TT. One could restrict the domain of ff to f −1(R)f^{-1}(R) and the codomain of ff to RR, and find the preimage of f −1(R)f^{-1}(R) under ff, or the 2-fold iterated preimage of RR under ff:
f −2(R)≔{x∈S|∃b∈f −1(R).f(x)=b}f^{-2}(R) \coloneqq \{x \in S \vert \exists b \in f^{-1}(R).f(x) = b\}
One could repeat this definition indefinitely, which could be formalised by the indexed sets f −n(R)f^{-n}(R) representing the nn-fold iterated preimage of RR under ff.
f −0(R)≔Rf^{-0}(R) \coloneqq R
and for n∈ℕn \in \mathbb{N},
f −(n+1)(S)≔{x∈S|∃b∈f −(n)(R).f(x)=b}f^{-(n+1)}(S) \coloneqq \{x \in S \vert \exists b \in f^{-(n)}(R).f(x) = b\}
One example of an iterated preimage is the set of iterated differentiable functions and the iterated continuously differentiable functions C n(ℝ)C^n(\mathbb{R}), which are the nn-th iterated preimage of all functions and pointwise continuous functions on the real numbers under the derivative/Newton-Leibniz operator respectively.
Infinitely iterated preimages
The above definition of an iterated preimage is inductive; one could also consider the coinductive version of above. This leads to infinitely iterated preimages:
For every set TT and subset S⊆TS \subseteq T, let f:S→Tf:S \to T be a function from the subset SS to TT. Given any subset R⊆TR \subseteq T, the infinitely iterated preimage is defined as the largest subset f −∞(R)⊆Tf^{-\infty}(R) \subseteq T such that the preimage of f −∞(R)f^{-\infty}(R) under ff is f −∞(R)f^{-\infty}(R) itself.
One example of an infinitely iterated preimage is the set of smooth functions C ∞(ℝ)C^\infty(\mathbb{R}), which is the infinitely iterated preimage of pointwise continuous functions under the derivative/Newton-Leibniz operator.
For a generalisation to sheaves, see inverse image.
References
- F. William Lawvere, Metric spaces, generalized logic and closed categories, TAC Reprint, 1986. Web.
Last revised on June 17, 2022 at 23:04:30. See the history of this page for a list of all contributions to it.