Definitions/Def_AlgebraicGeometry_ModulesRigidifyV2.lean

Fix schemes T and P. For a morphism \sigma : T \to P, a morphism q : P \to T and a sheaf of modules L on P (an object of P.Modules), the rigidification is defined by \operatorname{rigidify} \sigma\, q\, L \;=\; L \otimes q^{*}\bigl((\sigma^{*}L)^{\vee}\bigr), where \sigma^{*} and q^{*} are the pullback functors Scheme.Modules.pullback on sheaves of modules, \otimes is the monoidal product on P.Modules, and the dual is Scheme.Modules.dual M = (ihom M).obj (𝟙_ X.Modules), the internal hom into the unit object for the monoidal closed structure on modules over a scheme. The defining equation is also recorded as a rewriting lemma. Functoriality on isomorphisms is provided: dualMapIso sends an isomorphism e : L \cong L' of modules on X to an isomorphism L^{\vee} \cong L'^{\vee}, obtained by applying the internal-hom functor to e^{-1} in the contravariant variable and evaluating at the unit; and rigidifyMapIso combines e with the image of \sigma^{*}e under dualisation and q^{*} to give \operatorname{rigidify} \sigma\, q\, L \cong \operatorname{rigidify} \sigma\, q\, L'. No naturality or coherence statements beyond these isomorphisms are asserted.

The ambient structure on which these constructions rest is the symmetric monoidal closed structure on X.Modules and on X.PresheafOfModules. For presheaves of modules over a presheaf of commutative rings R, the internal hom at X is the R(X)-module of families \varphi_f : F(Y) \to N(Y) of R(Y)-linear maps indexed by f : X \to Y, compatible with restriction; the resulting adjunction F \otimes - \dashv \operatorname{ihom}(F,-) makes presheaves of modules monoidal closed. Sheafification is a monoidal localisation at the class of maps that become weak equivalences of presheaves of abelian groups, which transports the symmetric monoidal structure, its closedness, and the monoidality of the sheafification functor to sheaves of modules, hence to X.Modules.