Chosen finite products on sheaves

In this file, we put a CartesianMonoidalCategory instance on A-valued sheaves for a GrothendieckTopology whenever A has a CartesianMonoidalCategory instance.

theorem CategoryTheory.Sheaf.tensorProd_isSheaf {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] (X Y : Sheaf J A) : Presheaf.IsSheaf J (MonoidalCategoryStruct.tensorObj X.val Y.val)

theorem CategoryTheory.Sheaf.tensorUnit_isSheaf {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : Presheaf.IsSheaf J (MonoidalCategoryStruct.tensorUnit (Functor Cᵒᵖ A))

noncomputable instance CategoryTheory.Sheaf.cartesianMonoidalCategory {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : CartesianMonoidalCategory (Sheaf J A)

Any CartesianMonoidalCategory on A induce a CartesianMonoidalCategory structure on A-valued sheaves.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] (X Y : Sheaf J A) : (CartesianMonoidalCategory.fst X Y).val = CartesianMonoidalCategory.fst X.val Y.val

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] (X Y : Sheaf J A) : (CartesianMonoidalCategory.snd X Y).val = CartesianMonoidalCategory.snd X.val Y.val

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] {X Y W : Sheaf J A} (f : W ⟶ X) (g : W ⟶ Y) : (CartesianMonoidalCategory.lift f g).val = CartesianMonoidalCategory.lift f.val g.val

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] {X W : Sheaf J A} (f : W ⟶ X) : (MonoidalCategoryStruct.whiskerLeft X f).val = MonoidalCategoryStruct.whiskerLeft X.val f.val

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] {X W : Sheaf J A} (f : W ⟶ X) : (MonoidalCategoryStruct.whiskerRight f X).val = MonoidalCategoryStruct.whiskerRight f.val X.val

noncomputable instance CategoryTheory.sheafToPresheafMonoidal {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : (sheafToPresheaf J A).Monoidal

The inclusion from sheaves to presheaves is monoidal with respect to the cartesian monoidal structures.

Equations

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

@[simp]

theorem CategoryTheory.sheafToPresheaf_ε {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : Functor.LaxMonoidal.ε (sheafToPresheaf J A) = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit (Functor Cᵒᵖ A))

@[simp]

theorem CategoryTheory.sheafToPresheaf_η {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : Functor.OplaxMonoidal.η (sheafToPresheaf J A) = CategoryStruct.id ((sheafToPresheaf J A).obj (MonoidalCategoryStruct.tensorUnit (Sheaf J A)))

@[simp]

theorem CategoryTheory.sheafToPresheaf_μ {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] {J : GrothendieckTopology C} [CartesianMonoidalCategory A] (X Y : Sheaf J A) : Functor.LaxMonoidal.μ (sheafToPresheaf J A) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((sheafToPresheaf J A).obj X) ((sheafToPresheaf J A).obj Y))

@[simp]

theorem CategoryTheory.sheafToPresheaf_δ {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] {J : GrothendieckTopology C} [CartesianMonoidalCategory A] (X Y : Sheaf J A) : Functor.OplaxMonoidal.δ (sheafToPresheaf J A) X Y = CategoryStruct.id ((sheafToPresheaf J A).obj (MonoidalCategoryStruct.tensorObj X Y))