Monoidal category structure on categories of sheaves #
If A is a closed braided category with suitable limits,
and J is a Grothendieck topology with HasWeakSheafify J A,
then Sheaf J A can be equipped with a monoidal category
structure. This is not made an instance as in some cases
it may conflict with monoidal structure deduced from
chosen finite products.
TODO #
- show that the monoidal category structure on sheaves is closed,
and that the internal hom can be defined in such a way that the
underlying presheaf is the internal hom in the category of presheaves.
Note that a
MonoidalClosedinstance on sheaves can already be obtained abstractly using the material inCategoryTheory.Monoidal.Braided.Reflection.
noncomputable def
CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv
{C : Type u'}
[Category.{v', u'} C]
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
(M : A)
(F G : Functor Cᵒᵖ A)
[Enriched.FunctorCategory.HasFunctorEnrichedHom A F G]
(X : C)
:
((Enriched.FunctorCategory.functorEnrichedHom A F G).comp (coyoneda.obj (Opposite.op M))).obj (Opposite.op X) ≃ (presheafHom (MonoidalCategoryStruct.tensorObj F ((Functor.const Cᵒᵖ).obj M)) G).obj (Opposite.op X)
Relation between functorEnrichedHom and presheafHom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Presheaf.functorEnrichedHomCoyonedaObjEquiv_naturality
{C : Type u'}
[Category.{v', u'} C]
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
{M : A}
{F G : Functor Cᵒᵖ A}
{X Y : C}
(f : X ⟶ Y)
[Enriched.FunctorCategory.HasFunctorEnrichedHom A F G]
(y : ((Enriched.FunctorCategory.functorEnrichedHom A F G).comp (coyoneda.obj (Opposite.op M))).obj (Opposite.op Y))
:
(functorEnrichedHomCoyonedaObjEquiv M F G X)
(CategoryStruct.comp y
(Enriched.FunctorCategory.precompEnrichedHom' A (Under.map f.op)
(Iso.refl ((Under.map f.op).comp ((Under.forget (Opposite.op Y)).comp F)))
(Iso.refl ((Under.map f.op).comp ((Under.forget (Opposite.op Y)).comp G))))) = (presheafHom (MonoidalCategoryStruct.tensorObj F ((Functor.const Cᵒᵖ).obj M)) G).map f.op
((functorEnrichedHomCoyonedaObjEquiv M F G Y) y)
theorem
CategoryTheory.Presheaf.isSheaf_functorEnrichedHom
{C : Type u'}
[Category.{v', u'} C]
{J : GrothendieckTopology C}
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
(F G : Functor Cᵒᵖ A)
(hG : IsSheaf J G)
[Enriched.FunctorCategory.HasFunctorEnrichedHom A F G]
:
theorem
CategoryTheory.GrothendieckTopology.W.whiskerLeft
{C : Type u'}
[Category.{v', u'} C]
{J : GrothendieckTopology C}
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
{G₁ G₂ : Functor Cᵒᵖ A}
{g : G₁ ⟶ G₂}
(hg : J.W g)
(F : Functor Cᵒᵖ A)
:
J.W (MonoidalCategoryStruct.whiskerLeft F g)
theorem
CategoryTheory.GrothendieckTopology.W.whiskerRight
{C : Type u'}
[Category.{v', u'} C]
{J : GrothendieckTopology C}
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
[BraidedCategory A]
{F₁ F₂ : Functor Cᵒᵖ A}
{f : F₁ ⟶ F₂}
(hf : J.W f)
(G : Functor Cᵒᵖ A)
:
J.W (MonoidalCategoryStruct.whiskerRight f G)
instance
CategoryTheory.GrothendieckTopology.W.monoidal
{C : Type u'}
[Category.{v', u'} C]
{J : GrothendieckTopology C}
{A : Type u}
[Category.{v, u} A]
[MonoidalCategory A]
[MonoidalClosed A]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasFunctorEnrichedHom A F₁ F₂]
[∀ (F₁ F₂ : Functor Cᵒᵖ A), Enriched.FunctorCategory.HasEnrichedHom A F₁ F₂]
[BraidedCategory A]
:
J.W.IsMonoidal
noncomputable def
CategoryTheory.Sheaf.monoidalCategory
{C : Type u'}
[Category.{v', u'} C]
(J : GrothendieckTopology C)
(A : Type u)
[Category.{v, u} A]
[MonoidalCategory A]
[J.W.IsMonoidal]
[HasWeakSheafify J A]
:
MonoidalCategory (Sheaf J A)
The monoidal category structure on Sheaf J A that is obtained
by localization of the monoidal category structure on the category
of presheaves.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable instance
CategoryTheory.Sheaf.instMonoidalFunctorOppositePresheafToSheaf
{C : Type u'}
[Category.{v', u'} C]
(J : GrothendieckTopology C)
(A : Type u)
[Category.{v, u} A]
[MonoidalCategory A]
[J.W.IsMonoidal]
[HasWeakSheafify J A]
:
(presheafToSheaf J A).Monoidal
Equations
- One or more equations did not get rendered due to their size.