Definitions/Def_AlgebraicGeometry_ModulesSectionsTensorV2.lean

This module contains no declarations of its own: it fixes a scheme X, modules L, M over X, opens U, V and a section s \in \Gamma(M,U) in its variable lines, and serves to make the section-level tensor calculus for sheaves of modules on a scheme available under one import. The notions it collects are the following. On presheaves of modules over R \circ \mathrm{forget}_2 there is an internal hom ihomObj F N, whose value at X is the R(X)-module of families \varphi assigning to each f : X \to Y an R(Y)-linear map F(Y) \to N(Y) subject to the naturality condition N(g)(\varphi_f x) = \varphi_{f \circ g}(F(g)x); currying and uncurrying of maps F \otimes G \to N along pure tensors give an adjunction F \otimes - \dashv \mathrm{ihom}(F,-) and hence a monoidal closed structure. The monoidal, symmetric and closed structures on X-modules are obtained by localising the presheaf-level structures along sheafification, with tensorIsoSheafify identifying the sheafification of L.\mathrm{val} \otimes M.\mathrm{val} with L \otimes M; dual L is \mathrm{ihom}(L, \mathcal O_X). Composing the sheafification unit with that isomorphism yields tensorSectionsHom, and tensorSections s t \in \Gamma(L \otimes M, U) is the image of the pure tensor s \otimes_{\Gamma(X,U)} t; it is \Gamma(X,U)-bilinear, bundled as tensorSectionsBilin, and commutes with restriction. Tensor powers are defined by L^{\otimes 0} = \mathbf 1, L^{\otimes(n+1)} = L^{\otimes n} \otimes L, with unitSection U the unit 1 \in \Gamma(X,U) and tensorPowSection s n the iterated tensor of s with itself. Finally IsFrameOn s V asserts that for every open W with W \le U and W \le V the map \Gamma(X,W) \to \Gamma(M,W), g \mapsto g \cdot (s|_W), is bijective; it is monotone in V, unchanged on replacing V by V \sqcap U, stable under restricting s and under isomorphisms of modules, and holds for the unit section.