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 a generalisation to sheaves, see inverse image.
Last revised on July 2, 2017 at 11:18:18. See the history of this page for a list of all contributions to it.