Monoidal category structure on categories of sheaves

If A is a closed braided category with suitable limits, and J is a Grothendieck topology with HasWeakSheafify J A, then Sheaf J A can be equipped with a monoidal category structure. This is not made an instance as in some cases it may conflict with monoidal structure deduced from chosen finite products.

TODO

• show that the monoidal category structure on sheaves is closed, and that the internal hom can be defined in such a way that the underlying presheaf is the internal hom in the category of presheaves. Note that a MonoidalClosed instance on sheaves can already be obtained abstractly using the material in CategoryTheory.Monoidal.Braided.Reflection.

noncomputable def CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] (M : A) (F G : Functor Cᵒᵖ A) [Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] (X : C) : ((Enriched.FunctorCategory.functorEnrichedHom A F G).comp (coyoneda.obj (Opposite.op M))).obj (Opposite.op X) ≃ (presheafHom (MonoidalCategoryStruct.tensorObj F ((Functor.const Cᵒᵖ).obj M)) G).obj (Opposite.op X)

Relation between functorEnrichedHom and presheafHom.

theorem CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] {M : A} {F G : Functor Cᵒᵖ A} {X Y : C} (f : X ⟶ Y) [Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] (y : ((Enriched.FunctorCategory.functorEnrichedHom A F G).comp (coyoneda.obj (Opposite.op M))).obj (Opposite.op Y)) : (functorEnrichedHomCoyonedaObjEquiv M F G X) (CategoryStruct.comp y (Enriched.FunctorCategory.precompEnrichedHom' A (Under.map f.op) (Iso.refl ((Under.map f.op).comp ((Under.forget (Opposite.op Y)).comp F))) (Iso.refl ((Under.map f.op).comp ((Under.forget (Opposite.op Y)).comp G))))) = (presheafHom (MonoidalCategoryStruct.tensorObj F ((Functor.const Cᵒᵖ).obj M)) G).map f.op ((functorEnrichedHomCoyonedaObjEquiv M F G Y) y)

theorem CategoryTheory.Presheaf.isSheaf_functorEnrichedHom {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] (F G : Functor Cᵒᵖ A) (hG : IsSheaf J G) [Enriched.FunctorCategory.HasFunctorEnrichedHom A F G] : IsSheaf J (Enriched.FunctorCategory.functorEnrichedHom A F G)

theorem CategoryTheory.GrothendieckTopology.W.transport_isMonoidal {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] {D : Type u₂} [Category.{v₂, u₂} D] (K : GrothendieckTopology D) (G : Functor D C) [G.IsCoverDense J] [G.Full] [G.IsContinuous K J] [(G.sheafPushforwardContinuous A K J).EssSurj] [K.W.IsMonoidal] : J.W.IsMonoidal

theorem CategoryTheory.GrothendieckTopology.W.whiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂] {G₁ G₂ : Functor Cᵒᵖ A} {g : G₁ ⟶ G₂} (hg : J.W g) (F : Functor Cᵒᵖ A) : J.W (MonoidalCategoryStruct.whiskerLeft F g)

theorem CategoryTheory.GrothendieckTopology.W.whiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂] [BraidedCategory A] {F₁ F₂ : Functor Cᵒᵖ A} {f : F₁ ⟶ F₂} (hf : J.W f) (G : Functor Cᵒᵖ A) : J.W (MonoidalCategoryStruct.whiskerRight f G)

instance CategoryTheory.GrothendieckTopology.W.monoidal {C : Type u₁} [Category.{v₁, u₁} C] {J : GrothendieckTopology C} {A : Type u₃} [Category.{v₃, u₃} A] [MonoidalCategory A] [MonoidalClosed A] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂] [∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂] [BraidedCategory A] : J.W.IsMonoidal

noncomputable def CategoryTheory.Sheaf.monoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] [J.W.IsMonoidal] [HasWeakSheafify J A] : MonoidalCategory (Sheaf J A)

The monoidal category structure on Sheaf J A that is obtained by localization of the monoidal category structure on the category of presheaves.

noncomputable def CategoryTheory.Sheaf.braidedCategory {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] [J.W.IsMonoidal] [HasWeakSheafify J A] [BraidedCategory A] : BraidedCategory (Sheaf J A)

The monoidal category structure on Sheaf J A obtained in Sheaf.monoidalCategory is braided when A is braided.

noncomputable def CategoryTheory.Sheaf.symmetricCategory {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] [J.W.IsMonoidal] [HasWeakSheafify J A] [SymmetricCategory A] : SymmetricCategory (Sheaf J A)

The monoidal category structure on Sheaf J A obtained in Sheaf.monoidalCategory is symmetric when A is symmetric.

noncomputable instance CategoryTheory.Sheaf.instMonoidalFunctorOppositePresheafToSheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] [J.W.IsMonoidal] [HasWeakSheafify J A] : (presheafToSheaf J A).Monoidal

noncomputable instance CategoryTheory.Sheaf.instBraidedFunctorOppositePresheafToSheaf {C : Type u₁} [Category.{v₁, u₁} C] (J : GrothendieckTopology C) (A : Type u₃) [Category.{v₃, u₃} A] [MonoidalCategory A] [J.W.IsMonoidal] [HasWeakSheafify J A] [BraidedCategory A] : (presheafToSheaf J A).Braided