# Name for this map of power sets associated with a function?

Given a function $$f: X \to Y$$, there are two associated maps of power sets: the direct image $$f^{\to}: \mathcal{P}(X) \to \mathcal{P}(Y)$$ and the inverse image $$f^{\leftarrow}: \mathcal{P}(Y) \to \mathcal{P}(X)$$.

Consider the map

$$f^?: \mathcal{P}(X) \to \mathcal{P}(Y)$$

defined by

$$f^?(A) = \{y \in Y: f^\leftarrow(\{y\}) \subset A\}$$

In words, $$f^?(A)$$ is the set of all $$y \in Y$$ so that every $$x$$ which maps to $$y$$ is in $$A$$.

Does this map have a standard name and notation?

Note: I became interested in this while reading this nCategory Cafe post. Knowing the context is not needed to answer the question, but $$f^?$$ is associated with universal quantification in the sense of the post.

• I wouldn't really know if it has a name or notation. But $f^?(A) = Y \setminus f^{\rightarrow}(X \setminus A)$ gives the set of things not in the image of $f$ on $X \setminus A$. You could write something hilarious like $f^? = \neg \circ f^{\rightarrow} \circ \neg$ (I've no idea if the complement map has a standard notation) to emphasize it's not really anything 'new'. Feb 19, 2021 at 14:50
• @Sharkos Your observation is exactly (in the sense of the nCategory cafe post) the connection that $\forall x P(x) = \neg \exists x \neg P(x)$. So it is "nothing new" if your logic is classical, but is new if your logic is intuitionistic. Feb 19, 2021 at 14:59
• I like to call this the "coimage". I'm not sure how standard this is, but I've seen it used in a few other places. Unfortunately "coimage" has another standard meaning in category theory... Feb 20, 2021 at 4:45
• It does make some sense to call it "coimage", despite the terminology conflict. Not that long ago this came up in a group discussion, but no one IMO supplied a great alternative terminology. I may try some other people for suggestions. Something with the same visual impact as "image", optimally. Feb 20, 2021 at 14:41

(Adapted from an email I sent the OP, who was also asking about connections with "the six operations" of Grothendieck.)

I guess it might depend which community you're talking to. I believe the notation $$\exists_f$$ (for direct image along $$f$$) and $$\forall_f$$ notation (for the thing OP is asking about) is somewhat standard for those working in topos theory and categorical logic. For example, you see both notations in Mac Lane-Moerdijk, Sheaves in Geometry and Logic, Proposition IV.9.3 and just before. In the same place you will see the parallel notation for functors between slice toposes, $$\Sigma_f: E/X \to E/Y$$ and $$\Pi_f: E/X \to E/Y$$.

(These notations make sense when you consider that

$$f^\to(A) = \exists_f(A) = \{y \in Y: \exists_{x \in X}\; y = f(x) \wedge x \in A\}$$

$$f^?(A) = \forall_f(A) = \{y \in Y: \forall_{x \in X}\; y = f(x) \Rightarrow x \in A\}$$

These notations may have begun with Lawvere, who uses it e.g. in his 1970 paper Quantifiers and Sheaves.)

For some reason, $$\forall_f$$ seems to be the "weak sister", much less well-known than her brother the direct image along $$f$$. I am not aware of any standard name or notation for it in the traditional logical literature. And yet, it plays a role here and there. For example, if X is a compact space with a countable base $$B$$ and $$f: X \to Y$$ is a continuous surjection to a Hausdorff space, then $$Y$$ also has a countable base; the most natural choice for that base is $$\{\forall_f(U): U \in B\}$$. Another example: it's more direct to prove that if $$X$$ is compact and $$Y$$ is a space, and $$p: X \times Y \to Y$$ is projection, then the operator $$\forall_p$$ takes open sets to open sets, than it is to prove that the direct image $$\exists_p$$ takes closed sets to closed sets (which is the De Morgan dual statement).

In representation theory, the corresponding operations are induction and coinduction (of a $$G$$-representation along a group homomorphism $$f: G \to H$$) that are left and right adjoint to the restriction functor along $$f$$. These can also be described by (enriched) Kan extensions. So $$Res_f$$ would be like pullback $$f^\ast = f^\leftarrow$$, $$Ind_f$$ would be like $$\exists_f$$, and $$Coind_f$$ would be like $$\forall_f$$.

Yes, morally this is related to "the six operations" although I don't know much about that either. In particular, what I know as "Frobenius reciprocity", whose logical form is $$\exists_f(S) \wedge T = \exists_f(S \wedge f^\ast(T)$$), is formally like the projection formula in algebraic geometry (and there's a similar-looking one for Chow rings). The name "Frobenius reciprocity" here was introduced by Lawvere (naturally), borrowing from terminology of representation theorists, who often refer just to the adjunction $$Ind_f \dashv Res_f$$ as "Frobenius reciprocity", but who sometimes include as part of this the analogous isomorphism

$$Ind_f(V) \otimes W \cong Ind_f(V \otimes Res_f(W)).$$

In the language of hyperdoctrines, these reciprocity isomorphisms arise from the fact that pulling back or restriction along $$f$$ preserves the internal hom (see again Mac Lane & Moerdijk, IV.9, although they don't mention the word "hyperdoctrine").