Documentation Verification Report

CartesianMonoidal

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

Statistics

Metric	Count
Definitions	0
Theorems `cartesianMonoidalCategoryFst_hom`, `cartesianMonoidalCategoryFst_val`, `cartesianMonoidalCategoryLift_hom`, `cartesianMonoidalCategoryLift_val`, `cartesianMonoidalCategorySnd_hom`, `cartesianMonoidalCategorySnd_val`, `cartesianMonoidalCategoryWhiskerLeft_hom`, `cartesianMonoidalCategoryWhiskerLeft_val`, `cartesianMonoidalCategoryWhiskerRight_hom`, `cartesianMonoidalCategoryWhiskerRight_val`, `instIsMonoidalFunctorOppositeIsSheaf`, `tensorProd_isSheaf`, `tensorUnit_isSheaf`, `sheafToPresheaf_δ`, `sheafToPresheaf_ε`, `sheafToPresheaf_η`, `sheafToPresheaf_μ`	17
Total	17

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sheafToPresheaf_δ` 📖	mathematical	—	`Functor.OplaxMonoidal.δ` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.fullMonoidalSubcategory` `Monoidal.functorCategoryMonoidal` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Sheaf.instIsMonoidalFunctorOppositeIsSheaf` `sheafToPresheaf` `Functor.Monoidal.toOplaxMonoidal` `ObjectProperty.monoidalι` `CategoryStruct.id` `Category.toCategoryStruct` `Functor.obj` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct`	—	`Sheaf.instIsMonoidalFunctorOppositeIsSheaf`
`sheafToPresheaf_ε` 📖	mathematical	—	`Functor.LaxMonoidal.ε` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.fullMonoidalSubcategory` `Monoidal.functorCategoryMonoidal` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Sheaf.instIsMonoidalFunctorOppositeIsSheaf` `sheafToPresheaf` `Functor.Monoidal.toLaxMonoidal` `ObjectProperty.monoidalι` `CategoryStruct.id` `Category.toCategoryStruct` `MonoidalCategoryStruct.tensorUnit` `MonoidalCategory.toMonoidalCategoryStruct`	—	`Sheaf.instIsMonoidalFunctorOppositeIsSheaf`
`sheafToPresheaf_η` 📖	mathematical	—	`Functor.OplaxMonoidal.η` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.fullMonoidalSubcategory` `Monoidal.functorCategoryMonoidal` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Sheaf.instIsMonoidalFunctorOppositeIsSheaf` `sheafToPresheaf` `Functor.Monoidal.toOplaxMonoidal` `ObjectProperty.monoidalι` `CategoryStruct.id` `Category.toCategoryStruct` `Functor.obj` `MonoidalCategoryStruct.tensorUnit` `MonoidalCategory.toMonoidalCategoryStruct`	—	`Sheaf.instIsMonoidalFunctorOppositeIsSheaf`
`sheafToPresheaf_μ` 📖	mathematical	—	`Functor.LaxMonoidal.μ` `Sheaf` `ObjectProperty.FullSubcategory.category` `Functor` `Opposite` `Category.opposite` `Functor.category` `Presheaf.IsSheaf` `ObjectProperty.fullMonoidalSubcategory` `Monoidal.functorCategoryMonoidal` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Sheaf.instIsMonoidalFunctorOppositeIsSheaf` `sheafToPresheaf` `Functor.Monoidal.toLaxMonoidal` `ObjectProperty.monoidalι` `CategoryStruct.id` `Category.toCategoryStruct` `MonoidalCategoryStruct.tensorObj` `MonoidalCategory.toMonoidalCategoryStruct` `Functor.obj`	—	`Sheaf.instIsMonoidalFunctorOppositeIsSheaf`

CategoryTheory.Sheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cartesianMonoidalCategoryFst_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.SemiCartesianMonoidalCategory.fst`	—	`instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype`
`cartesianMonoidalCategoryFst_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.SemiCartesianMonoidalCategory.fst`	—	`cartesianMonoidalCategoryFst_hom`
`cartesianMonoidalCategoryLift_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.CartesianMonoidalCategory.lift`	—	`instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype`
`cartesianMonoidalCategoryLift_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.CartesianMonoidalCategory.lift`	—	`cartesianMonoidalCategoryLift_hom`
`cartesianMonoidalCategorySnd_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.SemiCartesianMonoidalCategory.snd`	—	`instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype`
`cartesianMonoidalCategorySnd_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.fullSubcategory` `CategoryTheory.Functor.cartesianMonoidalCategory` `instIsClosedUnderLimitsOfShapeFunctorOppositeIsSheaf` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype` `Fintype.instPEmpty` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.SemiCartesianMonoidalCategory.snd`	—	`cartesianMonoidalCategorySnd_hom`
`cartesianMonoidalCategoryWhiskerLeft_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instIsMonoidalFunctorOppositeIsSheaf` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	`instIsMonoidalFunctorOppositeIsSheaf`
`cartesianMonoidalCategoryWhiskerLeft_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instIsMonoidalFunctorOppositeIsSheaf` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	`cartesianMonoidalCategoryWhiskerLeft_hom`
`cartesianMonoidalCategoryWhiskerRight_hom` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instIsMonoidalFunctorOppositeIsSheaf` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	`instIsMonoidalFunctorOppositeIsSheaf`
`cartesianMonoidalCategoryWhiskerRight_val` 📖	mathematical	—	`CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.ObjectProperty.FullSubcategory` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.ObjectProperty.FullSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Sheaf` `CategoryTheory.ObjectProperty.FullSubcategory.category` `CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instIsMonoidalFunctorOppositeIsSheaf` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct`	—	`cartesianMonoidalCategoryWhiskerRight_hom`
`instIsMonoidalFunctorOppositeIsSheaf` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsMonoidal` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidal` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.Presheaf.IsSheaf`	—	`tensorUnit_isSheaf` `tensorProd_isSheaf`
`tensorProd_isSheaf` 📖	mathematical	—	`CategoryTheory.Presheaf.IsSheaf` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CategoryTheory.ObjectProperty.FullSubcategory.obj`	—	`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.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory`	—	`isSheaf_of_isLimit` `CategoryTheory.Limits.hasLimitsOfShape_discrete` `CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts` `Finite.of_fintype`

---

← Back to Index