Towards the monoidal structure on sheaves of modules ([GAP1-W-MONO]) #
The AINTLIB ModularCurves GAP-1 development, route (b′) (board v10.64/v10.65): equip
SheafOfModules with a monoidal structure by localizing the monoidal category of
presheaves of modules at the class of morphisms inverted by sheafification, via
mathlib's LocalizedMonoidal machinery. The single load-bearing mathematical leaf is
tensor-stability of that class; everything else is registration plumbing.
PresheafOfModules.sheafificationW: the inverted class.sheafificationW_isLocalization: theIsLocalizationregistration atα = 𝟙(reflective case), viaAdjunction.isLocalization.sheafificationW_iff_isLocallyBijective: membership = locally injective + locally surjective on underlying presheaves of abelian groups (through mathlib'sWEqualsLocallyBijectiveand the reflection of isomorphisms bytoSheaf).[GAP1-W-MONO](staged): tensor-stability. The locally-surjective half (IsLocallySurjective.tensorHom) is proven at the level of sections; the locally-injective half (IsLocallyInjective.tensorHom) is the stalkwise/filtered argument (no flatness — stalks of a locally bijective map are isomorphisms) and is a registered work-in-progress leaf.
Once the leaf closes, LocalizedMonoidal (sheafification (𝟙 _)) (sheafificationW _) ε
with ε the sheafified-unit counit iso hands SheafOfModules its monoidal structure
with monoidal sheafification — the GAP-1 kernel, tensor-closure of invertible sheaves,
and the Pic-group coherences (board v10.64).
The class of morphisms of presheaves of modules inverted by the sheafification
functor: the localizing class for SheafOfModules.
Equations
Instances For
Membership in the localizing class is local bijectivity of the underlying morphism of presheaves of abelian groups: the sheafification of modules inverts exactly the locally bijective maps.
At α = 𝟙 the sheafification adjunction is reflective (forget is fully faithful
and restrictScalars (𝟙 _) is an equivalence), so the sheafification functor is a
localization at sheafificationW.
The locally-surjective half of the [GAP1-W-MONO] tensor-stability leaf: the tensor product of locally surjective morphisms of presheaves of modules is locally surjective. Sections of the tensor presheaf are finite sums of simple tensors; each factor is locally hit, and the finitely many image sieves intersect to a covering sieve.
([W-MONO-inj]) Precomposition with the tensor of locally surjective morphisms
is injective on morphisms into a presheaf of modules whose underlying presheaf is a
sheaf: two maps out of the tensor agreeing after f ⊗ₘ g agree on simple tensors
locally, hence agree by separatedness.
([W-MONO-glue]) Precomposition with the tensor of locally bijective morphisms
is surjective on morphisms into a presheaf of modules whose underlying presheaf is a
sheaf: every χ factors through the glued bilinear pairing.
([GAP1-W-MONO], the leaf) The class of morphisms inverted by sheafification of
modules is closed under tensor product. Proof: sheafificationW-membership is local
bijectivity (the bridge), so f, g locally bijective make precomposition with
f ⊗ₘ g a bijection on morphisms into every sheaf-underlying target
(tensorHom_precomp_injective/_surjective); transporting that bijection across the
sheafification adjunction homEquiv (naturality-left) and detecting isomorphisms by
coyoneda-bijectivity shows (sheafification α).map (f ⊗ₘ g) is an isomorphism. No
flatness and no stalks — the topos-theoretic replacement for the pointwise argument.
([GAP1-W-MONO], corollary — the original loc-injective claim) The tensor product of
morphisms inverted by sheafification is locally injective on underlying presheaves. This was
the staged stalkwise leaf; it now follows free from sheafificationW_tensorHom through the
local-bijectivity bridge, with the sheafification datum α standing in for the stalks a
general site lacks: f, g locally bijective (i.e. sheafificationW α-members) ⟹
sheafificationW α (f ⊗ₘ g) ⟹ its underlying presheaf map is locally bijective, in
particular locally injective. (The bare statement over an arbitrary presheaf of commutative
rings, with only local-bijectivity instances and no α, is not closable — the sheafification
adjunction is the topos-theoretic replacement for a pointwise/stalkwise argument — so this
carries α and the sheafificationW hypotheses rather than the byte-identical staged
signature; obtain those hypotheses from local-bijectivity via
sheafificationW_iff_isLocallyBijective.)
([GAP1-W-MONO]) The localizing class sheafificationW is monoidal: multiplicative
(registration) and closed under ⊗ₘ (sheafificationW_tensorHom). This is the sole
hypothesis, beyond the localization registration, that LocalizedMonoidal needs to hand
SheafOfModules its monoidal structure.
The reflective localization registration, specialised to the ring sheaf underlying a
sheaf of commutative rings (with R' spelled literally so type-class resolution matches it
directly, rather than having to invert the .obj projection). Delegates to
sheafificationW_isLocalization.
The monoidality of the localizing class, specialised to the same ring sheaf (again with
R' spelled literally for direct resolution). Delegates to sheafificationW_isMonoidal
(this file's leaf).
([GAP1-W-MONO] — the payoff) The LocalizedMonoidal instantiation resolves: fed the
two registrations above (the reflective localization and the monoidality of the localizing
class — this file's leaf), mathlib's LocalizedMonoidal equips the localization of
presheaves of modules over a sheaf of commutative rings with a MonoidalCategory structure.
That localized category is definitionally SheafOfModules ⟨S ⋙ forget₂ _ _, hS⟩ — so
sheaves of modules over a sheaf of commutative rings form a monoidal category,
monoidally under sheafification. This is the GAP-1 payoff; downstream consumers name the
localized category and read off the tensor product, unit, and Pic coherences.