nLab
interactions of images and pre-images with unions and intersections

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

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

syntax object language

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type

falseinitial objectempty type

proposition(-1)-truncated objecth-proposition, mere proposition

proofgeneralized elementprogram

cut rulecomposition of classifying morphisms / pullback of display mapssubstitution

cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction

introduction rule for implicationunit for hom-tensor adjunctioneta conversion

logical conjunctionproductproduct type

disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)

implicationinternal homfunction type

negationinternal hom into initial objectfunction type into empty type

universal quantificationdependent productdependent product type

existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)

equivalencepath space objectidentity type

equivalence classquotientquotient type

inductioncolimitinductive type, W-type, M-type

higher inductionhigher colimithigher inductive type

completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set

setinternal 0-groupoidBishop set/setoid

universeobject classifiertype of types

modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)

linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation

proof netstring diagramquantum circuit

(absence of) contraction rule(absence of) diagonalno-cloning theorem

synthetic mathematicsdomain specific embedded programming language

</table>

homotopy levels

semantics

Contents

Introduction

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.

Statements

Proposition

(images preserve unions but not in general intersections)

Let f:XYf \colon X \longrightarrow Y be a function between sets. Let {S iX} iI\{S_i \subset X\}_{i \in I} be a set of subsets of XX. Then

  1. im f(iIS i)=(iIim f(S i))im_f\left( \underset{i \in I}{\cup} S_i\right) = \left(\underset{i \in I}{\cup} im_f(S_i)\right) (the image under ff of a union of subsets is the union of the images)

  2. im f(iIS i)(iIim f(S i))im_f\left( \underset{i \in I}{\cap} S_i\right) \subset \left(\underset{i \in I}{\cap} im_f(S_i)\right) (the image under ff 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 ff is an injective function then this is a bijection:

  • (finjective)(im f(iIS i)=(iIim f(S i)))(f\,\text{injective}) \Rightarrow \left(im_f\left( \underset{i \in I}{\cap} S_i\right) = \left(\underset{i \in I}{\cap} im_f(S_i)\right)\right)

provided that II is inhabited.

Proposition

(pre-images preserve unions and intersections)

Let f:XYf \colon X \longrightarrow Y be a function between sets. Let {T iY} iI\{T_i \subset Y\}_{i \in I} be a set of subsets of YY. Then

  1. f 1(iIT i)=(iIf 1(T i))f^{-1}\left( \underset{i \in I}{\cup} T_i\right) = \left(\underset{i \in I}{\cup} f^{-1}(T_i)\right) (the pre-image under ff of a union of subsets is the union of the pre-images),

  2. f 1(iIT i)=(iIf 1(T i))f^{-1}\left( \underset{i \in I}{\cap} T_i\right) = \left(\underset{i \in I}{\cap} f^{-1}(T_i)\right) (the pre-image under ff of the intersection of the subsets is contained in the intersection of the pre-images).

Proposition

(projection formula) Let f:XYf: X \longrightarrow Y be a function between sets. Let SXS \subset X be a subset of XX, and TYT \subseteq Y be a subset of YY. Then

f(S)T=f(Sf 1(T)).f(S) \cap T = f(S \cap f^{-1}(T)).

Proofs via adjoints

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).

Direct images preserve unions, inverse images preserve intersections

The first such relationship is that, for all subsets SXS \subseteq X and TYT \subseteq Y, we have

f(S)TiffSf 1(T)f(S) \subseteq T \qquad iff \qquad S \subseteq f^{-1}(T)

One says in this situation that the direct image mapping f()f(-) is left adjoint to the inverse image mapping f 1()f^{-1}(-), 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 AA and BB are adjoint if one has an equation

Ax,y=x,By\langle A x, y \rangle = \langle x, B y \rangle

for all x,yx, y in suitable inner product spaces (and in fact the analogy is not idle; see for instance Baez).

In that case, we have the following elementary inferences:

iIf(S i)T iff ( iI)f(S i)T iff ( iI)S if 1(T) iff iIS if 1(T) iff f( iIS i)T\array{ \bigcup_{i \in I} f(S_i) \subseteq T & iff & (\forall_{i \in I})\; f(S_i) \subseteq T \\ & iff & (\forall_{i \in I})\; S_i \subseteq f^{-1}(T) \\ & iff & \bigcup_{i \in I} S_i \subseteq f^{-1}(T) \\ & iff & f\left(\bigcup_{i \in I} S_i\right) \subseteq T }

where the first and third lines use the defining property of unions. Then, putting T= iIf(S i)T = \bigcup_{i \in I} f(S_i) and reasoning forward, we get f( iIS i) iIf(S i)f\left(\bigcup_{i \in I} S_i\right) \subseteq \bigcup_{i \in I} f(S_i). On the other hand, putting T=f( iIS i)T = f\left(\bigcup_{i \in I} S_i\right) and reasoning backward, we get iIf(S i)f( iIS i)\bigcup_{i \in I} f(S_i) \subseteq f\left(\bigcup_{i \in I} S_i\right). These two inclusions together give iIf(S i)=f( iIS i)\bigcup_{i \in I} f(S_i) = f\left(\bigcup_{i \in I} S_i\right).

The dual of this proof immediately gives the fact that inverse images preserve arbitrary intersections, but let us spell it out directly:

S iIf 1(T i) iff ( iI)Sf 1(T i) iff ( iI)f(S)T i iff f(S) iIT i iff Sf 1( iIT i)\array{ S \subseteq \bigcap_{i \in I} f^{-1}(T_i) & iff & (\forall_{i \in I})\; S \subseteq f^{-1}(T_i) \\ & iff & (\forall_{i \in I})\; f(S) \subseteq T_i \\ & iff & f(S) \subseteq \bigcap_{i \in I} T_i \\ & iff & S \subseteq f^{-1}\left(\bigcap_{i \in I} T_i \right) }

and again by using the reasoning forward/backward trick, we infer iIf 1(T i)=f 1( iIT i)\bigcap_{i \in I} f^{-1}(T_i) = f^{-1}\left(\bigcap_{i \in I} T_i\right).

Remark

The “reasoning forward/backward trick” may be summarized by saying that in a poset, we have A=BA = B iff (ATBTA \leq T \Leftrightarrow B \leq T), or dually that A=BA = B iff (SASBS \leq A \Leftrightarrow S \leq B). This trick is vastly extrapolated by the Yoneda lemma.

Remark

People who work with categorial forms of logic denote direct images f(S)f(S) by f(S)\exists_f(S). The suggestion is to view existential quantification as corresponding to taking of a direct image. For example, given a property PP of pairs (x,y)(x, y), i.e. a subset PX×YP \subseteq X \times Y where we write P(x,y)P(x, y) to say (x,y)P(x, y) \in P holds, the set of yy such that ( xX)P(x,y)(\exists_{x \in X})\; P(x, y) holds is exactly the direct image π 2(P)\pi_2(P) under the projection map π 2:X×YY\pi_2: X \times Y \to Y. 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 f(S)={yY:( x:f(x)=y)xS}f(S) = \{y \in Y: (\exists_{x: f(x) = y})\; x \in S\} by f(S)\exists_f(S), giving an operator f:P(X)P(Y)\exists_f: P(X) \to P(Y) between power sets. This is left adjoint to the taking of inverse images Tf 1(T)T \mapsto f^{-1}(T) as an operator f 1:P(Y)P(X)f^{-1}: P(Y) \to P(X), also denoted by f *:P(Y)P(X)f^\ast: P(Y) \to P(X). The adjointness relationship between direct image and inverse image, denoted by ff *\exists_f \dashv f^\ast, 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

f( iIS i) iIf(S i)f\left(\bigcap_{i \in I} S_i\right) \subseteq \bigcap_{i \in I} f(S_i)

because this is equivalent to ( iI)f( iIS i)f(S i)(\forall_{i \in I})\; f\left(\bigcap_{i \in I} S_i\right) \subseteq f(S_i), which is obvious because for all iIi \in I, we have iIS iS i\bigcap_{i \in I} S_i \subseteq S_i, and f(A)f(B)f(A) \subseteq f(B) if ABA \subseteq B.

This inclusion is not usually an equality. For example, in the cartesian space 2\mathbb{R}^2 with xyx y-coordinates, the projection (x,y)x(x, y) \mapsto x does not preserve the intersection of the lines y=1y = 1 and y=2y = 2.

However, if f:XYf: X \to Y is injective, then the direct image operator Sf(S)S \mapsto f(S) does preserve intersections of subsets (S i) iI(S_i)_{i \in I} indexed over nonempty sets II. This is not difficult to check once we verify that

  • For any map f:XYf: X \to Y (not necessarily injective) and any subset TYT \subseteq Y, we have f(X)T=f(f 1(T))f(X) \cap T = f(f^{-1}(T)).

  • If ff is injective, then for any subset SXS \subseteq X we have S=f 1(f(S))S = f^{-1}(f(S)).

For then, if T= iIf(S i)T = \bigcap_{i \in I} f(S_i) and II is inhabited, we have for some ii that Tf(S i)f(X)T \subseteq f(S_i) \subseteq f(X), and then

T=f(X)T = f(f 1(T)) = f(f 1( if(S i))) = f( iIf 1(f(S i))) = f( iIS i)\array{ T = f(X) \cap T & = & f(f^{-1}(T)) \\ & = & f(f^{-1}(\bigcap_i f(S_i))) \\ & = & f\left(\bigcap_{i \in I} f^{-1}(f(S_i))\right) \\ & = & f\left(\bigcap_{i \in I} S_i\right) }

which was to be shown.

Inverse images preserve unions, codirect images preserve intersections

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 f:XYf: X \to Y and a subset UXU \subseteq X, define

f(U)={yY:( x:f(x)=y)xU}\forall_f(U) = \{y \in Y: (\forall_{x: f(x) = y})\; x \in U\}

which is analogous to the formula f(S)=f(S)={yY:( x:f(x)=y)xS}\exists_f(S) = f(S) = \{y \in Y: (\exists_{x: f(x) = y})\; x \in S\} in Remark . (Alternatively, in classical logic where the negation operator ¬\neg on power sets means complementation, we have f=¬ f¬\forall_f = \neg \exists_f \neg.) Then it is easy to verify a second adjunction

f 1(T)UiffT f(U)f^{-1}(T) \subseteq U \qquad iff \qquad T \subseteq \forall_f (U)

The same adjointness proof as used to prove property 1., then shows that the left adjoint part which here is the inverse image operator f 1=f *:P(Y)P(X)f^{-1} = f^\ast: P(Y) \to P(X) preserves unions, and that right adjoint part which here is the “codirect image” operator f:P(X)P(Y)\forall_f: P(X) \to P(Y) preserves intersections.

Remark

In terms of some more category theory jargon the above situation may be phrased as follows:

Subsets of some set SS are the (-1)-truncated objects in the slice category Set /SSet_{/S} of Set over SS. Since Set is a topos, every morphism, i.e. function XYX \longrightarrow Y induces a base change adjoint triple

Set /Xf *f *f !Set /Y. Set_{/X} \underoverset {\underset{f^\ast}{\longrightarrow}} {\overset{f_!}{\longrightarrow}} {\overset{f_\ast}{\longleftarrow}} Set_{/Y} \,.

Here in the language of type theory

  1. the left adjoint f !f_! is also called the dependent sum

  2. the middle morphism is also called context extension

  3. the right adjoint f *f_\ast 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

  1. the left adjoint f !f_! as the existential quantifier f\exists_f

  2. the right adjoint f *f_\ast as the universal quantifier f\forall_f.

Now the fact that left adjoint f\exists_f preserves unions is the fact that left adjoints preserve colimits, and the fact that the left- and right adjoint f *f^\ast preserves unions and intersections is that in addition right adjoints preserve limits.

Projection formula

Another useful formula for interactions between images and pre-images and intersections is the projection formula:

Proposition

Let f:XYf: X \to Y be a function, and let SX,TYS \subseteq X, T \subseteq Y be subsets. Then f(S)T=f(Sf 1(T))f(S) \cap T = f(S \cap f^{-1}(T)).

Proof

The easy direction is the inclusion f(Sf 1(T))f(S)Tf(S \cap f^{-1}(T)) \subseteq f(S) \cap T: by the defining property of intersections, it suffices to show f(Sf 1(T))f(S)f(S \cap f^{-1}(T)) \subseteq f(S) and f(Sf 1(T))Tf(S \cap f^{-1}(T)) \subset T. The first is clear since Sf 1(T)SS \cap f^{-1}(T) \subseteq S, and ABA \subseteq B implies f(A)f(B)f(A) \subseteq f(B). Similarly, f(Sf 1(T))f(f 1(T))f(S \cap f^{-1}(T)) \subseteq f(f^{-1}(T)), and f(f 1(T))Tf(f^{-1}(T)) \subseteq T since this is equivalent to f 1(T)f 1(T)f^{-1}(T) \subseteq f^{-1}(T) by the adjunction between direct and inverse image.

To be continued.

References

The slogan of Lawvere on logic and adjoint functors appears in

  • F. William Lawvere, An elementary theory of the category of sets, Proceedings of the National Academy of Science of the U.S.A 52 (1965), 1506-1511. Reprinted in an expanded version, with commentary by Colin McLarty and by Lawvere, in Reprints in Theory and Applications of Categories, No. 11 (2005), pp. 1-35. (link)

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:

  • Dave L. Renfro, Mikhail Y. Suslin and Lebesgue’s error, two Mathforum posts dated July 29, 2006 (first post 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


  1. 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 July 2, 2017 at 10:23:47. See the history of this page for a list of all contributions to it.