Fiber functors are monoidal

Let Φ be a point of a site (C, J). Let A be a monoidal category where the tensor product commutes with filtered colimits in both variables. We show that the fiber functors Φ.presheafFiber : (Cᵒᵖ ⥤ A) ⥤ A and Φ.sheafFiber : Sheaf J A ⥤ A are monoidal.

@[implicit_reducible]

noncomputable instance CategoryTheory.GrothendieckTopology.Point.instOplaxMonoidalFunctorOppositePresheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] : Φ.presheafFiber.OplaxMonoidal

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) : CategoryStruct.comp (Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorUnit (Functor Cᵒᵖ A))) (Functor.OplaxMonoidal.η Φ.presheafFiber) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit A)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_η_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) {Z : A} (h : MonoidalCategoryStruct.tensorUnit A ⟶ Z) : CategoryStruct.comp (Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorUnit (Functor Cᵒᵖ A))) (CategoryStruct.comp (Functor.OplaxMonoidal.η Φ.presheafFiber) h) = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit A)) h

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : Functor Cᵒᵖ A) : CategoryStruct.comp (Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorObj G₁ G₂)) (Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) = MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : Functor Cᵒᵖ A) {Z : A} (h : MonoidalCategoryStruct.tensorObj (Φ.presheafFiber.obj G₁) (Φ.presheafFiber.obj G₂) ⟶ Z) : CategoryStruct.comp (Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorObj G₁ G₂)) (CategoryStruct.comp (Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) h

instance CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorFlipCurriedTensor {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] (M : A) : Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((MonoidalCategory.curriedTensor A).flip.obj M)

instance CategoryTheory.GrothendieckTopology.Point.instPreservesColimitsOfShapeOppositeElementsFiberObjFunctorCurriedTensor {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] (M : A) : Limits.PreservesColimitsOfShape Φ.fiber.Elementsᵒᵖ ((MonoidalCategory.curriedTensor A).obj M)

instance CategoryTheory.GrothendieckTopology.Point.instIsIsoηFunctorOppositePresheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] : IsIso (Functor.OplaxMonoidal.η Φ.presheafFiber)

instance CategoryTheory.GrothendieckTopology.Point.instIsIsoδFunctorOppositePresheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] (P₁ P₂ : Functor Cᵒᵖ A) : IsIso (Functor.OplaxMonoidal.δ Φ.presheafFiber P₁ P₂)

@[implicit_reducible]

noncomputable instance CategoryTheory.GrothendieckTopology.Point.instMonoidalFunctorOppositePresheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] : Φ.presheafFiber.Monoidal

Equations

• Φ.instMonoidalFunctorOppositePresheafFiber = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal Φ.presheafFiber

theorem CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_ε {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) : Functor.LaxMonoidal.ε Φ.presheafFiber = Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorUnit (Functor Cᵒᵖ A))

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : Functor Cᵒᵖ A) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) = Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorObj G₁ G₂)

@[simp]

theorem CategoryTheory.GrothendieckTopology.Point.tensorHom_comp_toPresheafFiber_μ_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] (X : C) (x : Φ.fiber.obj X) (G₁ G₂ : Functor Cᵒᵖ A) {Z : A} (h : Φ.presheafFiber.obj (MonoidalCategoryStruct.tensorObj G₁ G₂) ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)) (CategoryStruct.comp (Functor.LaxMonoidal.μ Φ.presheafFiber G₁ G₂) h) = CategoryStruct.comp (Φ.toPresheafFiber X x (MonoidalCategoryStruct.tensorObj G₁ G₂)) h

@[implicit_reducible]

noncomputable instance CategoryTheory.GrothendieckTopology.Point.instMonoidalSheafSheafFiber {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [HasWeakSheafify J A] [Limits.HasProducts A] : Φ.sheafFiber.Monoidal

Equations

• Φ.instMonoidalSheafSheafFiber = CategoryTheory.Localization.Monoidal.functorMonoidalOfComp (CategoryTheory.presheafToSheaf J A) J.W Φ.sheafFiber Φ.presheafFiber

instance CategoryTheory.GrothendieckTopology.Point.instIsMonoidalFunctorOppositeHomPresheafToSheafCompSheafFiberIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (Φ : J.Point) {A : Type u'} [Category.{v', u'} A] [MonoidalCategory A] [Limits.HasColimitsOfSize.{w, w, v', u'} A] [LocallySmall.{w, v, u} C] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)] [∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)] [J.W.IsMonoidal] [HasWeakSheafify J A] [Limits.HasProducts A] : NatTrans.IsMonoidal (Φ.presheafToSheafCompSheafFiberIso A).hom