IsMonoidalW

📁 Source: Mathlib/CategoryTheory/Sites/Point/IsMonoidalW.lean

Statistics

Metric	Count
Definitions	0
Theorems isMonoidal_W, instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints	2
Total	2

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonoidalFunctorOppositeWOfHasSheafComposeForgetOfHasEnoughPoints 📖	mathematical	Limits.HasProducts Limits.PreservesFilteredColimitsOfSize MonoidalCategory.tensorLeft MonoidalCategory.tensorRight	MorphismProperty.IsMonoidal Functor Opposite Category.opposite Functor.category GrothendieckTopology.W Monoidal.functorCategoryMonoidal	—	GrothendieckTopology.HasEnoughPoints.exists_objectProperty ObjectProperty.IsConservativeFamilyOfPoints.isMonoidal_W

CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMonoidal_W 📖	mathematical	CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints CategoryTheory.Limits.HasProducts CategoryTheory.Limits.PreservesFilteredColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.MorphismProperty.IsMonoidal CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.GrothendieckTopology.W CategoryTheory.Monoidal.functorCategoryMonoidal	—	CategoryTheory.MorphismProperty.IsMonoidal.mk' CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal W_iff CategoryTheory.Functor.Monoidal.map_tensor CategoryTheory.IsIso.comp_isIso CategoryTheory.Functor.Monoidal.instIsIsoδ CategoryTheory.MonoidalCategory.tensor_isIso CategoryTheory.Functor.Monoidal.instIsIsoμ

---

← Back to Index