Documentation Verification Report

Widesubcategory

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

Statistics

Metric	Count
Definitions `IsStableUnderComonoid`, `instComonObjWideSubcategoryOfIsStableUnderComonoidObj`, `instCopyDiscardCategoryWideSubcategoryOfIsStableUnderComonoid`	3
Theorems `comul_mem`, `counit_mem`, `comul_hom`, `counit_hom`, `instIsCommComonObjWideSubcategoryOfObj`	5
Total	8

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
`IsStableUnderComonoid` 📖	CompData	1 math math: `instIsStableUnderComonoidSFinKerStochHom`
`instComonObjWideSubcategoryOfIsStableUnderComonoidObj` 📖	CompOp	3 math math: `counit_hom`, `comul_hom`, `instIsCommComonObjWideSubcategoryOfObj`
`instCopyDiscardCategoryWideSubcategoryOfIsStableUnderComonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comul_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `CategoryTheory.WideSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.WideSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.WideSubcategory.instMonoidalCategory` `CategoryTheory.ComonObj.comul` `IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal` `instComonObjWideSubcategoryOfIsStableUnderComonoidObj`	—	`IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal`
`counit_hom` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `CategoryTheory.WideSubcategory.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.WideSubcategory.category` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.WideSubcategory.instMonoidalCategory` `CategoryTheory.ComonObj.counit` `IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal` `instComonObjWideSubcategoryOfIsStableUnderComonoidObj`	—	`IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal`
`instIsCommComonObjWideSubcategoryOfObj` 📖	mathematical	—	`CategoryTheory.IsCommComonObj` `CategoryTheory.WideSubcategory` `IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal` `IsStableUnderBraiding.toIsMonoidalStable` `CategoryTheory.WideSubcategory.category` `CategoryTheory.WideSubcategory.instMonoidalCategory` `CategoryTheory.WideSubcategory.instBraidedCategory` `instComonObjWideSubcategoryOfIsStableUnderComonoidObj`	—	`IsMonoidal.toIsMultiplicative` `IsMonoidalStable.toIsMonoidal` `IsStableUnderBraiding.toIsMonoidalStable` `CategoryTheory.WideSubcategory.hom_ext` `CategoryTheory.IsCommComonObj.comul_comm`

CategoryTheory.MorphismProperty.IsStableUnderComonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comul_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.comul`	—	—
`counit_mem` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.counit`	—	—

---

← Back to Index