The Stacks project

Lemma 6.21.8. Let $f : X \to Y$ be a continuous map. Let $\mathcal{F}$ be a sheaf of sets on $X$ and let $\mathcal{G}$ be a sheaf of sets on $Y$. There are canonical bijections between the following three 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}$.

Proof. We leave the easy verification to the reader. $\square$

Comments (8)

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 ?42?" 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.

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'.