Definitions/Def_AlgebraicGeometry_ModulesTensorPow.lean

For a scheme X, the category X.Modules of sheaves of \mathcal{O}_X-modules carries a symmetric monoidal structure with unit SheafOfModules.unit X.ringCatSheaf, i.e. \mathcal{O}_X itself, obtained by transporting the tensor product of presheaves of modules along the sheafification functor Scheme.Modules.sheafify X, which is a localisation with respect to the class of morphisms of presheaves of modules that become local isomorphisms on underlying abelian-group-valued presheaves; that class is shown to be compatible with the monoidal structure, and the resulting monoidal category is symmetric and monoidal closed, the internal hom coming from the internal hom on presheaves of modules, whose sections over U are the families of \mathcal{O}-linear maps \mathcal{F}(V) \to \mathcal{N}(V) indexed by the objects over U and natural in V. Relative to this structure, the tensor power \mathcal{L}^{\otimes n} of an \mathcal{O}_X-module \mathcal{L} is defined by recursion on n: tensorPow L 0 is the monoidal unit \mathcal{O}_X, and tensorPow L (n+1) is tensorPow L n ⊗ L. Thus the recursion multiplies on the right, so \mathcal{L}^{\otimes n} is the left-bracketed product (\cdots((\mathcal{O}_X \otimes \mathcal{L}) \otimes \mathcal{L}) \cdots) \otimes \mathcal{L}. The two accompanying equations record the defining clauses as equalities of objects, not merely isomorphisms: tensorPow_zero identifies \mathcal{L}^{\otimes 0} with the unit, and tensorPow_succ identifies \mathcal{L}^{\otimes(n+1)} with \mathcal{L}^{\otimes n} \otimes \mathcal{L}. Finally tensorPowOneIso is an isomorphism \mathcal{L}^{\otimes 1} \cong \mathcal{L}, namely the left unitor of the monoidal structure applied to \mathcal{L}, since \mathcal{L}^{\otimes 1} is by definition \mathcal{O}_X \otimes \mathcal{L}. Also provided, for comparison with the presheaf-level tensor product, is the isomorphism identifying the sheafification of \mathcal{L}.\mathrm{val} \otimes \mathcal{M}.\mathrm{val} with \mathcal{L} \otimes \mathcal{M}, and the dual \mathcal{L}^{\vee} as the internal hom from \mathcal{L} into the unit.