Monoidal comparisons for scheme-module pullback

The sheafified tensor product is the canonical monoidal structure on all scheme-module sheaves. Consequently, strong monoidality of Mathlib's existing pullback f functor is expressed by the standard Functor.Monoidal class, not by a parallel repository-specific capability or carrier.

At the current Mathlib pin the strong-monoidal instance itself is an external input. This module names its two standard comparison isomorphisms so line bundles, determinants, Picard classes, and the projection-formula lane can share one API while the construction of that instance is pursued.

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackTensorIso {X Y : Scheme} (f : X ⟶ Y) [(pullback f).Monoidal] (M N : Y.Modules) : ((pullback f).obj M).tensorObj ((pullback f).obj N) ≅ (pullback f).obj (M.tensorObj N)

The tensor comparison supplied by a standard strong-monoidal structure on module pullback.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackTensorIso f M N = id (CategoryTheory.Functor.Monoidal.μIso (AlgebraicGeometry.Scheme.Modules.pullback f) M N)

noncomputable def AlgebraicGeometry.Scheme.Modules.pullbackUnitIso {X Y : Scheme} (f : X ⟶ Y) [(pullback f).Monoidal] : (pullback f).obj (SheafOfModules.unit Y.ringCatSheaf) ≅ SheafOfModules.unit X.ringCatSheaf

The unit comparison supplied by a standard strong-monoidal structure on module pullback.

Equations

• AlgebraicGeometry.Scheme.Modules.pullbackUnitIso f = id (CategoryTheory.Functor.Monoidal.εIso (AlgebraicGeometry.Scheme.Modules.pullback f)).symm