The twisted multiplication `A(d) ⊗ M → M(d)`, at a localization #

#584's remaining piece is the comparison F ⊗ O(d) ≅ F(d) — tensoring with O(d) is shifting the grading by d. Both routes to it need the same thing first: a map, and the map is multiplication of homogeneous fractions. This file supplies it at one localization, with the bilinearity a tensor lift consumes.

Why it is short #

Because of a fact about the model rather than a construction. DegreeZeroLocalization 𝒜 𝓝 S is a submodule of LocalizedModule S M, and for 𝓝 over the ring itself the ambient is LocalizedModule S A, which is Localization S. So an element of DegreeZeroLocalization 𝒜 (intShift 𝒜 d) S is already a scalar acting on LocalizedModule S M: no multiplication has to be defined on representatives, and no well-definedness argument is needed. All that is left is to check the product lands in the right submodule, which is smul_mem_intShift on the numerator and SetLike.mul_mem_graded on the denominator.

This is the same observation that made #689 and #692 tractable — the grading is a property of subobjects of one ambient, not extra structure the ambient knows about.

The one thing that does not come free #

twistMul_smul_right needs SMulCommClass (HomogeneousLocalization 𝒜 S) (LocalizedModule S A) (LocalizedModule S M), which is not an instance. The HomogeneousLocalization 𝒜 S-action is Module.compHom along algebraMap into Localization S, so naming that map moves the goal into Localization S where commutativity is free. The same gap appeared in #695's map_smul'.

Up to the presheaf #

sectionTwistMul is the same product on sections. Its local-fraction certificate is the product of the two factors' certificates on the intersection of their opens, rebuilt by twistMul_mk — which is what that rule exists for. Three details carry the proof: the neighbourhood must be V₁ ⊓ V₂, because each factor's fraction is valid only on its own open; the denominator misses the point by primality, since neither factor's does; and the degree is e₂ + e₁ in that order, because twistMul takes the A(d) factor first.

twistMultiplicationHom is then ModuleCat.MonoidalCategory.tensorLift fed the four laws LinearMap.mk₂ asks for. Note the scalar changes ring between the two levels: a section-level scalar lives in Γ(U, 𝒪) and a fibre-level one in HomogeneousLocalization 𝒜 (primeCompl x), so the two smul laws push it through openToLocalization. The argument order flips with it — section-level left linearity is fibre-level twistMul_*_right.

What the chart sees #

intShiftZeroModuleLinearEquiv_twistMul is the identity the isomorphism proof turns on. On a localization containing a degree-one f, the module trivialization and the ring trivialization are multiplication by the same scalar, so they commute with the product by associativity of that action and nothing else. Read the other way: over a degree-one chart the twisted multiplication is the untwisted one, conjugated by two isomorphisms — which is why the local half of Presheaf.W_of_coversTop should not need the generator machinery Divisors/AssociatedSheaf/Construction.lean builds for the corresponding Cartier statement.

Scope #