Closed Symmetric Monoidal

Stream: Copenhagen Masterclass 2023

[Jon Eugster]

Consider the #mwe below. Does anybody know if the last two sorrys are solved easily using some results from the library?

import Mathlib

universe u

noncomputable section

open CategoryTheory Limits

/-- `Ab` is the category of `ℤ`-modules -/
lemma moduleCat_int_equiv_ab : ModuleCat.{u} (ULift.{u} ℤ) ≌ Ab.{u} := sorry

/-- The monoidal structure on `Ab` is induced by the one on `ℤ`-modules. -/
instance : MonoidalCategory Ab := Monoidal.transport moduleCat_int_equiv_ab

/- Move Limits across the iso above. This should be straight forward -/
#synth PreservesLimits <| forget (ModuleCat.{u} (ULift.{u} ℤ))
instance : PreservesLimits (forget Ab.{u+1}) := sorry

variable {C : Type (u+1)} [c : Category.{u} C] (J : GrothendieckTopology C)

open MonoidalCategory

/-- `S(SF ⊗ G) ≅ S(F ⊗ G)` where `S` is the sheafification. -/
def helper_1 (F G : Cᵒᵖ ⥤ Ab.{u+1}) :
    (presheafToSheaf J Ab).obj (tensorObj (J.sheafify F) G) ≅
    (presheafToSheaf J Ab).obj (tensorObj F G) :=
  sorry -- HERE: Does the library have something related?


/-- `S(F ⊗ SG) ≅ S(F ⊗ G)` where `S` is the sheafification. -/
def helper_2 (F G : Cᵒᵖ ⥤ Ab.{u+1}) :
    (presheafToSheaf J Ab).obj (tensorObj F (J.sheafify G)) ≅
    (presheafToSheaf J Ab).obj (tensorObj F G) :=
  sorry -- HERE: Does the library have something related?

[Johan Commelin]

If you show that the category of presheaves is closed monoidal, then I think you can get quite far by using the tensor-hom adjunction.

[Jon Eugster]

(deleted)

[Jon Eugster]

ok we already have the result that the category od presheaves is closed monoidal, thats good

[Jon Eugster]

my internet... :(