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 and a subset of , the preimage (sometimes also called the inverse image, though that may mean something different) of under is a subset of , consisting of those arguments whose values belong to .
That is,
A traditional notation for is , but this can conflict with the notation for an inverse function of (which indeed might not even exist). In fact is borrowed from a notation for pullbacks; indeed, a preimage is an example of a pullback:
Notice also that may be regarded as an operator between power sets. Power sets are exponential objects in the topos ; under this identification the pre-image operator is thereby identified with the map (variously called “pulling back along or substituting along ) obtained by currying the composite map
The appearance of the asterisk as a superscript in serves as a reminder of the contravariance of the map . Similarly, one uses a subscript notation such as (or sometimes ) for the direct image, considered as an operator in the covariant direction.
Naturally all of this generalizes to the context of toposes, where the set is replaced by the subobject classifier and , with a pullback description similar to the above.
interactions of images and pre-images with unions and intersections:
As emphasized by Lawvere, the quantifiers are vastly generalized by the concept of enriched Kan extensions which provide left and right adjoints to pulling-back operators for -enriched functors .
For partial endofunctions, one could also consider iterating the construction of the preimage of the partial endofunction.
For every set and subset , let be a function from the subset to . Given any subset , the preimage by definition is a subset of and thus a subset of . One could restrict the domain of to and the codomain of to , and find the preimage of under , or the 2-fold iterated preimage of under :
One could repeat this definition indefinitely, which could be formalised by the indexed sets representing the -fold iterated preimage of under .
and for ,
One example of an iterated preimage is the set of iterated differentiable functions and the iterated continuously differentiable functions , which are the -th iterated preimage of all functions and pointwise continuous functions on the real numbers under the derivative/Newton-Leibniz operator respectively.
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 and subset , let be a function from the subset to . Given any subset , the infinitely iterated preimage is defined as the largest subset such that the preimage of under is itself.
One example of an infinitely iterated preimage is the set of smooth functions , which is the infinitely iterated preimage of pointwise continuous functions under the derivative/Newton-Leibniz operator.
For a generalisation to sheaves, see inverse image.
Last revised on June 17, 2022 at 23:04:30. See the history of this page for a list of all contributions to it.