4.6.3 Codirect Images

    Let $f\colon X\to Y$ be a function.

    The codirect image function associated to $f$ is the function

    \[ f_{*}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

    defined by1,2

    \begin{align*} f_{*}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ y\in Y\ \middle |\ \begin{aligned} & \text{for each $x\in X$, if we have}\\ & \text{$f\webleft (x\webright )=y$, then $x\in U$}\end{aligned} \right\} \\ & = \left\{ y\in Y\ \middle |\ \text{we have $f^{-1}\webleft (y\webright )\subset U$}\right\} \end{align*}

    for each $U\in \mathcal{P}\webleft (X\webright )$.


    1. 1Further Terminology: The set $f_{*}\webleft (U\webright )$ is called the codirect image of $U$ by $f$.
    2. 2We also have
      \begin{align*} f_{*}\webleft (U\webright ) & = f_{!}\webleft (U^{\textsf{c}}\webright )^{\textsf{c}}\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}Y\setminus f_{!}\webleft (X\setminus U\webright );\end{align*}
      see Item 16 of Proposition 4.6.3.1.7.

    Sometimes one finds the notation

    \[ \forall _{f}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

    for $f_{!}$. This notation comes from the fact that the following statements are equivalent, where $y\in Y$ and $U\in \mathcal{P}\webleft (X\webright )$:

    • We have $y\in \forall _{f}\webleft (U\webright )$.

    • For each $x\in X$, if $y=f\webleft (x\webright )$, then $x\in U$.

    We will not make use of this notation elsewhere in Clowder.

    Identifying $\mathcal{P}\webleft (X\webright )$ with $\mathsf{Sets}\webleft (X,\{ \mathsf{t},\mathsf{f}\} \webright )$ via Item 2 of Proposition 4.5.1.1.4, we see that the codirect image function associated to $f$ is equivalently the function

    \[ f_{*}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright ) \]

    defined by

    \begin{align*} f_{*}\webleft (\chi _{U}\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\operatorname {\mathrm{Ran}}_{f}\webleft (\chi _{U}\webright )\\ & = \operatorname*{\operatorname {\mathrm{lim}}}\webleft (\webleft (\underline{\webleft (-_{1}\webright )}\mathbin {\overset {\to }{\times }}f\webright )\overset {\operatorname {\mathrm{\mathrm{pr}}}}{\twoheadrightarrow }X\overset {\chi _{U}}{\to }\{ \mathsf{true},\mathsf{false}\} \webright )\\ & = \operatorname*{\operatorname {\mathrm{lim}}}_{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=-_{1} \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=-_{1} \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright ).\end{align*}

    where we have used Unresolved reference, Unresolved reference for the second equality. In other words, we have

    \begin{align*} \webleft [f_{*}\webleft (\chi _{U}\webright )\webright ]\webleft (y\webright ) & = \bigwedge _{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=y \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \begin{cases} \mathsf{true}& \text{if, for each $x\in X$ such that}\\ & \text{$f\webleft (x\webright )=y$, we have $x\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & = \begin{cases} \mathsf{true}& \text{if $f^{-1}\webleft (y\webright )\subset U$}\\ \mathsf{false}& \text{otherwise} \end{cases}\end{align*}

    for each $y\in Y$.

    Let $U$ be a subset of $X$.1,2

    1. 1.

      The image part of the codirect image $f_{*}\webleft (U\webright )$ of $U$ is the set $f_{*,\mathrm{im}}\webleft (U\webright )$ defined by

      \begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U\webright )\cap \mathrm{Im}\webleft (f\webright )\\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{we have $f^{-1}\webleft (y\webright )\subset U$}\\ & \text{and $f^{-1}\webleft (y\webright )\neq \text{Ø}$.} \end{aligned}\right\} .\end{align*}
    2. 2.

      The complement part of the codirect image $f_{*}\webleft (U\webright )$ of $U$ is the set $f_{*,\mathrm{cp}}\webleft (U\webright )$ defined by

      \begin{align*} f_{*,\mathrm{cp}}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (U\webright )\cap \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\\ & = Y\setminus \mathrm{Im}\webleft (f\webright )\\ & = \left\{ y\in Y\ \middle |\ \begin{aligned} & \text{we have $f^{-1}\webleft (y\webright )\subset U$}\\ & \text{and $f^{-1}\webleft (y\webright )=\text{Ø}$.} \end{aligned}\right\} \\ & = \left\{ y\in Y\ \middle |\ f^{-1}\webleft (y\webright )=\text{Ø}\right\} .\end{align*}


    1. 1Note that we have
      \[ f_{*}\webleft (U\webright )=f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright ), \]
      as
      \begin{align*} f_{*}\webleft (U\webright ) & = f_{*}\webleft (U\webright )\cap Y\\ & = f_{*}\webleft (U\webright )\cap \webleft (\mathrm{Im}\webleft (f\webright )\cup \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\webright )\\ & = \webleft (f_{*}\webleft (U\webright )\cap \mathrm{Im}\webleft (f\webright )\webright )\cup \webleft (f_{*}\webleft (U\webright )\cap \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright )\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright ). \end{align*}
    2. 2In terms of the meet computation of $f_{*}\webleft (U\webright )$ of Remark 4.6.3.1.4, namely
      \[ f_{*}\webleft (\chi _{U}\webright ) =\bigwedge _{\substack {x\in X\\ f\webleft (x\webright )=-_{1}}}\webleft (\chi _{U}\webleft (x\webright )\webright ), \]
      we see that $\smash {f_{*,\mathrm{im}}}$ corresponds to meets indexed over nonempty sets, while $\smash {f_{*,\mathrm{cp}}}$ corresponds to meets indexed over the empty set.

    Here are some examples of codirect images.

    1. 1.

      Multiplication by Two. Consider the function $f\colon \mathbb {N}\to \mathbb {N}$ given by

      \[ f\webleft (n\webright ) \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}2n \]

      for each $n\in \mathbb {N}$. Since $f$ is injective, we have

      \begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & = f_{!}\webleft (U\webright )\\ f_{*,\mathrm{cp}}\webleft (U\webright ) & = \left\{ \text{odd natural numbers}\right\} \end{align*}

      for any $U\subset \mathbb {N}$. In particular, we have

      \[ f_{*}\webleft (\left\{ \text{even natural numbers}\right\} \webright )=\mathbb {N}. \]
    2. 2.

      Parabolas. Consider the function $f\colon \mathbb {R}\to \mathbb {R}$ given by

      \[ f\webleft (x\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x^{2} \]

      for each $x\in \mathbb {R}$. We have

      \[ f_{*,\mathrm{cp}}\webleft (U\webright )=\mathbb {R}_{<0} \]

      for any $U\subset \mathbb {R}$. Moreover, since $f^{-1}\webleft (x\webright )=\left\{ -\sqrt{x},\sqrt{x}\right\} $, we have e.g.:

      \begin{gather*} \begin{aligned} f_{*,\mathrm{im}}\webleft (\webleft [0,1\webright ]\webright ) & = \left\{ 0\right\} ,\\ f_{*,\mathrm{im}}\webleft (\webleft [-1,1\webright ]\webright ) & = \webleft [0,1\webright ],\\ f_{*,\mathrm{im}}\webleft (\webleft [1,2\webright ]\webright ) & = \text{Ø}, \end{aligned}\\ f_{*,\mathrm{im}}\webleft (\webleft [-2,-1\webright ]\cup \webleft [1,2\webright ]\webright ) = \webleft [1,4\webright ]. \end{gather*}
    3. 3.

      Circles. Consider the function $f\colon \mathbb {R}^{2}\to \mathbb {R}$ given by

      \[ f\webleft (x,y\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}x^{2}+y^{2} \]

      for each $\webleft (x,y\webright )\in \mathbb {R}^{2}$. We have

      \[ f_{*,\mathrm{cp}}\webleft (U\webright )=\mathbb {R}_{<0} \]

      for any $U\subset \mathbb {R}^{2}$, and since

      \[ f^{-1}\webleft (r\webright )= \begin{cases} \text{a circle of radius $r$ about the origin} & \text{if $r>0$,}\\ \left\{ \webleft (0,0\webright )\right\} & \text{if $r=0$,}\\ \text{Ø}& \text{if $r<0$,} \end{cases} \]

      we have e.g.:

      \begin{gather*} f_{*,\mathrm{im}}\webleft (\webleft [-1,1\webright ]\times \webleft [-1,1\webright ]\webright ) = \webleft [0,1\webright ],\\ f_{*,\mathrm{im}}\webleft (\webleft (\webleft [-1,1\webright ]\times \webleft [-1,1\webright ]\webright )\setminus \webleft [-1,1\webright ]\times \left\{ 0\right\} \webright ) = \text{Ø}. \end{gather*}

    Let $f\colon X\to Y$ be a function.

    1. 1.

      Functoriality. The assignment $U\mapsto f_{*}\webleft (U\webright )$ defines a functor

      \[ f_{*}\colon \webleft (\mathcal{P}\webleft (X\webright ),\subset \webright )\to \webleft (\mathcal{P}\webleft (Y\webright ),\subset \webright ). \]

      In particular, for each $U,V\in \mathcal{P}\webleft (X\webright )$, the following condition is satisfied:

      • (★)
      • If $U\subset V$, then $f_{*}\webleft (U\webright )\subset f_{*}\webleft (V\webright )$.
    2. 2.

      Triple Adjointness. We have a triple adjunction

      witnessed by:

      1. (a)

        Units and counits of the form

        \[ \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )} & \hookrightarrow f^{-1}\circ f_{!},\\ f_{!}\circ f^{-1} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )},\\ \end{aligned} \qquad \begin{aligned} \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (Y\webright )} & \hookrightarrow f_{*}\circ f^{-1},\\ f^{-1}\circ f_{*} & \hookrightarrow \operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )}, \end{aligned} \]

        having components of the form

        \[ \begin{gathered} U \subset f^{-1}\webleft (f_{!}\webleft (U\webright )\webright ),\\ f_{!}\webleft (f^{-1}\webleft (V\webright )\webright ) \subset V, \end{gathered} \qquad \begin{gathered} V \subset f_{*}\webleft (f^{-1}\webleft (V\webright )\webright ),\\ f^{-1}\webleft (f_{*}\webleft (U\webright )\webright ) \subset U \end{gathered} \]

        indexed by $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$.

      2. (b)

        Bijections of sets

        \begin{align*} \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (Y\webright )}\webleft (f_{!}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f^{-1}\webleft (V\webright )\webright ),\\ \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (f^{-1}\webleft (U\webright ),V\webright ) & \cong \operatorname {\mathrm{Hom}}_{\mathcal{P}\webleft (X\webright )}\webleft (U,f_{*}\webleft (V\webright )\webright ), \end{align*}

        natural in $U\in \mathcal{P}\webleft (X\webright )$ and $V\in \mathcal{P}\webleft (Y\webright )$ and (respectively) $V\in \mathcal{P}\webleft (X\webright )$ and $U\in \mathcal{P}\webleft (Y\webright )$. In particular:

        1. (i)

          The following conditions are equivalent:

  • (I)

    We have $f_{!}\webleft (U\webright )\subset V$.

  • (II)

    We have $U\subset f^{-1}\webleft (V\webright )$.

  • (ii)

    The following conditions are equivalent:

    1. (I)

      We have $f^{-1}\webleft (U\webright )\subset V$.

    2. (II)

      We have $U\subset f_{*}\webleft (V\webright )$.

  • 3.

    Interaction With Unions of Families of Subsets. The diagram

    commutes, i.e. we have

    \[ \bigcup _{U\in \mathcal{U}}f_{*}\webleft (U\webright )=\bigcup _{V\in f_{*}\webleft (\mathcal{U}\webright )}V \]

    for each $\mathcal{U}\in \mathcal{P}\webleft (X\webright )$, where $f_{*}\webleft (\mathcal{U}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f_{*}\webright )_{*}\webleft (\mathcal{U}\webright )$.

  • 4.

    Interaction With Intersections of Families of Subsets. The diagram

    commutes, i.e. we have

    \[ \bigcap _{U\in \mathcal{U}}f_{*}\webleft (U\webright )=\bigcap _{V\in f_{*}\webleft (\mathcal{U}\webright )}V \]

    for each $\mathcal{U}\in \mathcal{P}\webleft (X\webright )$, where $f_{*}\webleft (\mathcal{U}\webright )\mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\webleft (f_{*}\webright )_{*}\webleft (\mathcal{U}\webright )$.

  • 5.

    Interaction With Binary Unions. Let $f\colon X\to Y$ be a function. We have a natural transformation

    with components

    \[ f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright )\subset f_{*}\webleft (U\cup V\webright ) \]

    indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 6.

    Interaction With Binary Intersections. The diagram

    commutes, i.e. we have

    \[ f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright )=f_{*}\webleft (U\cap V\webright ) \]

    for each $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 7.

    Interaction With Complements. The diagram

    commutes, i.e. we have

    \[ f_{*}\webleft (U^{\textsf{c}}\webright )=f_{!}\webleft (U\webright )^{\textsf{c}} \]

    for each $U\in \mathcal{P}\webleft (X\webright )$.

  • 8.

    Interaction With Symmetric Differences. We have a natural transformation

    with components

    \[ f_{*}\webleft (U\mathbin {\triangle }V\webright )\subset f_{*}\webleft (U\webright )\mathbin {\triangle }f_{*}\webleft (V\webright ) \]

    indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 9.

    Interaction With Internal Homs of Powersets. We have a natural transformation

    with components

    \[ \webleft [f_{!}\webleft (U\webright ),f_{*}\webleft (V\webright )\webright ]_{Y}\subset f_{*}\webleft (\webleft [U,V\webright ]_{X}\webright ) \]

    indexed by $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 10.

    Lax Preservation of Colimits. We have an inclusion of sets

    \[ \bigcup _{i\in I}f_{*}\webleft (U_{i}\webright )\subset f_{*}\left(\bigcup _{i\in I}U_{i}\right), \]

    natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}\webleft (X\webright )^{\times I}$. In particular, we have inclusions

    \[ \begin{gathered} f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) \hookrightarrow f_{*}\webleft (U\cup V\webright ),\\ \text{Ø}\hookrightarrow f_{*}\webleft (\text{Ø}\webright ), \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 11.

    Preservation of Limits. We have an equality of sets

    \[ f_{*}\left(\bigcap _{i\in I}U_{i}\right)=\bigcap _{i\in I}f_{*}\webleft (U_{i}\webright ), \]

    natural in $\left\{ U_{i}\right\} _{i\in I}\in \mathcal{P}\webleft (X\webright )^{\times I}$. In particular, we have equalities

    \[ \begin{gathered} f^{-1}\webleft (U\cap V\webright ) = f_{*}\webleft (U\webright )\cap f^{-1}\webleft (V\webright ),\\ f_{*}\webleft (X\webright ) = Y, \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 12.

    Symmetric Lax Monoidality With Respect to Unions. The codirect image function of Item 1 has a symmetric lax monoidal structure

    \[ \webleft (f_{*},f^{\otimes }_{*},f^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (X\webright ),\cup ,\text{Ø}\webright ) \to \webleft (\mathcal{P}\webleft (Y\webright ),\cup ,\text{Ø}\webright ), \]

    being equipped with inclusions

    \[ \begin{gathered} f^{\otimes }_{*|U,V} \colon f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) \hookrightarrow f_{*}\webleft (U\cup V\webright ),\\ f^{\otimes }_{*|\mathbb {1}} \colon \text{Ø}\hookrightarrow f_{*}\webleft (\text{Ø}\webright ), \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 13.

    Symmetric Strict Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric strict monoidal structure

    \[ \webleft (f_{*},f^{\otimes }_{*},f^{\otimes }_{*|\mathbb {1}}\webright ) \colon \webleft (\mathcal{P}\webleft (X\webright ),\cap ,X\webright ) \to \webleft (\mathcal{P}\webleft (Y\webright ),\cap ,Y\webright ), \]

    being equipped with equalities

    \[ \begin{gathered} f^{\otimes }_{*|U,V} \colon f_{*}\webleft (U\cap V\webright ) \mathbin {\overset {=}{\rightarrow }}f_{*}\webleft (U\webright )\cap f_{*}\webleft (V\webright ),\\ f^{\otimes }_{*|\mathbb {1}} \colon f_{*}\webleft (X\webright ) \mathbin {\overset {=}{\rightarrow }}Y, \end{gathered} \]

    natural in $U,V\in \mathcal{P}\webleft (X\webright )$.

  • 14.

    Interaction With Coproducts. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. We have

    \[ \webleft (f\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g\webright )_{*}\webleft (U\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}V\webright )=f_{*}\webleft (U\webright )\mathchoice {\mathbin {\textstyle \coprod }}{\mathbin {\textstyle \coprod }}{\mathbin {\scriptstyle \textstyle \coprod }}{\mathbin {\scriptscriptstyle \textstyle \coprod }}g_{*}\webleft (V\webright ) \]

    for each $U\in \mathcal{P}\webleft (X\webright )$ and each $V\in \mathcal{P}\webleft (Y\webright )$.

  • 15.

    Interaction With Products. Let $f\colon X\to X'$ and $g\colon Y\to Y'$ be maps of sets. We have

    \[ \webleft (f\boxtimes _{X\times Y} g\webright )_{*}\webleft (U\boxtimes _{X\times Y}V\webright )=f_{*}\webleft (U\webright )\boxtimes _{X'\times Y'}g_{*}\webleft (V\webright ) \]

    for each $U\in \mathcal{P}\webleft (X\webright )$ and each $V\in \mathcal{P}\webleft (Y\webright )$.

  • 16.

    Relation to Direct Images. We have

    \begin{align*} f_{*}\webleft (U\webright ) & = f_{!}\webleft (U^{\textsf{c}}\webright )^{\textsf{c}}\\ & = Y\setminus f_{!}\webleft (X\setminus U\webright ) \end{align*}

    for each $U\in \mathcal{P}\webleft (X\webright )$.

  • 17.

    Interaction With Injections. If $f$ is injective, then we have

    \begin{gather*} f_{*,\mathrm{im}}\webleft (U\webright ) = f_{!}\webleft (U\webright ),\\ f_{*,\mathrm{cp}}\webleft (U\webright ) = Y\setminus \mathrm{Im}\webleft (f\webright ),\\ \end{gather*}

    and so

    \begin{align*} f_{*}\webleft (U\webright ) & = f_{*,\mathrm{im}}\webleft (U\webright )\cup f_{*,\mathrm{cp}}\webleft (U\webright )\\ & = f_{!}\webleft (U\webright )\cup \webleft (Y\setminus \mathrm{Im}\webleft (f\webright )\webright ) \end{align*}

    for each $U\in \mathcal{P}\webleft (X\webright )$.

  • 18.

    Interaction With Surjections. If $f$ is surjective, then we have

    \begin{align*} f_{*,\mathrm{im}}\webleft (U\webright ) & \subset f_{!}\webleft (U\webright ),\\ f_{*,\mathrm{cp}}\webleft (U\webright ) & = \text{Ø},\\ \end{align*}

    and so

    \[ f_{*}\webleft (U\webright )\subset f_{!}\webleft (U\webright ) \]

    for each $U\in \mathcal{P}\webleft (X\webright )$.

  • Item 1: Functoriality
    Omitted.

    Item 2: Triple Adjointness
    This follows from Remark 4.6.1.1.4, Remark 4.6.2.1.2, Remark 4.6.3.1.4, and Unresolved reference, Unresolved reference of Unresolved reference.

    Item 3: Interaction With Unions of Families of Subsets
    We have

    \begin{align*} \bigcup _{V\in f_{*}\webleft (\mathcal{U}\webright )}V & = \bigcup _{V\in \left\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcup _{U\in \mathcal{U}}f_{*}\webleft (U\webright ).\end{align*}

    This finishes the proof.

    Item 4: Interaction With Intersections of Families of Subsets
    We have

    \begin{align*} \bigcap _{V\in f_{*}\webleft (\mathcal{U}\webright )}V & = \bigcap _{V\in \left\{ f_{*}\webleft (U\webright )\in \mathcal{P}\webleft (X\webright )\ \middle |\ U\in \mathcal{U}\right\} }V\\ & = \bigcap _{U\in \mathcal{U}}f_{*}\webleft (U\webright ).\end{align*}

    This finishes the proof.

    Item 5: Interaction With Binary Unions
    We have

    \begin{align*} f_{*}\webleft (U\webright )\cup f_{*}\webleft (V\webright ) & = f_{!}\webleft (U^{\textsf{c}}\webright )^{\textsf{c}}\cup f_{!}\webleft (V^{\textsf{c}}\webright )^{\textsf{c}}\\ & = \webleft (f_{!}\webleft (U^{\textsf{c}}\webright )\cap f_{!}\webleft (V^{\textsf{c}}\webright )\webright )^{\textsf{c}}\\ & \subset \webleft (f_{!}\webleft (U^{\textsf{c}}\cap V^{\textsf{c}}\webright )\webright )^{\textsf{c}}\\ & = f_{!}\webleft (\webleft (U\cup V\webright )^{\textsf{c}}\webright )^{\textsf{c}}\\ & = f_{*}\webleft (U\cup V\webright ), \end{align*}

    where:

    1. 1.

      We have used Item 16 for the first equality.

    2. 2.

      We have used Item 2 of Proposition 4.3.11.1.2 for the second equality.

    3. 3.

      We have used Item 6 of Proposition 4.6.1.1.5 for the third equality.

    4. 4.

      We have used Item 2 of Proposition 4.3.11.1.2 for the fourth equality.

    5. 5.

      We have used Item 16 for the last equality.

    This finishes the proof.

    Item 6: Interaction With Binary Intersections
    This follows from Item 11.

    Item 7: Interaction With Complements
    Omitted.

    Item 8: Interaction With Symmetric Differences
    Omitted.

    Item 9: Interaction With Internal Homs of Powersets
    We have

    \begin{align*} \big [f_{!}\webleft (U\webright ),f^{!}\webleft (V\webright )\big ]_{X} & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{!}\webleft (U\webright )^{\textsf{c}}\cup f_{*}\webleft (V\webright )\\ & = f_{*}\webleft (U^{\textsf{c}}\webright )\cup f_{*}\webleft (V\webright )\\ & \subset f_{*}\webleft (U^{\textsf{c}}\cup V\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f_{*}\webleft (\webleft [U,V\webright ]_{X}\webright ), \end{align*}

    where we have used:

    1. 1.

      Item 7 of Proposition 4.6.3.1.7 for the second equality.

    2. 2.

      Item 5 of Proposition 4.6.3.1.7 for the inclusion.

    Since $\mathcal{P}\webleft (X\webright )$ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2). This finishes the proof.

    Item 10: Lax Preservation of Colimits
    Omitted.

    Item 11: Preservation of Limits
    This follows from Item 2 and Unresolved reference, Unresolved reference of Unresolved reference.

    Item 12: Symmetric Lax Monoidality With Respect to Unions
    This follows from Item 10.

    Item 13: Symmetric Strict Monoidality With Respect to Intersections
    This follows from Item 11.

    Item 14: Interaction With Coproducts
    Omitted.

    Item 15: Interaction With Products
    Omitted.

    Item 16: Relation to Direct Images
    We claim that $f_{*}\webleft (U\webright )=Y\setminus f_{!}\webleft (X\setminus U\webright )$.

    • The First Implication. We claim that

      \[ f_{*}\webleft (U\webright )\subset Y\setminus f_{!}\webleft (X\setminus U\webright ). \]

      Let $y\in f_{*}\webleft (U\webright )$. We need to show that $y\not\in f_{!}\webleft (X\setminus U\webright )$, i.e. that there is no $x\in X\setminus U$ such that $f\webleft (x\webright )=y$.

      This is indeed the case, as otherwise we would have $x\in f^{-1}\webleft (y\webright )$ and $x\not\in U$, contradicting $f^{-1}\webleft (y\webright )\subset U$ (which holds since $y\in f_{*}\webleft (U\webright )$).

      Thus $y\in Y\setminus f_{!}\webleft (X\setminus U\webright )$.

    • The Second Implication. We claim that

      \[ Y\setminus f_{!}\webleft (X\setminus U\webright )\subset f_{*}\webleft (U\webright ). \]

      Let $y\in Y\setminus f_{!}\webleft (X\setminus U\webright )$. We need to show that $y\in f_{*}\webleft (U\webright )$, i.e. that $f^{-1}\webleft (y\webright )\subset U$.

      Since $y\not\in f_{!}\webleft (X\setminus U\webright )$, there exists no $x\in X\setminus U$ such that $y=f\webleft (x\webright )$, and hence $f^{-1}\webleft (y\webright )\subset U$.

      Thus $y\in f_{*}\webleft (U\webright )$.

    This finishes the proof of Item 16.

    Item 17: Interaction With Injections
    Omitted.

    Item 18: Interaction With Surjections
    Omitted.

    Let $f\colon X\to B$ be a function.

    1. 1.

      Functionality I. The assignment $f\mapsto f_{*}$ defines a function

      \[ \webleft (-\webright )_{!|X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Sets}\webleft (\mathcal{P}\webleft (X\webright ),\mathcal{P}\webleft (Y\webright )\webright ). \]
    2. 2.

      Functionality II. The assignment $f\mapsto f_{*}$ defines a function

      \[ \webleft (-\webright )_{!|X,Y}\colon \mathsf{Sets}\webleft (X,Y\webright ) \to \mathsf{Pos}\webleft (\webleft (\mathcal{P}\webleft (X\webright ),\subset \webright ),\webleft (\mathcal{P}\webleft (Y\webright ),\subset \webright )\webright ). \]
    3. 3.

      Interaction With Identities. For each $X\in \operatorname {\mathrm{Obj}}\webleft (\mathsf{Sets}\webright )$, we have

      \[ \webleft (\operatorname {\mathrm{id}}_{X}\webright )_{*}=\operatorname {\mathrm{id}}_{\mathcal{P}\webleft (X\webright )}. \]
    4. 4.

      Interaction With Composition. For each pair of composable functions $f\colon X\to Y$ and $g\colon Y\to Z$, we have


Noticed something off, or have any comments? Feel free to reach out!


You can also use the contact form below: