The Stacks project

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?

I believe it means that $(G,F) \mapsto Hom(G,f_{\*}F)$ and $(G,F)\mapsto Hom(f^{-1}G,F)$ are isomorphic as functors $Sh^{op} \times Sh \to Sets$.

Spelled out, this means that the bijections $\varphi_{G,F} : Hom(G,f_{\*}F) \to Hom(f^{-1}G,F)$ satisfy the following property: for every $\alpha : F \to F_1$, $\beta : G_1 \to G$, and $u\in Hom(f^{-1}G,F)$, it is the case that $\varphi_{G_1,F_1}(\alpha\circ u\circ f^{-1}\beta) = f_{\*}\alpha\circ\varphi_{G,F}(u)\circ \beta$ as maps $G_1\to f_{\*}F_1$.

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 $a : \mathcal{G} \to f_\star\mathcal{F}$ is by definition a rule which to each open $V$ of $Y$ determines a map $a_V : \mathcal{G}(V) \to f_\star\mathcal{F}(V)$ and we have $f_\star\mathcal{F}(V) = \mathcal{F}(f^{-1}(V))$. Thus at least the "data" corresponds exactly to what you need for an $f$-map from $\mathcal{G}$ to $\mathcal{F}$ and all you have to show is that the fact that $a$ 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 $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. So you would first need to tell your student how to set up a bijective correspondence between $b$s and $b_p$s. OK. Next, to give $b_p$ you need to specify for each open $U$ of $X$ a map $$b_{p, U} : colim_{f(U) \subset V} \mathcal{G}(V) \longrightarrow \mathcal{F}(U)$$ compatible with restriction mappings (whatever that means). Next, you can 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. Thus we see that $b_p$ corresponds to what we might call an *extended $f$-map $\tilde \xi$ from $\mathcal{G}$ to $\mathcal{F}$" which is the data of a collection of maps $\tilde \xi_{U, V}$ as above.

Then to finish the proof of the lemma you have to show that by "forgetting structure" the rule that to an extended $f$-map associates an $f$-map 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)$.

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.

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 $(G,F) \mapsto Hom(G,f_{*}F)$ and $(G,F)\mapsto Hom(f^{-1}G,F)$ are isomorphic as functors $Sh^{op} \times Sh \to Sets$.

Spelled out, this means that the bijections $\varphi_{G,F} : Hom(G,f_{*}F) \to Hom(f^{-1}G,F)$ satisfy the following property: for every $\alpha : F \to F_1$, $\beta : G_1 \to G$, and $u\in Hom(f^{-1}G,F)$, it is the case that $\varphi_{G_1,F_1}(\alpha\circ u\circ f^{-1}\beta) = f_{*}\alpha\circ\varphi_{G,F}(u)\circ \beta$ as maps $G_1\to f_{*}F_1$.

@#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 $f_*$ and $f^{-1}$ 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 $f = (f^{-1}, f_*)$ is the adjunction between $f^{-1}$ and $f_*$ unique? Equivalently, can it ever happen that the functor $f_*$ 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.

@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_*.

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.

Made some changes, see here.