Documentation Verification Report

CommComon_

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

Statistics

Metric	Count
Definitions `CommComon`, `X`, `comon`, `forget₂Comon`, `instCategory`, `instInhabited`, `toComon`, `trivial`	8
Theorems `comm`, `comp_hom`, `forget₂Comon_map`, `forget₂Comon_obj_X`, `forget₂Comon_obj_comon`, `hom_ext`, `hom_ext_iff`, `id_hom`, `instCommComonObjUnit`, `toComon_X`, `trivial_X`, `trivial_comon_comul`, `trivial_comon_counit`	13
Total	21

CategoryTheory

Definitions

Name	Category	Theorems
`CommComon` 📖	CompData	6 math math: `CommComon.comp_hom`, `CommComon.forget₂Comon_map`, `CommComon.hom_ext_iff`, `CommComon.id_hom`, `CommComon.forget₂Comon_obj_comon`, `CommComon.forget₂Comon_obj_X`

CategoryTheory.CommComon

Definitions

Name	Category	Theorems
`X` 📖	CompOp	5 math math: `comm`, `toComon_X`, `trivial_X`, `id_hom`, `forget₂Comon_obj_X`
`comon` 📖	CompOp	4 math math: `trivial_comon_comul`, `comm`, `trivial_comon_counit`, `forget₂Comon_obj_comon`
`forget₂Comon` 📖	CompOp	3 math math: `forget₂Comon_map`, `forget₂Comon_obj_comon`, `forget₂Comon_obj_X`
`instCategory` 📖	CompOp	5 math math: `comp_hom`, `forget₂Comon_map`, `id_hom`, `forget₂Comon_obj_comon`, `forget₂Comon_obj_X`
`instInhabited` 📖	CompOp	—
`toComon` 📖	CompOp	5 math math: `comp_hom`, `forget₂Comon_map`, `toComon_X`, `hom_ext_iff`, `id_hom`
`trivial` 📖	CompOp	3 math math: `trivial_comon_comul`, `trivial_comon_counit`, `trivial_X`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	—	`CategoryTheory.IsCommComonObj` `X` `comon`	—	—
`comp_hom` 📖	mathematical	—	`CategoryTheory.Comon.Hom.hom` `toComon` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.CommComon` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.Comon.X`	—	—
`forget₂Comon_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.CommComon` `instCategory` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory` `forget₂Comon` `CategoryTheory.InducedCategory.Hom.hom` `toComon`	—	—
`forget₂Comon_obj_X` 📖	mathematical	—	`CategoryTheory.Comon.X` `CategoryTheory.Functor.obj` `CategoryTheory.CommComon` `instCategory` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory` `forget₂Comon` `X`	—	—
`forget₂Comon_obj_comon` 📖	mathematical	—	`CategoryTheory.Comon.comon` `CategoryTheory.Functor.obj` `CategoryTheory.CommComon` `instCategory` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory` `forget₂Comon` `comon`	—	—
`hom_ext` 📖	—	`CategoryTheory.Comon.Hom.hom` `toComon` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.CommComon` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory`	—	—	`CategoryTheory.InducedCategory.hom_ext` `CategoryTheory.Comon.Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.Comon.Hom.hom` `toComon` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.CommComon` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory`	—	`hom_ext`
`id_hom` 📖	mathematical	—	`CategoryTheory.Comon.Hom.hom` `toComon` `CategoryTheory.InducedCategory.Hom.hom` `CategoryTheory.CommComon` `CategoryTheory.Comon` `CategoryTheory.Comon.instCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X`	—	—
`instCommComonObjUnit` 📖	mathematical	—	`CategoryTheory.IsCommComonObj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.ComonObj.instTensorUnit`	—	`CategoryTheory.braiding_tensorUnit_right` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id`
`toComon_X` 📖	mathematical	—	`CategoryTheory.Comon.X` `toComon` `X`	—	—
`trivial_X` 📖	mathematical	—	`X` `trivial` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`trivial_comon_comul` 📖	mathematical	—	`CategoryTheory.ComonObj.comul` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `comon` `trivial` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`trivial_comon_counit` 📖	mathematical	—	`CategoryTheory.ComonObj.counit` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `comon` `trivial` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—

---

← Back to Index