Monoidal structure on sheaves using enough points #
Let (C, J) be a site with a conservative family of points.
If A is a suitable monoidal category, we show that
the class of morphisms J.W : MorphismProperty (Cᵒᵖ ⥤ A)
is stable under tensor products, which allows to
check the assumptions of Sheaf.monoidalCategory in the
file Mathlib/CategoryTheory/Sites/Monoidal.lean,
i.e. this can be used in order to construct the monoidal
category structure on Sheaf J A.
theorem
CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W
{C : Type u}
[Category.{v, u} C]
[LocallySmall.{w, v, u} C]
{J : GrothendieckTopology C}
{P : ObjectProperty J.Point}
(hP : P.IsConservativeFamilyOfPoints)
(A : Type u')
[Category.{v', u'} A]
[MonoidalCategory A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasProducts A]
{FC : A → A → Type u_1}
{CC : A → Type w}
[(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory A FC]
[HasWeakSheafify J A]
[(forget A).ReflectsIsomorphisms]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)]
[∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)]
[∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)]
[J.HasSheafCompose (forget A)]
:
J.W.IsMonoidal
instance
CategoryTheory.instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints
{C : Type u}
[Category.{v, u} C]
[LocallySmall.{w, v, u} C]
{J : GrothendieckTopology C}
(A : Type u')
[Category.{v', u'} A]
[MonoidalCategory A]
[Limits.HasColimitsOfSize.{w, w, v', u'} A]
[Limits.HasProducts A]
{FC : A → A → Type u_1}
{CC : A → Type w}
[(X Y : A) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory A FC]
[HasWeakSheafify J A]
[(forget A).ReflectsIsomorphisms]
[Limits.PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)]
[∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorLeft X)]
[∀ (X : A), Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (MonoidalCategory.tensorRight X)]
[J.HasSheafCompose (forget A)]
[J.HasEnoughPoints]
:
J.W.IsMonoidal