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.

  • 1
    $\begingroup$ 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'. $\endgroup$ Feb 19, 2021 at 14:50
  • $\begingroup$ @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. $\endgroup$ Feb 19, 2021 at 14:59
  • $\begingroup$ 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... $\endgroup$ Feb 20, 2021 at 4:45
  • $\begingroup$ 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. $\endgroup$
    – user43208
    Feb 20, 2021 at 14:41

1 Answer 1


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

Sorry that I don't have a better answer to your question!

  • $\begingroup$ Thanks so much! I am accepting this answer because it seems that there really is no standard terminology. If I ever write about it I might call it the "universal image". $\endgroup$ Feb 20, 2021 at 15:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .