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₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.ChosenFiniteProducts A] (X Y : CategoryTheory.Sheaf J A) : CategoryTheory.Presheaf.IsSheaf J (CategoryTheory.MonoidalCategory.tensorObj X.val Y.val)

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

noncomputable instance CategoryTheory.Sheaf.chosenFiniteProducts {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.ChosenFiniteProducts A] : CategoryTheory.ChosenFiniteProducts (CategoryTheory.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₁} [CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [CategoryTheory.Category.{v₂, u₂} A] (J : CategoryTheory.GrothendieckTopology C) [CategoryTheory.ChosenFiniteProducts A] {X✝ Y✝ : Cᵒᵖ} (x✝ : X✝ ⟶ Y✝) : CategoryTheory.ChosenFiniteProducts.terminal.cone.pt.val.map x✝ = CategoryTheory.CategoryStruct.id (𝟙_ A)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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