The closed monoidal category of sheaves of modules

Let R be a sheaf of commutative rings on a small site. This file makes sheaves of R-modules into a closed symmetric monoidal category. Consequently, tensoring on the left has the internal Hom functor as a right adjoint; Mathlib's standard ihom.adjunction, ihom.ev, and ihom.coev provide the tensor--Hom adjunction, evaluation, and coevaluation.

Presheaves of modules form a closed monoidal category by TauCeti.PresheafOfModules.monoidalClosed. Day's reflection theorem transports this closed structure across the reflective sheafification adjunction. Thus the internal Hom of sheaves is the sheafification of the presheaf internal Hom.

Main declarations

• TauCeti.SheafOfModules.presheafMonoidalClosed transfers the closed structure of TauCeti.PresheafOfModules.monoidalClosed to presheaves of modules over the ring presheaf underlying R;
• TauCeti.SheafOfModules.monoidalClosed gives the closed structure on sheaves of modules;
• TauCeti.SheafOfModules.monoidalPreadditive makes tensoring additive in each variable;
• SheafOfModules.ihom_obj identifies its internal Hom object with the sheafification of the presheaf internal Hom;
• SheafOfModules.dual and SheafOfModules.dualIso give the internal-Hom dual and its action on isomorphisms.

The use of the special adjoint functor theorem and Day reflection follows the construction of closed monoidal structures on sheaf categories in Mathlib's CategoryTheory.Monoidal.Braided.Reflection and Condensed.Light.Monoidal.

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.presheafMonoidalClosed {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] (R : CategoryTheory.Sheaf J CommRingCat) : CategoryTheory.MonoidalClosed (PresheafOfModules (ringCatSheaf R).obj)

The closed monoidal structure on presheaves of modules over the ring presheaf underlying R, transferred from TauCeti.PresheafOfModules.monoidalClosed so that instance search finds it at (ringCatSheaf R).obj.

Equations

• TauCeti.SheafOfModules.presheafMonoidalClosed R = { closed := TauCeti.SheafOfModules.presheafMonoidalClosed._aux_1 R }

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.monoidalClosed {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) : CategoryTheory.MonoidalClosed (SheafOfModules (ringCatSheaf R))

The closed symmetric monoidal structure on sheaves of R-modules. It is obtained from the closed structure on presheaves of modules by Day's reflection theorem.

Equations

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

instance TauCeti.SheafOfModules.monoidalPreadditive {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J CommRingCat) : CategoryTheory.MonoidalPreadditive (SheafOfModules (ringCatSheaf R))

The tensor product of sheaves of modules is additive in each variable.

@[simp]

theorem SheafOfModules.ihom_obj {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : (CategoryTheory.ihom M).obj N = (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).obj ((CategoryTheory.ihom M.val).obj N.val)

The internal Hom of sheaves of modules is the sheafification of the internal Hom of their underlying presheaves of modules.

@[simp]

theorem SheafOfModules.ihom_map {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) {N P : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (f : N ⟶ P) : (CategoryTheory.ihom M).map f = (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map ((CategoryTheory.ihom M.val).map f.val)

On morphisms, the internal Hom of sheaves of modules is induced by sheafification from the internal Hom of presheaves of modules.

@[reducible, inline]

noncomputable abbrev SheafOfModules.dual {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)

The internal-Hom dual of a sheaf of modules.

Equations

• M.dual = (CategoryTheory.ihom M).obj (SheafOfModules.unit (TauCeti.SheafOfModules.ringCatSheaf R))

noncomputable def SheafOfModules.dualIso {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (e : M ≅ N) : M.dual ≅ N.dual

An isomorphism of sheaves induces an isomorphism of their duals.

Equations

• SheafOfModules.dualIso e = CategoryTheory.asIso ((CategoryTheory.MonoidalClosed.pre e.inv).app (SheafOfModules.unit (TauCeti.SheafOfModules.ringCatSheaf R)))

@[simp]

theorem SheafOfModules.dualIso_hom {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (e : M ≅ N) : (dualIso e).hom = (CategoryTheory.MonoidalClosed.pre e.inv).app (unit (TauCeti.SheafOfModules.ringCatSheaf R))

The forward map on duals induced by an isomorphism is precomposition with its inverse.

@[simp]

theorem SheafOfModules.dualIso_inv {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (e : M ≅ N) : (dualIso e).inv = (CategoryTheory.MonoidalClosed.pre e.hom).app (unit (TauCeti.SheafOfModules.ringCatSheaf R))

The inverse map on duals induced by an isomorphism is precomposition with its forward map.