The Stacks project

Lemma 6.21.8. Let $f : X \to Y$ be a continuous map. There are bijections between the following four sets

  1. the set of maps $\mathcal{G} \to f_*\mathcal{F}$,

  2. the set of maps $f^{-1}\mathcal{G} \to \mathcal{F}$,

  3. the set of $f$-maps $\xi : \mathcal{G} \to \mathcal{F}$, and

  4. the set of all collections of maps $\xi _{U, V} : \mathcal{G}(V) \to \mathcal{F}(U)$ for all $U \subset X$ and $V \subset Y$ open such that $f(U) \subset V$ compatible with all restriction maps,

functorially in $\mathcal{F} \in \mathop{\mathit{Sh}}\nolimits (X)$ and $\mathcal{G} \in \mathop{\mathit{Sh}}\nolimits (Y)$.

Proof. A map of sheaves $a : \mathcal{G} \to f_*\mathcal{F}$ is by definition a rule which to each open $V$ of $Y$ assigns a map $a_ V : \mathcal{G}(V) \to f_*\mathcal{F}(V)$ and we have $f_*\mathcal{F}(V) = \mathcal{F}(f^{-1}(V))$. Thus at least the "data" corresponds exactly to what you need for an $f$-map $\xi $ from $\mathcal{G}$ to $\mathcal{F}$. To show that the sets (1) and (3) are in bijection we observe that $a$ is a map of sheaves if and only if corresponding family of maps $a_ V$ satisfy the condition in Definition 6.21.7.

Recall that $f^{-1}\mathcal{G}$ is the sheafification of $f_ p\mathcal{G}$. By the universal property of sheafification a map of sheaves $b : f^{-1}\mathcal{G} \to \mathcal{F}$ is the same thing as a map of presheaves $b_ p : f_ p\mathcal{G} \to \mathcal{F}$ where $f_ p$ is the functor defined earlier in the section. To give such a map $b_ p$ you need to specify for each open $U$ of $X$ a map

\[ b_{p, U} : \mathop{\mathrm{colim}}\nolimits _{f(U) \subset V} \mathcal{G}(V) \longrightarrow \mathcal{F}(U) \]

compatible with restriction mappings. We may and do view $b_{p, U}$ as a collection of maps $b_{p, U, V} : \mathcal{G}(V) \to \mathcal{F}(U)$ for all $V$ open in $Y$ with $f(U) \subset V$. These maps have to be compatible with all possible restriction mappings you can think of. In other words, we see that $b_ p$ corresponds to a collection of maps as in (4). Of course, conversely such a collection defines a map $b_ p$ and in turn a map $b : f^{-1}\mathcal{G} \to \mathcal{F}$.

To finish the proof of the lemma you have to show that by "forgetting structure" the rule that to a collection $\xi _{U, V}$ as in (4) associates the $f$-map $\xi $ with $\xi _ V = \xi _{f^{-1}(V), V}$ is bijective. To do this, if $\xi $ is a usual $f$-map then we just define $\tilde\xi _{U, V}$ to be the composition of $\xi _ V : \mathcal{G}(V) \to \mathcal{F}(f^{-1}(V))$ by the restruction map $\mathcal{F}(f^{-1}(V)) \to \mathcal{F}(U)$ which makes sense exactly because $f(U) \subset V$, i.e., $U \subset f^{-1}(V)$. This finishes the proof. $\square$


Comments (14)

Comment #5955 by on

I cannot finish the proof of this "easy verification" in Lean because I cannot understand the definition of the word "canonical map" in Wikipedia, and there appears to be no definition of this word in the Stacks Project. Can you please clarify what is being asserted here?

Comment #5956 by Nicolás on

I believe it means that and are isomorphic as functors .

Spelled out, this means that the bijections satisfy the following property: for every , , and , it is the case that as maps .

Comment #5957 by on

Yes, this is a bit terse indeed. Here are some more details. I might add this later when I next go through all the comments.

A map of sheaves is by definition a rule which to each open of determines a map and we have . Thus at least the "data" corresponds exactly to what you need for an -map from to and all you have to show is that the fact that is a map of sheaves is the same thing as the corresponding family of maps satisfying the condition in Definition 6.21.7.

Next, a map of sheaves is the same thing as a map of presheaves where is the functor defined earlier in the section. So you would first need to tell your student how to set up a bijective correspondence between s and s. OK. Next, to give you need to specify for each open of a map compatible with restriction mappings (whatever that means). Next, you can view as a collection of maps for all open in with . These maps have to be compatible with all possible restriction mappings you can think of. Thus we see that corresponds to what we might call an *extended -map from to " which is the data of a collection of maps as above.

Then to finish the proof of the lemma you have to show that by "forgetting structure" the rule that to an extended -map associates an -map is bijective. To do this, if is a usual -map then we just define to be the composition of by the restruction map which makes sense exactly because , i.e., .

Comment #5986 by on

Just to be clear -- I can construct the bijections no problem -- I am just unclear about the meaning of the assertion that they're "canonical". My model of what is going on is just that the constructions have some nice properties (e.g. they commute with various things like binary direct sums and a gazillion other things) but I was wondering whether the use of the word "canonical" had any actual formal meaning beyond the informal "you can construct these bijections by following your nose".

I wish I could read Nicolas' comment! I get a bunch of "undefined control sequence *" messages.

Comment #5988 by on

He seems to have used a macro which causes some issues. I think he might have gotten thrown off by rendering issues in the preview. Let me reconstruct the message from the HTML source. In any case it looks like I have some bug fixing to do.

I believe it means that and are isomorphic as functors .

Spelled out, this means that the bijections satisfy the following property: for every , , and , it is the case that as maps .

Comment #5990 by on

@#5986 Dear Kevin, ok often "canonical" isn't a good word to use as is true in this case. In this case it means "most human beings reading this would come up with the same bijections as I did when I wrote a proof of this lemma on a napkin". In particular these other humans (and maybe some aliens too) would find that these bijections are bifunctorial and exhibit and as a pair of adjoint functors as stated earlier in the text.

Maybe a fun related mathematical question wouid be: given a morphism of topoi is the adjunction between and unique? Equivalently, can it ever happen that the functor has a non-identity automorphism?

Anyway, this entire section could be written more clearly so it would be easier to read for Xena as well as human beings. Comments complaining about terminology are very welcome, especially if accompanied by suggestions for improvements.

Comment #6018 by Harry Gindi on

@Kevin: The bijection between (i) and (ii) is in fact natural, as Pieter correctly notes (as one should expect from an adjunction). The bijection between (i) and (iii) is precisely a one-step unwinding of the definition of f_*.

Comment #6025 by on

Harry I'm well aware of these things. My comments, which are in jest really (and Johan is well aware of this) is that whilst we have perfectly good words from category theory which can be applied here, mathematicians often avoid them and instead choose the not-properly-defined word "canonical", which is problematic for me as a formaliser because it is not clear precisely what is being claimed. Equally clear however is that whatever "canonical" properties a mathematician might require from this bijection, such properties will be easily proved in practice. The joke is just that by saying "canonical" a mathematician can avoid having to precisely specify what they actually mean, so i was challening Johan to list everything which he means so that I can formalise this tag "properly" in Lean. The joke stops being funny when people start saying that a Langlands correspondence is "canonical", and as a formaliser what I am learning is that some mathematicians simply don't know the difference between a theorem ("there exists a canonical map...") and a definition ("I am defining a map. Next I will prove the following theorems about it. Whether or not this makes my map canonical is up to you, because the word has no formal meaning.") Our instinct is to write everything in terms of theorems, but actually the "lemma" above should be a definition of three bijections (rather than a claim that such bijections happen to exist, which is never what is used in practice) followed by theorems about those bijections (such as the ones cited above). I'm not sure that here is the best place to be having this conversation but would quite happily continue it offline -- you know where to find me.

Comment #6785 by Elías Guisado on

I think the proof of this proposition also works when and are presheaves? As fair as I've understood, the proof does not use the sheaf condition at any moment. The proposition would be more general stating it that way.

Comment #6787 by on

@#6785. This is true, except that the pullback in the category of presheaves is different from pullback in the category of sheaves. Also, the notion of an -map is only defined for sheaves at the moment. But yes, there is a statement you can formulate and prove for presheaves which then implies the statement for sheaves using that sheafification is an adjoint to the inclusion of presheaves into sheaves.

I think there is a typo in the first paragraph of the proof and it should say "To show that (1) and (3 are in bijection" and not "(1) and (2)".

Comment #6788 by Elías Guisado on

@#6787 I have just realized that there is a step in the proof which uses the hypothesis of being a sheaf. Namely, the part of "a map of sheaves is the same thing as a map of presheaves ". But yes, as I think you are suggesting, substituting on point (2) in the statement "f^{-1}\mathcal{G}\to\mathcal{F}f_p\mathcal{G}\to\mathcal{F}$ would generalize the lemma to presheaves.

There are also:

  • 2 comment(s) on Section 6.21: Continuous maps and sheaves

Post a comment

Your email address will not be published. Required fields are marked.

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).

Unfortunately JavaScript is disabled in your browser, so the comment preview function will not work.

All contributions are licensed under the GNU Free Documentation License.




In order to prevent bots from posting comments, we would like you to prove that you are human. You can do this by filling in the name of the current tag in the following input field. As a reminder, this is tag 008K. Beware of the difference between the letter 'O' and the digit '0'.