CartesianMonoidal

📁 Source: Mathlib/CategoryTheory/Sites/CartesianMonoidal.lean

Statistics

Metric	Count
Definitions cartesianMonoidalCategory, sheafToPresheafMonoidal	2
Theorems cartesianMonoidalCategoryFst_val, cartesianMonoidalCategoryLift_val, cartesianMonoidalCategorySnd_val, cartesianMonoidalCategoryWhiskerLeft_val, cartesianMonoidalCategoryWhiskerRight_val, tensorProd_isSheaf, tensorUnit_isSheaf, sheafToPresheaf_δ, sheafToPresheaf_ε, sheafToPresheaf_η, sheafToPresheaf_μ	11
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
sheafToPresheafMonoidal 📖	CompOp	4 math math: sheafToPresheaf_μ, sheafToPresheaf_δ, sheafToPresheaf_η, sheafToPresheaf_ε

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sheafToPresheaf_δ 📖	mathematical	—	Functor.OplaxMonoidal.δ Sheaf Sheaf.instCategorySheaf SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Sheaf.cartesianMonoidalCategory Functor Opposite Category.opposite Functor.category Functor.cartesianMonoidalCategory sheafToPresheaf Functor.Monoidal.toOplaxMonoidal sheafToPresheafMonoidal CategoryStruct.id Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct	—	—
sheafToPresheaf_ε 📖	mathematical	—	Functor.LaxMonoidal.ε Sheaf Sheaf.instCategorySheaf SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Sheaf.cartesianMonoidalCategory Functor Opposite Category.opposite Functor.category Functor.cartesianMonoidalCategory sheafToPresheaf Functor.Monoidal.toLaxMonoidal sheafToPresheafMonoidal CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
sheafToPresheaf_η 📖	mathematical	—	Functor.OplaxMonoidal.η Sheaf Sheaf.instCategorySheaf SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Sheaf.cartesianMonoidalCategory Functor Opposite Category.opposite Functor.category Functor.cartesianMonoidalCategory sheafToPresheaf Functor.Monoidal.toOplaxMonoidal sheafToPresheafMonoidal CategoryStruct.id Category.toCategoryStruct Functor.obj MonoidalCategoryStruct.tensorUnit MonoidalCategory.toMonoidalCategoryStruct	—	—
sheafToPresheaf_μ 📖	mathematical	—	Functor.LaxMonoidal.μ Sheaf Sheaf.instCategorySheaf SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Sheaf.cartesianMonoidalCategory Functor Opposite Category.opposite Functor.category Functor.cartesianMonoidalCategory sheafToPresheaf Functor.Monoidal.toLaxMonoidal sheafToPresheafMonoidal CategoryStruct.id Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Functor.obj	—	—

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
cartesianMonoidalCategory 📖	CompOp	9 math math: cartesianMonoidalCategoryLift_val, CategoryTheory.sheafToPresheaf_μ, cartesianMonoidalCategorySnd_val, CategoryTheory.sheafToPresheaf_δ, cartesianMonoidalCategoryWhiskerRight_val, CategoryTheory.sheafToPresheaf_η, cartesianMonoidalCategoryFst_val, CategoryTheory.sheafToPresheaf_ε, cartesianMonoidalCategoryWhiskerLeft_val

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cartesianMonoidalCategoryFst_val 📖	mathematical	—	Hom.val CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.fst CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.cartesianMonoidalCategory val	—	—
cartesianMonoidalCategoryLift_val 📖	mathematical	—	Hom.val CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.cartesianMonoidalCategory val	—	—
cartesianMonoidalCategorySnd_val 📖	mathematical	—	Hom.val CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.SemiCartesianMonoidalCategory.snd CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.cartesianMonoidalCategory val	—	—
cartesianMonoidalCategoryWhiskerLeft_val 📖	mathematical	—	Hom.val CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.cartesianMonoidalCategory val	—	—
cartesianMonoidalCategoryWhiskerRight_val 📖	mathematical	—	Hom.val CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Sheaf instCategorySheaf CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory cartesianMonoidalCategory CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Functor.cartesianMonoidalCategory val	—	—
tensorProd_isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.cartesianMonoidalCategory val	—	isSheaf_of_isLimit CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype
tensorUnit_isSheaf 📖	mathematical	—	CategoryTheory.Presheaf.IsSheaf CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory CategoryTheory.Functor.cartesianMonoidalCategory	—	isSheaf_of_isLimit CategoryTheory.Limits.hasLimitsOfShape_discrete CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts Finite.of_fintype

---

← Back to Index