Documentation Verification Report

Widesubcategory

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

Statistics

Metric	Count
Definitions `IsMonoidalStable`, `IsStableUnderAssociator`, `IsStableUnderBraiding`, `IsStableUnderUnitor`, `instBraidedCategory`, `instMonoidalCategory`, `instMonoidalCategoryStruct`, `instSymmetricCategory`	8
Theorems `toIsMonoidal`, `toIsStableUnderAssociator`, `toIsStableUnderUnitor`, `associator_hom_mem`, `associator_inv_mem`, `braiding_hom_mem`, `braiding_inv_mem`, `toIsMonoidalStable`, `leftUnitor_hom_mem`, `leftUnitor_inv_mem`, `rightUnitor_hom_mem`, `rightUnitor_inv_mem`, `associator_def`, `leftUnitor_def`, `rightUnitor_def`, `tensorHom_hom`, `tensorObj_obj`, `tensorUnit_obj`, `tensorμ_hom`, `whiskerLeft_hom`, `whiskerRight_hom`	21
Total	29

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsMonoidalStable` 📖	CompData	1 math math: `IsStableUnderBraiding.toIsMonoidalStable`
`IsStableUnderAssociator` 📖	CompData	1 math math: `IsMonoidalStable.toIsStableUnderAssociator`
`IsStableUnderBraiding` 📖	CompData	1 math math: `instIsStableUnderBraidingSFinKerStochHom`
`IsStableUnderUnitor` 📖	CompData	1 math math: `IsMonoidalStable.toIsStableUnderUnitor`

CategoryTheory.MorphismProperty.IsMonoidalStable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toIsMonoidal` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMonoidal`	—	—
`toIsStableUnderAssociator` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderAssociator`	—	—
`toIsStableUnderUnitor` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderUnitor`	—	—

CategoryTheory.MorphismProperty.IsStableUnderAssociator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`associator_inv_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—

CategoryTheory.MorphismProperty.IsStableUnderBraiding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`braiding_hom_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding`	—	—
`braiding_inv_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding`	—	—
`toIsMonoidalStable` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMonoidalStable`	—	—

CategoryTheory.MorphismProperty.IsStableUnderUnitor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`leftUnitor_hom_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`leftUnitor_inv_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`rightUnitor_hom_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`rightUnitor_inv_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—

CategoryTheory.WideSubcategory

Definitions

Name	Category	Theorems
`instBraidedCategory` 📖	CompOp	2 math math: `tensorμ_hom`, `CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj`
`instMonoidalCategory` 📖	CompOp	4 math math: `tensorμ_hom`, `CategoryTheory.MorphismProperty.counit_hom`, `CategoryTheory.MorphismProperty.comul_hom`, `CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj`
`instMonoidalCategoryStruct` 📖	CompOp	8 math math: `rightUnitor_def`, `associator_def`, `whiskerLeft_hom`, `tensorHom_hom`, `tensorUnit_obj`, `leftUnitor_def`, `tensorObj_obj`, `whiskerRight_hom`
`instSymmetricCategory` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct` `CategoryTheory.isoMk` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `obj`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct` `CategoryTheory.isoMk` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct` `CategoryTheory.isoMk` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`tensorHom_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`tensorObj_obj` 📖	mathematical	—	`obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`tensorUnit_obj` 📖	mathematical	—	`obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`tensorμ_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `CategoryTheory.MorphismProperty.IsStableUnderBraiding.toIsMonoidalStable` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.MonoidalCategory.tensorμ` `instBraidedCategory`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `CategoryTheory.MorphismProperty.IsStableUnderBraiding.toIsMonoidalStable`
`whiskerLeft_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`
`whiskerRight_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal` `category` `instMonoidalCategoryStruct`	—	`CategoryTheory.MorphismProperty.IsMonoidal.toIsMultiplicative` `CategoryTheory.MorphismProperty.IsMonoidalStable.toIsMonoidal`

---

← Back to Index