Chosen finite products on sheaves

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

theorem CategoryTheory.Sheaf.tensorProd_isSheaf {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [ChosenFiniteProducts 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) [ChosenFiniteProducts A] : Presheaf.IsSheaf J (𝟙_ (Functor Cᵒᵖ A))

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

Any ChosenFiniteProducts on A induce a ChosenFiniteProducts structures on A-valued sheaves.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.chosenFiniteProducts_terminal_cone_pt_val_map {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [ChosenFiniteProducts A] {X✝ Y✝ : Cᵒᵖ} (x✝ : X✝ ⟶ Y✝) : ChosenFiniteProducts.terminal.cone.pt.val.map x✝ = CategoryStruct.id (𝟙_ A)

@[simp]

theorem CategoryTheory.Sheaf.chosenFiniteProducts_product_cone_pt_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [ChosenFiniteProducts A] (X Y : Sheaf J A) : (ChosenFiniteProducts.product X Y).cone.pt.val = MonoidalCategoryStruct.tensorObj X.val Y.val

@[simp]

theorem CategoryTheory.Sheaf.chosenFiniteProducts_terminal_cone_pt_val_obj {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [ChosenFiniteProducts A] (x✝ : Cᵒᵖ) : ChosenFiniteProducts.terminal.cone.pt.val.obj x✝ = 𝟙_ A

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Sheaf.chosenFiniteProducts_whiskerRight_val {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] (J : GrothendieckTopology C) [ChosenFiniteProducts 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) [ChosenFiniteProducts 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) [ChosenFiniteProducts A] : Functor.LaxMonoidal.ε (sheafToPresheaf J A) = CategoryStruct.id (𝟙_ (Functor Cᵒᵖ A))

@[simp]

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

@[simp]

theorem CategoryTheory.sheafToPresheaf_μ {C : Type u₁} [Category.{v₁, u₁} C] {A : Type u₂} [Category.{v₂, u₂} A] {J : GrothendieckTopology C} [ChosenFiniteProducts 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} [ChosenFiniteProducts A] (X Y : Sheaf J A) : Functor.OplaxMonoidal.δ (sheafToPresheaf J A) X Y = CategoryStruct.id ((sheafToPresheaf J A).obj (MonoidalCategoryStruct.tensorObj X Y))