Documentation Verification Report

Comon_

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean

Statistics

Metric	Count
Definitions `cartesianComon`, `comonEquiv`, `isoCartesianComon`	3
Theorems `comonEquiv_counitIso`, `comonEquiv_functor`, `comonEquiv_inverse`, `comonEquiv_unitIso`, `comul_eq_lift`, `counit_eq_toUnit`, `isoCartesianComon_hom_hom`, `isoCartesianComon_inv_hom`	8
Total	11

CategoryTheory

Definitions

Name	Category	Theorems
`cartesianComon` 📖	CompOp	5 math math: `comonEquiv_unitIso`, `isoCartesianComon_hom_hom`, `isoCartesianComon_inv_hom`, `comonEquiv_inverse`, `comonEquiv_counitIso`
`comonEquiv` 📖	CompOp	4 math math: `comonEquiv_unitIso`, `comonEquiv_functor`, `comonEquiv_inverse`, `comonEquiv_counitIso`
`isoCartesianComon` 📖	CompOp	3 math math: `comonEquiv_unitIso`, `isoCartesianComon_hom_hom`, `isoCartesianComon_inv_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comonEquiv_counitIso` 📖	mathematical	—	`Equivalence.counitIso` `Comon` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Comon.instCategory` `comonEquiv` `NatIso.ofComponents` `Functor.comp` `cartesianComon` `Comon.forget` `Functor.id` `Iso.refl` `Functor.obj`	—	—
`comonEquiv_functor` 📖	mathematical	—	`Equivalence.functor` `Comon` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Comon.instCategory` `comonEquiv` `Comon.forget`	—	—
`comonEquiv_inverse` 📖	mathematical	—	`Equivalence.inverse` `Comon` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Comon.instCategory` `comonEquiv` `cartesianComon`	—	—
`comonEquiv_unitIso` 📖	mathematical	—	`Equivalence.unitIso` `Comon` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Comon.instCategory` `comonEquiv` `NatIso.ofComponents` `Functor.id` `Functor.comp` `Comon.forget` `cartesianComon` `isoCartesianComon`	—	—
`comul_eq_lift` 📖	mathematical	—	`ComonObj.comul` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `CartesianMonoidalCategory.lift` `CategoryStruct.id` `Category.toCategoryStruct`	—	`CartesianMonoidalCategory.hom_ext` `CartesianMonoidalCategory.lift_fst` `counit_eq_toUnit` `Category.assoc` `CartesianMonoidalCategory.whiskerLeft_fst` `CartesianMonoidalCategory.rightUnitor_inv_fst` `eq_whisker` `ComonObj.comul_counit` `CartesianMonoidalCategory.lift_snd` `CartesianMonoidalCategory.whiskerRight_snd` `CartesianMonoidalCategory.leftUnitor_inv_snd` `ComonObj.counit_comul`
`counit_eq_toUnit` 📖	mathematical	—	`ComonObj.counit` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `SemiCartesianMonoidalCategory.toUnit`	—	`SemiCartesianMonoidalCategory.toUnit_unique`
`isoCartesianComon_hom_hom` 📖	mathematical	—	`Comon.Hom.hom` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Functor.obj` `Comon` `Comon.instCategory` `cartesianComon` `Comon.X` `Iso.hom` `isoCartesianComon` `CategoryStruct.id` `Category.toCategoryStruct`	—	—
`isoCartesianComon_inv_hom` 📖	mathematical	—	`Comon.Hom.hom` `SemiCartesianMonoidalCategory.toMonoidalCategory` `CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `Functor.obj` `Comon` `Comon.instCategory` `cartesianComon` `Comon.X` `Iso.inv` `isoCartesianComon` `CategoryStruct.id` `Category.toCategoryStruct`	—	—

---

← Back to Index