Definitions/Def_AlgebraicGeometry_ModulesProjectionMorphism.lean

Fix a morphism of schemes i\colon Z\to X. Both Z.Modules and X.Modules, the categories of sheaves of modules over the structure sheaves, carry the symmetric monoidal structure obtained by localising the tensor product of presheaves of modules along sheafification, and the inverse-image functor Modules.pullback i is monoidal for these structures; the tensor unit \mathbb 1_{Z.\mathrm{Modules}} is the structure sheaf \mathcal O_Z viewed as a module over itself. Two morphisms are defined, for each F in X.Modules.

First, projectionMorphismMate i F is a morphism i^{*}\bigl(i_{*}\mathcal O_Z\otimes F\bigr)\to i^{*}F, namely the composite of: the inverse of the monoidal structure isomorphism \mu of Modules.pullback i at the pair (i_{*}\mathcal O_Z, F), which identifies i^{*}(i_{*}\mathcal O_Z\otimes F) with i^{*}i_{*}\mathcal O_Z\otimes i^{*}F; the right whiskering by i^{*}F of the counit of the adjunction pullbackPushforwardAdjunction i evaluated at the unit object, i^{*}i_{*}\mathcal O_Z\to\mathcal O_Z; and the left unitor \mathbb 1\otimes i^{*}F\xrightarrow{\ \sim\ }i^{*}F.

Second, projectionMorphism i F is the morphism i_{*}\mathcal O_Z\otimes_{\mathcal O_X}F\;\longrightarrow\;i_{*}\,i^{*}F obtained by transposing the mate across the adjunction i^{*}\dashv i_{*}, i.e. the image of projectionMorphismMate i F under the hom-equivalence of pullbackPushforwardAdjunction i. No assertion is attached: only the morphism is constructed, so that the several statements about it (its transpose identity, its naturality in F, and its invertibility under hypotheses on i and F) all speak about one and the same map. The remaining two declarations are unfolding lemmas recording these two composites as the definitions of projectionMorphism and projectionMorphismMate.