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.obj Y.obj)

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))

instance CategoryTheory.Sheaf.instIsMonoidalFunctorOppositeIsSheaf {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [CartesianMonoidalCategory A] : ObjectProperty.IsMonoidal (Presheaf.IsSheaf J)

@[simp]

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

@[simp]

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

@[deprecated CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom (since := "2026-03-05")]

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) : (SemiCartesianMonoidalCategory.fst X Y).hom = SemiCartesianMonoidalCategory.fst X.obj Y.obj

Alias of CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom.

@[deprecated CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom (since := "2026-03-05")]

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) : (SemiCartesianMonoidalCategory.snd X Y).hom = SemiCartesianMonoidalCategory.snd X.obj Y.obj

Alias of CategoryTheory.Sheaf.cartesianMonoidalCategorySnd_hom.

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom {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).hom = CartesianMonoidalCategory.lift f.hom g.hom

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom {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).hom = MonoidalCategoryStruct.whiskerLeft X.obj f.hom

@[simp]

theorem CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom {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).hom = MonoidalCategoryStruct.whiskerRight f.hom X.obj

@[deprecated CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom (since := "2026-03-05")]

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).hom = CartesianMonoidalCategory.lift f.hom g.hom

Alias of CategoryTheory.Sheaf.cartesianMonoidalCategoryLift_hom.

@[deprecated CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom (since := "2026-03-05")]

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).hom = MonoidalCategoryStruct.whiskerLeft X.obj f.hom

Alias of CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerLeft_hom.

@[deprecated CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom (since := "2026-03-05")]

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).hom = MonoidalCategoryStruct.whiskerRight f.hom X.obj

Alias of CategoryTheory.Sheaf.cartesianMonoidalCategoryWhiskerRight_hom.

@[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))