The closed monoidal category of presheaves of modules

Let R₀ be a presheaf of commutative rings on a small category. This file makes presheaves of R₀-modules into a closed monoidal category. Tensoring presheaves of modules preserves small colimits, and the free modules on representables form a small separating family, so the special adjoint functor theorem gives a right adjoint to tensoring by each presheaf of modules.

Main declarations

• TauCeti.PresheafOfModules.monoidalClosed gives the closed structure on presheaves of modules over a presheaf of commutative rings.

@[instance_reducible]

noncomputable instance TauCeti.PresheafOfModules.monoidalClosed {C : Type u} [CategoryTheory.SmallCategory C] (R₀ : CategoryTheory.Functor Cᵒᵖ CommRingCat) : CategoryTheory.MonoidalClosed (PresheafOfModules (R₀.comp (CategoryTheory.forget₂ CommRingCat RingCat)))

The closed monoidal structure on presheaves of modules over a presheaf of commutative rings. Its internal Hom is the right adjoint supplied by the special adjoint functor theorem.

Equations

• One or more equations did not get rendered due to their size.