Documentation Verification Report

Monoidal

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

Statistics

Metric	Count
Definitions `functorEnrichedHomCoyonedaObjEquiv`, `braidedCategory`, `instBraidedFunctorOppositePresheafToSheaf`, `instMonoidalFunctorOppositePresheafToSheaf`, `monoidalCategory`, `symmetricCategory`	6
Theorems `monoidal`, `transport_isMonoidal`, `whiskerLeft`, `whiskerRight`, `functorEnrichedHomCoyonedaObjEquiv_naturality`, `isSheaf_functorEnrichedHom`	6
Total	12

CategoryTheory.GrothendieckTopology.W

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monoidal` 📖	mathematical	`CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf` `CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom`	`CategoryTheory.MorphismProperty.IsMonoidal` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.GrothendieckTopology.W` `CategoryTheory.Monoidal.functorCategoryMonoidal`	—	`CategoryTheory.ObjectProperty.instIsMultiplicativeIsLocal` `whiskerLeft` `whiskerRight`
`transport_isMonoidal` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMonoidal` `CategoryTheory.Functor` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.Functor.category` `CategoryTheory.GrothendieckTopology.W` `CategoryTheory.Monoidal.functorCategoryMonoidal`	—	`CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft` `CategoryTheory.MorphismProperty.instIsMonoidalInverseImageOfMonoidalOfRespectsIso` `CategoryTheory.ObjectProperty.instRespectsIsoIsLocal`
`whiskerLeft` 📖	mathematical	`CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf` `CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom` `CategoryTheory.GrothendieckTopology.W`	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft`	—	`CategoryTheory.Presheaf.isSheaf_functorEnrichedHom` `Function.Bijective.of_comp_iff'` `Equiv.bijective` `CategoryTheory.MonoidalClosed.curry_natural_left` `Function.Bijective.of_comp_iff`
`whiskerRight` 📖	mathematical	`CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf` `CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom` `CategoryTheory.GrothendieckTopology.W`	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight`	—	`CategoryTheory.MorphismProperty.arrow_mk_iso_iff` `CategoryTheory.ObjectProperty.instRespectsIsoIsLocal` `CategoryTheory.BraidedCategory.braiding_naturality_left` `whiskerLeft`

CategoryTheory.Presheaf

Definitions

Name	Category	Theorems
`functorEnrichedHomCoyonedaObjEquiv` 📖	CompOp	1 math math: `functorEnrichedHomCoyonedaObjEquiv_naturality`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`functorEnrichedHomCoyonedaObjEquiv_naturality` 📖	mathematical	`CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf`	`DFunLike.coe` `Equiv` `CategoryTheory.Functor.obj` `CategoryTheory.types` `CategoryTheory.Functor.comp` `CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.coyoneda` `Opposite.op` `CategoryTheory.presheafHom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Monoidal.functorCategoryMonoidalStruct` `CategoryTheory.Functor.const` `EquivLike.toFunLike` `Equiv.instEquivLike` `functorEnrichedHomCoyonedaObjEquiv` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `CategoryTheory.Enriched.FunctorCategory.precompEnrichedHom'` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Under.forget` `CategoryTheory.Under.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Iso.refl` `CategoryTheory.Functor.map`	—	`CategoryTheory.NatTrans.ext'` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.end_.lift_π` `CategoryTheory.eHomWhiskerRight_id` `CategoryTheory.eHomWhiskerLeft_id` `CategoryTheory.Category.comp_id`
`isSheaf_functorEnrichedHom` 📖	mathematical	`IsSheaf` `CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf`	`CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom`	—	`CategoryTheory.Presieve.isSheaf_iff_of_nat_equiv` `functorEnrichedHomCoyonedaObjEquiv_naturality` `CategoryTheory.isSheaf_iff_isSheaf_of_type` `IsSheaf.hom`

CategoryTheory.Sheaf

Definitions

Name	Category	Theorems
`braidedCategory` 📖	CompOp	—
`instBraidedFunctorOppositePresheafToSheaf` 📖	CompOp	—
`instMonoidalFunctorOppositePresheafToSheaf` 📖	CompOp	—
`monoidalCategory` 📖	CompOp	—
`symmetricCategory` 📖	CompOp	—

---

← Back to Index