The symmetric monoidal category of sheaves of modules

Let R be a sheaf of commutative rings on a small site (C, J). This file equips the category of sheaves of R-modules with a symmetric monoidal category structure whose tensor product is the sheafification of the sectionwise tensor product of the underlying presheaves of modules, and whose unit is R itself.

The structure is obtained by localization. Sheafification PresheafOfModules ⥤ SheafOfModules is a localization functor with respect to the local isomorphisms of presheaves of modules (Mathlib's PresheafOfModules.sheafification instance of Functor.IsLocalization), and local isomorphisms are stable under the sectionwise tensor product (PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf). Mathlib's localized monoidal structure CategoryTheory.LocalizedMonoidal (with its braided and symmetric refinements) then provides the monoidal category structure, the coherence laws, and the braiding on the target of the localization functor, for which sheafification is a braided monoidal functor.

Main declarations

• SheafOfModules.monoidalCategory and SheafOfModules.symmetricCategory: the symmetric monoidal category structure on sheaves of R-modules;
• SheafOfModules.tensorUnit_eq: its unit is the sheaf of modules R itself;
• SheafOfModules.sheafificationMonoidal and SheafOfModules.sheafificationBraided: sheafification of presheaves of modules is a braided monoidal functor, whose unit comparison is SheafOfModules.sheafificationUnitIso (SheafOfModules.sheafification_ε);
• SheafOfModules.tensorUnderlyingIso: the identification of M ⊗ N with the sheafification of the sectionwise tensor product of the underlying presheaves of modules, natural in M and N (SheafOfModules.tensorUnderlyingIso_naturality) and compatible with the braiding and the unitors.
• SheafOfModules.sheafificationForgetAdjunction, SheafOfModules.forgetLaxMonoidal, and SheafOfModules.forgetLaxBraided: sheafification is left adjoint to the inclusion of sheaves of modules into presheaves of modules, which is therefore lax monoidal, with unit map the identity (SheafOfModules.forget_ε) and tensor map the unit of sheafification (SheafOfModules.forget_μ);
• SheafOfModules.tensor_hom_ext: morphisms out of M ⊗ N are determined by their restriction along that tensor map to the sectionwise tensor product.

The tensor object M ⊗ N and the sheaf SheafOfModules.tensorProduct R M N are both sheafifications of M.val ⊗ N.val, through tensorUnderlyingIso and tensorProductIso respectively.

The site is assumed small, with modules in the universe of its objects and morphisms, because the stability of local isomorphisms under tensor products is established in that generality.

instance TauCeti.SheafOfModules.isMonoidal_inverseImage_W_toPresheaf {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) : (J.W.inverseImage (PresheafOfModules.toPresheaf (ringCatSheaf R).obj)).IsMonoidal

Local isomorphisms of presheaves of modules over the sheaf of rings underlying a sheaf of commutative rings form a monoidal morphism property.

noncomputable def TauCeti.SheafOfModules.sheafificationUnitIso {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) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModules (ringCatSheaf R).obj)) ≅ SheafOfModules.unit (ringCatSheaf R)

Sheafifying the unit presheaf of modules recovers the sheaf of modules R itself. This is the unit datum from which the localized monoidal structure is built.

Equations

• TauCeti.SheafOfModules.sheafificationUnitIso R = TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) (SheafOfModules.unit (TauCeti.SheafOfModules.ringCatSheaf R))

theorem TauCeti.SheafOfModules.sheafificationUnitIso_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) : (sheafificationUnitIso R).hom = (PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).counit.app (SheafOfModules.unit (ringCatSheaf R))

The forward map of sheafificationUnitIso is the counit of the sheafification adjunction at the sheaf of modules R.

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.monoidalCategory {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.MonoidalCategory (SheafOfModules (ringCatSheaf R))

The monoidal category structure on sheaves of R-modules: the tensor product is the sheafification of the sectionwise tensor product, and the unit is R. It is the localized monoidal structure along sheafification.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.symmetricCategory {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.SymmetricCategory (SheafOfModules (ringCatSheaf R))

The symmetric monoidal category structure on sheaves of R-modules, whose braiding is induced by the symmetry of the sectionwise tensor product.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.tensorUnit_eq {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.MonoidalCategoryStruct.tensorUnit (SheafOfModules (ringCatSheaf R)) = SheafOfModules.unit (ringCatSheaf R)

The unit of the monoidal structure on sheaves of R-modules is R itself.

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.sheafificationMonoidal {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) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).Monoidal

Sheafification of presheaves of modules is a monoidal functor.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.sheafificationBraided {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) : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).Braided

Sheafification of presheaves of modules is a braided monoidal functor.

Equations

• TauCeti.SheafOfModules.sheafificationBraided R = { toMonoidal := TauCeti.SheafOfModules.sheafificationMonoidal R, braided := ⋯ }

@[simp]

theorem TauCeti.SheafOfModules.sheafification_ε {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.Functor.LaxMonoidal.ε (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)) = (sheafificationUnitIso R).inv

The unit comparison of the monoidal functor sheafification is the inverse of sheafificationUnitIso.

@[simp]

theorem TauCeti.SheafOfModules.sheafification_η {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.Functor.OplaxMonoidal.η (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)) = (sheafificationUnitIso R).hom

The inverse unit comparison of the monoidal functor sheafification is sheafificationUnitIso.

noncomputable def SheafOfModules.tensorUnderlyingIso {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.MonoidalCategoryStruct.tensorObj M N ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)

The tensor product of two sheaves of R-modules is the sheafification of the sectionwise tensor product of their underlying presheaves of modules.

Equations

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

theorem SheafOfModules.tensorUnderlyingIso_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)) : (M.tensorUnderlyingIso N).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).inv (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) N).inv) (CategoryTheory.Functor.LaxMonoidal.μ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)) M.val N.val)

The forward map of tensorUnderlyingIso: the inverses of sheafificationIso on both factors, followed by the tensor map of sheafification.

theorem SheafOfModules.tensorUnderlyingIso_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)) : (M.tensorUnderlyingIso N).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)) M.val N.val) (CategoryTheory.MonoidalCategoryStruct.tensorHom (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) N).hom)

The inverse map of tensorUnderlyingIso: the inverse tensor map of sheafification, followed by sheafificationIso on both factors.

theorem SheafOfModules.tensorUnderlyingIso_naturality {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 M' N N' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (f : M ⟶ M') (g : N ⟶ N') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (M'.tensorUnderlyingIso N').hom = CategoryTheory.CategoryStruct.comp (M.tensorUnderlyingIso N).hom ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f.val g.val))

tensorUnderlyingIso is natural: under it, the tensor product of two morphisms of sheaves of modules is the sheafification of the sectionwise tensor product of their underlying morphisms.

theorem SheafOfModules.tensorUnderlyingIso_naturality_assoc {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 M' N N' : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (f : M ⟶ M') (g : N ⟶ N') {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj M'.val N'.val) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (CategoryTheory.CategoryStruct.comp (M'.tensorUnderlyingIso N').hom h) = CategoryTheory.CategoryStruct.comp (M.tensorUnderlyingIso N).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f.val g.val)) h)

tensorUnderlyingIso is natural: under it, the tensor product of two morphisms of sheaves of modules is the sheafification of the sectionwise tensor product of their underlying morphisms.

theorem SheafOfModules.braiding_hom_tensorUnderlyingIso_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)) : CategoryTheory.CategoryStruct.comp (β_ M N).hom (N.tensorUnderlyingIso M).hom = CategoryTheory.CategoryStruct.comp (M.tensorUnderlyingIso N).hom ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (β_ M.val N.val).hom)

Under tensorUnderlyingIso, the braiding of sheaves of modules is the sheafification of the braiding of the sectionwise tensor product.

theorem SheafOfModules.braiding_hom_tensorUnderlyingIso_hom_assoc {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)) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj N.val M.val) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ M N).hom (CategoryTheory.CategoryStruct.comp (N.tensorUnderlyingIso M).hom h) = CategoryTheory.CategoryStruct.comp (M.tensorUnderlyingIso N).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (β_ M.val N.val).hom) h)

Under tensorUnderlyingIso, the braiding of sheaves of modules is the sheafification of the braiding of the sectionwise tensor product.

theorem SheafOfModules.leftUnitor_hom_eq {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)) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (TauCeti.SheafOfModules.sheafificationUnitIso R).inv (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)) (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj)) M.val) (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (CategoryTheory.MonoidalCategoryStruct.leftUnitor M.val).hom) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom))

The left unitor of sheaves of modules is the sheafification of the left unitor of the sectionwise tensor product, read through the unit comparison sheafificationUnitIso.

theorem SheafOfModules.rightUnitor_hom_eq {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)) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).inv (TauCeti.SheafOfModules.sheafificationUnitIso R).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)) M.val (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R).obj))) (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (CategoryTheory.MonoidalCategoryStruct.rightUnitor M.val).hom) (TauCeti.SheafOfModules.sheafificationIso (TauCeti.SheafOfModules.ringCatSheaf R) M).hom))

The right unitor of sheaves of modules is the sheafification of the right unitor of the sectionwise tensor product, read through the unit comparison sheafificationUnitIso.

noncomputable def TauCeti.SheafOfModules.sheafificationForgetAdjunction {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) : PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj) ⊣ SheafOfModules.forget (ringCatSheaf R)

Sheafification of presheaves of modules is left adjoint to the inclusion SheafOfModules.forget of sheaves of modules. This is Mathlib's PresheafOfModules.sheafificationAdjunction along the identity of the sheaf of rings, whose right adjoint forget ⋙ restrictScalars (𝟙 _) is definitionally forget.

Equations

• TauCeti.SheafOfModules.sheafificationForgetAdjunction R = PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)

theorem TauCeti.SheafOfModules.sheafificationForgetAdjunction_counit_app {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 (ringCatSheaf R)) : (sheafificationForgetAdjunction R).counit.app M = (sheafificationIso (ringCatSheaf R) M).hom

The counit of sheafificationForgetAdjunction at a sheaf of modules M is the identification sheafificationIso of the sheafification of M.val with M.

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.forgetLaxMonoidal {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) : (SheafOfModules.forget (ringCatSheaf R)).LaxMonoidal

The inclusion of sheaves of modules into presheaves of modules is lax monoidal, as the right adjoint of the monoidal functor sheafification. Its tensor map M.val ⊗ N.val ⟶ (M ⊗ N).val is the unit of sheafification (SheafOfModules.forget_μ), and its unit map is the identity (SheafOfModules.forget_ε).

Equations

• TauCeti.SheafOfModules.forgetLaxMonoidal R = (TauCeti.SheafOfModules.sheafificationForgetAdjunction R).rightAdjointLaxMonoidal

@[instance_reducible]

noncomputable instance TauCeti.SheafOfModules.forgetLaxBraided {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) : (SheafOfModules.forget (ringCatSheaf R)).LaxBraided

The inclusion of sheaves of modules into presheaves of modules respects symmetry, as the right adjoint of braided monoidal sheafification.

Equations

• TauCeti.SheafOfModules.forgetLaxBraided R = { toLaxMonoidal := TauCeti.SheafOfModules.forgetLaxMonoidal R, braided := ⋯ }

@[simp]

theorem TauCeti.SheafOfModules.forget_ε {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.Functor.LaxMonoidal.ε (SheafOfModules.forget (ringCatSheaf R)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModules (ringCatSheaf R).obj))

The unit map of the inclusion of sheaves of modules into presheaves of modules is the identity.

theorem TauCeti.SheafOfModules.forget_μ {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 (ringCatSheaf R)) : CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (ringCatSheaf R)) M N = CategoryTheory.CategoryStruct.comp ((sheafificationForgetAdjunction R).unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)) ((SheafOfModules.forget (ringCatSheaf R)).map (M.tensorUnderlyingIso N).inv)

The tensor map M.val ⊗ N.val ⟶ (M ⊗ N).val of the inclusion of sheaves of modules into presheaves of modules is the unit of sheafification, followed by the identification tensorUnderlyingIso of M ⊗ N with the sheafification of M.val ⊗ N.val.

theorem TauCeti.SheafOfModules.forget_μ_comp_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 N P : SheafOfModules (ringCatSheaf R)} (p : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (ringCatSheaf R)) M N) ((SheafOfModules.forget (ringCatSheaf R)).map p) = ((sheafificationForgetAdjunction R).homEquiv (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val) P) (CategoryTheory.CategoryStruct.comp (M.tensorUnderlyingIso N).inv p)

A morphism out of M ⊗ N, precomposed on underlying presheaves with the tensor map M.val ⊗ N.val ⟶ (M ⊗ N).val of forget, is the transpose along sheafification of the morphism read through tensorUnderlyingIso.

theorem TauCeti.SheafOfModules.tensor_hom_ext {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 P : SheafOfModules (ringCatSheaf R)} {p q : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (ringCatSheaf R)) M N) ((SheafOfModules.forget (ringCatSheaf R)).map p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (ringCatSheaf R)) M N) ((SheafOfModules.forget (ringCatSheaf R)).map q)) : p = q

Two morphisms out of a tensor product M ⊗ N of sheaves of modules agree as soon as they agree on the sectionwise tensor product M.val ⊗ N.val of the underlying presheaves of modules, that is, after precomposition with the tensor map of forget.