The comparison `F ⊗ O(d) ≅ F(d)`, and what follows from it #

#584's remaining structural piece. TwistMultiplication.lean built the map M̃ ⊗ A(d)~ ⟶ M(d)~ and showed what it looks like on a degree-one chart; this file shows the map is inverted by sheafification, and reads off the two deliverables that were waiting on it — F(d)(e) ≅ F(d + e) and preservation of coherence.

The route, and why it is not `Divisors/AssociatedSheaf/Construction.lean`'s #

That file proves the corresponding Cartier statement by exhibiting a generator of the tensor on a chart and finishing by 2-out-of-3. The generator route is unavailable here: it works because both Cartier factors are invertible, so the unit generates the tensor. Only O(d) is invertible here and F is arbitrary.

What replaces it is stronger and shorter. Over an open inside a degree-one chart the twisted multiplication is not merely a local weak equivalence — it is already bijective on sections, because A(d) is there the structure sheaf and the map is the scalar action. So the local input to Presheaf.W_of_coversTop is an isomorphism of presheaves, and no local injectivity or surjectivity has to be proved by hand at all.

Concretely twistMultiplicationHom_app_eq factors the map on sections as

M̃(U) ⊗ A(d)~(U) --(1 ⊗ ψ)--> M̃(U) ⊗ 𝒪(U) --rid--> M̃(U) --φ⁻¹--> M(d)~(U)

with ψ and φ the two chart trivializations. The content of that factorization is one identity, chartModuleTwistSectionEquiv_sectionTwistMul, and it is four lines on top of intShiftZeroModuleLinearEquiv_twistMul: both trivializations are multiplication by the same scalar, so what is left is associativity of that action.

Deliverables #

tensorTwistIso — the comparison, and associatedTensorTwistIso in tensorTwist spelling (2a);
tensorTwistAddIso / associatedTensorTwistAddIso — F(d)(e) ≅ F(d + e) (2b). With the comparison this is sheafTwistAddIso and needs no associator; TensorTwist.lean records why the monoidal structure cannot deliver it directly;
tensorObj_twistingSheaf_isCoherent / tensorTwist_isCoherent — coherence preservation (3), through the graded side, where intShiftModuleOverSelfIso trivializes the twist on a chart. It is not visible through the tensor, which is why it waited on the comparison.

Scope #

F is an associated sheaf. That is the honest statement: identifying an arbitrary coherent sheaf on Proj with an associated one is Serre's theorem, which is downstream — TwistInvertible.lean records the same boundary, and it is why O(d) was proved invertible rather than the tensor avoided.

Two things the section level needs that the fibre level did not #

sectionLinearEquivOfMemIff is the section-level counterpart of DegreeZeroLocalization.linearEquivOfMemIff: intShift 𝓜 0 and 𝓜 have the same members, so the underlying element never moves and only the local-fraction certificate is rebuilt. Both chart trivializations land at the (0)-twist rather than at the module, so this is what closes the gap; Finiteness.lean needs the same step at the sheaf level and gets it from associatedIsoOfPiecewiseIff.

The monoidal structure is TwistMultiplication.lean's local instance, re-enabled here with attribute [local instance] rather than redeclared — a second instance over the same spelling is the mistake references/instance-transparency.md names.

The comparison F ⊗ O(d) ≅ F(d), and what follows from it #

The route, and why it is not Divisors/AssociatedSheaf/Construction.lean's #

Deliverables #

Scope #

Two things the section level needs that the fibre level did not #

The tensorTwist spelling #

The comparison `F ⊗ O(d) ≅ F(d)`, and what follows from it #

The route, and why it is not `Divisors/AssociatedSheaf/Construction.lean`'s #

The `tensorTwist` spelling #