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
There is a battery of little set-theoretic lemmas which inevitably recur when laying the foundations of core mathematics, as when teaching the standard curriculum that includes basic topology, real analysis, algebra, and so forth. In this article we collect some of those core results having to do with the properties of image and pre-image operators, especially regarding their preservation (or not) of set-theoretic operations like unions and intersections.
The attitude and approach of the mathematics professor toward such routine bread-and-butter issues is a matter of some interest. A professional, upon being presented with any one of these “naive set theory” propositions, will probably be able to verify it on the spot using ordinary follow-your-nose logic, driven by the definitions. While being able to produce such verifications is part of basic training in mathematics, it is not quite the same as giving an explanation, and in fact even good mathematicians trained this way may struggle to remember “now which is it that direct images preserve, unions or intersections?”1
A strong pedagogy would not only instill this sort of basic training, but make the battery of routine results more memorable by concentrating their essence in one or two basic principles that provide an explanatory basis for the rest. According to Lawvere 69, Lawvere 05, logic is an interlocking system of certain types of adjoint functors, and we believe putting those adjoint relationships front and center and seeing how the rest flows from them is an effective way to arrange the facts.
(images preserve unions but not in general intersections)
Let be a function between sets. Let be an indexed set of subsets of . Then
(the image under of a union of subsets is the union of the images)
(the image under of the intersection of the subsets is contained in the intersection of the images).
The injection in the second item is in general proper. If is an injective function then this is a bijection:
provided that is inhabited.
(pre-images preserve unions and intersections)
Let be a function between sets. Let be an indexed set of subsets of . Then
(the pre-image under of a union of subsets is the union of the pre-images),
(the pre-image under of the intersection of the subsets is the intersection of the pre-images).
(projection formula) Let be a function between sets. Let be a subset of , and be a subset of . Then
The properties 1., 2. of Proposition may be proved by appeal to fundamental relationships between direct image and inverse image and the like, which category theorists call adjunctions (similar in form to adjoints in linear algebra). The advantage of this type of proof is that, despite its utter simplicity, it generalizes to much wider contexts (beyond elementary classical set theory).
The first such relationship is:
(preimage is right adjoint to image)
For all subsets and , we have
One says in this situation that the direct image mapping is left adjoint to the inverse image mapping (with respect to the posets of subsets, regarded as (0,1)-categories), or that inverse image is right adjoint to direct image. This terminology is guided by the formally similar usage in linear algebra where linear mappings and are adjoint if one has an equation
for all in suitable inner product spaces (and in fact the analogy is not idle; see for instance Baez 1997).
In that case, we have the following elementary inferences:
where the first and third lines use the defining property of unions. Then, putting and reasoning forward, we get . On the other hand, putting and reasoning backward, we get . These two inclusions together give .
The dual of this proof immediately gives the fact that inverse images preserve arbitrary intersections, but let us spell it out directly:
and again by using the reasoning forward/backward trick, we infer .
The “reasoning forward/backward trick” may be summarized by saying that in a poset, we have iff (), or dually that iff (). This trick is vastly extrapolated by the Yoneda lemma.
People who work with categorial forms of logic denote direct images by . The suggestion is to view existential quantification as corresponding to taking of a direct image. For example, given a property of pairs , i.e. a subset where we write to say holds, the set of such that holds is exactly the direct image under the projection map . This suggests furthermore a useful extended meaning of existential quantification, by considering direct images along more general maps, not just projection maps. With this in mind, category theorists often denote by , giving an operator between power sets. This is left adjoint to the taking of inverse images as an operator , also denoted by . The adjointness relationship between direct image and inverse image, denoted by , is an example of a famous slogan due to Lawvere: “Logical quantification is adjoint to substitution” (with resonances far beyond the purview of logic as ordinarily conceived; see Remark ).
As for direct images and intersections, we have
because this is equivalent to , which is obvious because for all , we have , and if .
This inclusion is not usually an equality. For example, in the cartesian space with -coordinates, the projection does not preserve the intersection of the lines and .
However, if is injective, then the direct image operator does preserve intersections of subsets indexed over nonempty sets . This is not difficult to check once we verify that
For any map (not necessarily injective) and any subset , we have .
If is injective, then for any subset we have .
For then, if and is inhabited, we have for some that , and then
which was to be shown.
As for the statement that inverse images of unions are unions of inverse images, it turns out this follows from a second fundamental logical adjunction. For a function and a subset , define
which is analogous to the formula in Remark . (Alternatively, in classical logic where the negation operator on power sets means complementation, we have .) Then it is easy to verify a second adjunction
The same adjointness proof as used to prove property 1., then shows that the left adjoint part which here is the inverse image operator preserves unions, and that right adjoint part which here is the “codirect image” operator preserves intersections.
In terms of some more category theory jargon the above situation may be phrased as follows:
Subsets of some set are the (-1)-truncated objects in the slice category of Set over . Since Set is a topos, every morphism, i.e. function induces a base change adjoint triple
Here in the language of type theory
the left adjoint is also called the dependent sum
the middle morphism is also called context extension
the right adjoint is also called the dependent product.
All this restricts to the (-1)-truncated objects by composing the left adjoint with (-1)-truncation. Then one also says that we are looking at a morphism in a hyperdoctrine and (under “propositions as types”) may think of
the left adjoint as the existential quantifier
the right adjoint as the universal quantifier .
Now the fact that left adjoint preserves unions is the fact that left adjoints preserve colimits, and the fact that the left- and right adjoint preserves unions and intersections is that in addition right adjoints preserve limits.
Another useful formula for interactions between images and pre-images and intersections is the projection formula:
(e.g. Lee 2000, Ex. A.4(k))
First observe that we have an inclusion:
By the defining property of intersections, it suffices to show (i) and (ii) . Here (i) follows since , and implies . and (ii) is seen as
where the first step is the functoriality of images with respect to subset inclusions, and the second step is the adjunct of with respect to the adjunction between direct and inverse image.
Now to see that this inclusion is actually an equality…
The two ways of consecutively forming images and preimages along maps that form a pullback diagram coincide according to Prop. below – a simple example of what is known as a “Beck-Chevalley condition”.
First to recall our notation: As above, for a set , we write for its power set regarded as a poset, meaning that
is the set of subsets ,
regarded as a category by declaring that there is a morphisms precisely if as subsets of .
Then for a function between sets, we obtain the follows three functors between their power sets:
forms images under
forms preimages under ,
forms the complement of images of complements.
As discussed above, these three functors constitute an adjoint triple
In particular, the familiar/evident fact that forming images and preimages preserves unions may be understood as a special case of the fact that left adjoints preserve colimits.
(Beck-Chevalley condition for pre-/images)
Given a pullback diagram in Set
then consecutively forming (pre)images along these maps satisfies a Beck-Chevalley condition in that the following diagram of poset-homomorphisms (functors) commutes:
To see this it is sufficient to check commutativity on singleton-subsets (because every other subset is a union of singletons and, as just remarked, images and preimages preserve unions) and given a singleton set on an element , we directly compute as follows:
Here it is the first two steps which make use of the assumption that (1) is a pullback square, namely which means that is compatibly bijective to the fiber product of with over :
Textbook accounts include:
Tom Apostol, p. 44 in: Mathematical Analysis 1973 (pdf)
John M. Lee, Exercise A.4 in: Introduction to topological manifolds. Graduate Texts in Mathematics 202 (2000), Springer. ISBN: 0-387-98759-2, 0-387-95026-5.
Second edition: Springer, 2011. ISBN: 978-1-4419-7939-1 (doi:10.1007/978-1-4419-7940-7, errata pdf)
The slogan of Lawvere on logic and adjoint functors appears in
based on
The story of Lebesgue’s slip that projections commute with intersections, in attempting to prove that projections of Borel sets are Borel, is well explained here:
The analogy between adjoint functors and adjoints in linear algebra becomes very strong when jacking up from Hilbert spaces to 2-Hilbert spaces. See
There is a famous story of how Suslin discovered an error in an argument of Lebesgue, concerning just this type of routine set-theoretic detail (that Lebesgue perhaps just misremembered). In response, Suslin was led to develop some of the basics of descriptive set theory. Details of the story have been told by Dave Renfro, here and here ↩
Last revised on February 8, 2024 at 07:02:54. See the history of this page for a list of all contributions to it.