4.6.1 Direct Images

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

    Definition 4.6.1.1.1 ▶ Direct Images

    The direct image function associated to $f$ is the function1

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

    defined by2

    \begin{align*} f_{!}\webleft (U\webright ) & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}f\webleft (U\webright )\\ & \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\left\{ y\in Y\ \middle |\ \begin{aligned} & \text{there exists some $x\in U$}\\ & \text{such that $y=f\webleft (x\webright )$} \end{aligned} \right\} \\ & = \left\{ f\webleft (x\webright )\in Y\ \middle |\ x\in U\right\} \end{align*}

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

    1. 1Further Notation: Also written simply $f\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright )$.
    2. 2Further Terminology: The set $f\webleft (U\webright )$ is called the direct image of $U$ by $f$.

    Notation 4.6.1.1.2 ▶ Further Notation for Direct Images

    Sometimes one finds the notation

    \[ \exists _{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 \exists _{f}\webleft (U\webright )$.

    • •

      There exists some $x\in U$ such that $f\webleft (x\webright )=y$.

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

    ゴ
    ゴ
    ゴ
    Warning 4.6.1.1.3 ▶ Notation for Direct Images Is Confusing

    Notation for direct images between powersets is tricky:

    1. 1.

      Direct images for powersets and presheaves are both adjoint to their corresponding inverse image functors. However, the direct image functor for powersets is a left adjoint, while the direct image functor for presheaves is a right adjoint:

      1. (a)

        Powersets. Given a function $f\colon X\to Y$, we have an inverse image functor

        \[ f^{-1}\colon \mathcal{P}\webleft (Y\webright )\to \mathcal{P}\webleft (X\webright ). \]

        The left adjoint of this functor is the usual direct image, defined above in Definition 4.6.1.1.1.

      2. (b)

        Presheaves. Given a morphism of topological spaces $f\colon X\to Y$, we have an inverse image functor

        \[ f^{-1}\colon \mathsf{PSh}\webleft (Y\webright )\to \mathsf{PSh}\webleft (X\webright ). \]

        The right adjoint of this functor is the direct image functor of presheaves, defined in Unresolved reference.

    2. 2.

      The presheaf direct image functor is denoted $f_{*}$, but the direct image functor for powersets is denoted $f_{!}$ (as it’s a left adjoint).

    3. 3.

      Adding to the confusion, it’s somewhat common for $f_{!}\colon \mathcal{P}\webleft (X\webright )\to \mathcal{P}\webleft (Y\webright )$ to be denoted $f_{*}$.

    We chose to write $f_{!}$ for the direct image to keep the notation aligned with the following similar adjoint situations:

    Situation

    Adjoint String

    Functoriality

    of Powersets

    $\webleft (f_{!}\dashv f^{-1}\dashv f_{*}\webright )\colon \mathcal{P}\webleft (X\webright )\overset {\rightleftarrows }{\to }\mathcal{P}\webleft (Y\webright )$

    Functoriality of

    Presheaf Categories

    $\webleft (f_{!}\dashv f^{-1}\dashv f_{*}\webright )\colon \mathsf{PSh}\webleft (X\webright )\overset {\rightleftarrows }{\to }\mathsf{PSh}\webleft (Y\webright )$

    Base Change

    $\webleft (f_{!}\dashv f^{*}\dashv f_{*}\webright )\colon \mathcal{C}_{/X}\overset {\rightleftarrows }{\to }\mathcal{C}_{/Y}$

    Kan Extensions

    $\webleft (F_{!}\dashv F^{*}\dashv F_{*}\webright )\colon \mathsf{Fun}\webleft (\mathcal{C},\mathcal{E}\webright )\overset {\rightleftarrows }{\to }\mathsf{Fun}\webleft (\mathcal{D},\mathcal{E}\webright )$

    ゴ
    ゴ
    ゴ

    Remark 4.6.1.1.4 ▶ Unwinding Definition 4.6.1.1.1

    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 direct 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{Lan}}_{f}\webleft (\chi _{U}\webright )\\ & = \operatorname*{\operatorname {\mathrm{colim}}}\webleft (\webleft (f\mathbin {\overset {\to }{\times }}\underline{\webleft (-_{1}\webright )}\webright )\overset {\operatorname {\mathrm{\mathrm{pr}}}}{\twoheadrightarrow }A\overset {\chi _{U}}{\to }\{ \mathsf{t},\mathsf{f}\} \webright )\\ & = \operatorname*{\operatorname {\mathrm{colim}}}_{\substack {x\in X\\ \begin{bgroup} f\webleft (x\webright )=-_{1} \end{bgroup}}}\webleft (\chi _{U}\webleft (x\webright )\webright )\\ & = \bigvee _{\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 )& =\bigvee _{\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 there exists some $x\in X$ such}\\ & \text{that $f\webleft (x\webright )=y$ and $x\in U,$}\\ \mathsf{false}& \text{otherwise} \end{cases}\\ & =\begin{cases} \mathsf{true}& \text{if there exists some $x\in U$}\\ & \text{such that $f\webleft (x\webright )=y$,}\\ \mathsf{false}& \text{otherwise} \end{cases}\end{align*}

    for each $y\in Y$.

    Proposition 4.6.1.1.5 ▶ Properties of Direct Images I

    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:

          1. (I)

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

          2. (II)

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

        2. (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. 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. 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. 5.

      Interaction With Binary Unions. The diagram

      commutes, i.e. we have

      \[ f_{!}\webleft (U\cup V\webright )=f_{!}\webleft (U\webright )\cup f_{!}\webleft (V\webright ) \]

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

    6. 6.

      Interaction With Binary Intersections. We have a natural transformation

      with components

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

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

    7. 7.

      Interaction With Differences. We have a natural transformation

      with components

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

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

    8. 8.

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

    9. 9.

      Interaction With Symmetric Differences. We have a natural transformation

      with components

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

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

    10. 10.

      Interaction With Internal Homs of Powersets. The diagram

      commutes, i.e. we have an equality of sets

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

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

    11. 11.

      Preservation of Colimits. We have an equality of sets

      \[ f_{!}\left(\bigcup _{i\in I}U_{i}\right)=\bigcup _{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_{!}\webleft (U\webright )\cup f_{!}\webleft (V\webright ) = f_{!}\webleft (U\cup V\webright ),\\ f_{!}\webleft (\text{Ø}\webright ) = \text{Ø}, \end{gathered} \]

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

    12. 12.

      Oplax Preservation of Limits. We have an inclusion of sets

      \[ f_{!}\left(\bigcap _{i\in I}U_{i}\right)\subset \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 inclusions

      \[ \begin{gathered} f_{!}\webleft (U\cap V\webright ) \subset f_{!}\webleft (U\webright )\cap f_{!}\webleft (V\webright ),\\ f_{!}\webleft (X\webright ) \subset Y, \end{gathered} \]

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

    13. 13.

      Symmetric Strict Monoidality With Respect to Unions. 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 ),\cup ,\text{Ø}\webright ) \to \webleft (\mathcal{P}\webleft (Y\webright ),\cup ,\text{Ø}\webright ), \]

      being equipped with equalities

      \[ \begin{gathered} f^{\otimes }_{!|U,V} \colon f_{!}\webleft (U\webright )\cup f_{!}\webleft (V\webright ) \mathbin {\overset {=}{\rightarrow }}f_{!}\webleft (U\cup V\webright ),\\ f^{\otimes }_{!|\mathbb {1}} \colon \text{Ø}\mathbin {\overset {=}{\rightarrow }}\text{Ø}, \end{gathered} \]

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

    14. 14.

      Symmetric Oplax Monoidality With Respect to Intersections. The direct image function of Item 1 has a symmetric oplax 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 inclusions

      \[ \begin{gathered} f^{\otimes }_{!|U,V} \colon f_{!}\webleft (U\cap V\webright ) \hookrightarrow f_{!}\webleft (U\webright )\cap f_{!}\webleft (V\webright ),\\ f^{\otimes }_{!|\mathbb {1}} \colon f_{!}\webleft (X\webright ) \hookrightarrow Y, \end{gathered} \]

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

    15. 15.

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

    16. 16.

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

    17. 17.

      Relation to Codirect Images. We 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*}

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

    Proof of Proposition 4.6.1.1.5.

    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
    See [Proof Wiki Contributors, Image of Union Under Mapping — Proof Wiki].

    Item 6: Interaction With Binary Intersections
    See [Proof Wiki Contributors, Image of Intersection Under Mapping — Proof Wiki].

    Item 7: Interaction With Differences
    See [Proof Wiki Contributors, Image of Set Difference Under Mapping — Proof Wiki].

    Item 8: Interaction With Complements
    Applying Item 17 to $X\setminus U$, we have

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

    This finishes the proof.

    Item 9: Interaction With Symmetric Differences
    We have

    \begin{align*} f_{!}\webleft (U\webright )\mathbin {\triangle }f_{!}\webleft (V\webright ) & = \webleft (f_{!}\webleft (U\webright )\cup f_{!}\webleft (V\webright )\webright )\setminus \webleft (f_{!}\webleft (U\webright )\cap f_{!}\webleft (V\webright )\webright )\\ & \subset \webleft (f_{!}\webleft (U\webright )\cup f_{!}\webleft (V\webright )\webright )\setminus \webleft (f_{!}\webleft (U\cap V\webright )\webright )\\ & = \webleft (f_{!}\webleft (U\cup V\webright )\webright )\setminus \webleft (f_{!}\webleft (U\cap V\webright )\webright )\\ & \subset f_{!}\webleft (\webleft (U\cup V\webright )\setminus \webleft (U\cap V\webright )\webright )\\ & = f_{!}\webleft (U\mathbin {\triangle }V\webright ), \end{align*}

    where we have used:

    1. 1.

      Item 2 of Proposition 4.3.12.1.2 for the first equality.

    2. 2.

      Item 6 of this proposition together with Item 1 of Proposition 4.3.10.1.2 for the first inclusion.

    3. 3.

      Item 5 for the second equality.

    4. 4.

      Item 7 for the second inclusion.

    5. 5.

      Item 2 of Proposition 4.3.12.1.2 for the tchird equality.

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

    Item 10: Interaction With Internal Homs of Powersets
    We have

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

    where we have used:

  • 1.

    Item 5 for the second equality.

  • 2.

    Item 17 for the third equality.

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

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

    Item 12: Oplax Preservation of Limits
    The inclusion $f_{!}\webleft (X\webright )\subset Y$ is automatic. See [Proof Wiki Contributors, Image of Intersection Under Mapping — Proof Wiki] for the other inclusions.

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

    Item 14: Symmetric Oplax Monoidality With Respect to Intersections
    The inclusions in the statement follow from Item 12. Since $\mathcal{P}\webleft (Y\webright )$ is posetal, the commutativity of the diagrams in the definition of a symmetric oplax monoidal functor is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2).

    Item 15: Interaction With Coproducts
    Omitted.

    Item 16: Interaction With Products
    Omitted.

    Item 17: Relation to Codirect Images
    Applying Item 16 of Proposition 4.6.3.1.7 to $X\setminus U$, we have

    \begin{align*} f_{*}\webleft (X\setminus U\webright ) & = B\setminus f_{!}\webleft (X\setminus \webleft (X\setminus U\webright )\webright )\\ & = B\setminus f_{!}\webleft (U\webright ). \end{align*}

    Taking complements, we then obtain

    \begin{align*} f_{!}\webleft (U\webright ) & = B\setminus \webleft (B\setminus f_{!}\webleft (U\webright )\webright ),\\ & = B\setminus f_{*}\webleft (X\setminus U\webright ), \end{align*}

    which finishes the proof.

    1. 1Reference: [Proof Wiki Contributors, Image of Union Under Mapping — Proof Wiki].

    Proposition 4.6.1.1.6 ▶ Properties of Direct Images II

    Let $f\colon X\to Y$ 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

    Proof of Proposition 4.6.1.1.6.
Up

View Item 1 as PDF
1 tag refers to this tag
Statistics Cite

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

You can also use the contact form below: