Documentation Verification Report

Widesubcategory

📁 Source: Mathlib/CategoryTheory/Widesubcategory.lean

Statistics

Metric	Count
Definitions `InducedWideCategory`, `hom`, `category`, `hasCoeToSort`, `WideSubcategory`, `category`, `obj`, `isoMk`, `wideInducedFunctor`, `wideSubcategoryInclusion`	10
Theorems `ext`, `ext_iff`, `property`, `category_comp_hom`, `category_id_hom`, `faithful`, `comp_def`, `ext`, `ext_iff`, `hom_ext`, `hom_ext_iff`, `id_def`, `isoMk_hom_hom`, `isoMk_inv_hom`, `wideInducedFunctor_map`, `wideInducedFunctor_obj`, `faithful`, `map`, `obj`	19
Total	29

CategoryTheory

Definitions

Name	Category	Theorems
`InducedWideCategory` 📖	CompOp	5 math math: `InducedWideCategory.faithful`, `InducedWideCategory.category_id_hom`, `InducedWideCategory.category_comp_hom`, `wideInducedFunctor_obj`, `wideInducedFunctor_map`
`WideSubcategory` 📖	CompData	21 math math: `WideSubcategory.hom_ext_iff`, `wideSubcategoryInclusion.obj`, `WideSubcategory.rightUnitor_def`, `WideSubcategory.id_def`, `wideSubcategory.faithful`, `WideSubcategory.associator_def`, `WideSubcategory.comp_def`, `WideSubcategory.whiskerLeft_hom`, `WideSubcategory.tensorHom_hom`, `WideSubcategory.tensorμ_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `MorphismProperty.counit_hom`, `isoMk_inv_hom`, `MorphismProperty.comul_hom`, `wideSubcategoryInclusion.map`, `WideSubcategory.tensorUnit_obj`, `WideSubcategory.leftUnitor_def`, `WideSubcategory.tensorObj_obj`, `WideSubcategory.whiskerRight_hom`, `MorphismProperty.instIsCommComonObjWideSubcategoryOfObj`, `isoMk_hom_hom`
`isoMk` 📖	CompOp	5 math math: `WideSubcategory.rightUnitor_def`, `WideSubcategory.associator_def`, `isoMk_inv_hom`, `WideSubcategory.leftUnitor_def`, `isoMk_hom_hom`
`wideInducedFunctor` 📖	CompOp	3 math math: `InducedWideCategory.faithful`, `wideInducedFunctor_obj`, `wideInducedFunctor_map`
`wideSubcategoryInclusion` 📖	CompOp	3 math math: `wideSubcategoryInclusion.obj`, `wideSubcategory.faithful`, `wideSubcategoryInclusion.map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isoMk_hom_hom` 📖	mathematical	`WideSubcategory.obj` `Iso.hom` `Iso.inv`	`InducedWideCategory.Hom.hom` `WideSubcategory` `WideSubcategory.obj` `Iso.hom` `WideSubcategory.category` `isoMk`	—	—
`isoMk_inv_hom` 📖	mathematical	`WideSubcategory.obj` `Iso.hom` `Iso.inv`	`InducedWideCategory.Hom.hom` `WideSubcategory` `WideSubcategory.obj` `Iso.inv` `WideSubcategory.category` `isoMk`	—	—
`wideInducedFunctor_map` 📖	mathematical	—	`Functor.map` `InducedWideCategory` `InducedWideCategory.category` `wideInducedFunctor` `InducedWideCategory.Hom.hom`	—	—
`wideInducedFunctor_obj` 📖	mathematical	—	`Functor.obj` `InducedWideCategory` `InducedWideCategory.category` `wideInducedFunctor`	—	—

CategoryTheory.InducedWideCategory

Definitions

Name	Category	Theorems
`category` 📖	CompOp	5 math math: `faithful`, `category_id_hom`, `category_comp_hom`, `CategoryTheory.wideInducedFunctor_obj`, `CategoryTheory.wideInducedFunctor_map`
`hasCoeToSort` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`category_comp_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.InducedWideCategory` `CategoryTheory.Category.toCategoryStruct` `category`	—	—
`category_id_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.InducedWideCategory` `CategoryTheory.Category.toCategoryStruct` `category`	—	—
`faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.InducedWideCategory` `category` `CategoryTheory.wideInducedFunctor`	—	—

CategoryTheory.InducedWideCategory.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	18 math math: `CategoryTheory.WideSubcategory.hom_ext_iff`, `CategoryTheory.WideSubcategory.id_def`, `property`, `CategoryTheory.WideSubcategory.comp_def`, `ext_iff`, `CategoryTheory.WideSubcategory.whiskerLeft_hom`, `CategoryTheory.WideSubcategory.tensorHom_hom`, `CategoryTheory.InducedWideCategory.category_id_hom`, `CategoryTheory.WideSubcategory.tensorμ_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `CategoryTheory.MorphismProperty.counit_hom`, `CategoryTheory.isoMk_inv_hom`, `CategoryTheory.MorphismProperty.comul_hom`, `CategoryTheory.wideSubcategoryInclusion.map`, `CategoryTheory.InducedWideCategory.category_comp_hom`, `CategoryTheory.WideSubcategory.whiskerRight_hom`, `CategoryTheory.wideInducedFunctor_map`, `CategoryTheory.isoMk_hom_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom`	—	—	—
`ext_iff` 📖	mathematical	—	`hom`	—	`ext`
`property` 📖	mathematical	—	`hom`	—	—

CategoryTheory.WideSubcategory

Definitions

Name	Category	Theorems
`category` 📖	CompOp	19 math math: `CategoryTheory.wideSubcategoryInclusion.obj`, `rightUnitor_def`, `id_def`, `CategoryTheory.wideSubcategory.faithful`, `associator_def`, `comp_def`, `whiskerLeft_hom`, `tensorHom_hom`, `tensorμ_hom`, `CategoryTheory.MorphismProperty.counit_hom`, `CategoryTheory.isoMk_inv_hom`, `CategoryTheory.MorphismProperty.comul_hom`, `CategoryTheory.wideSubcategoryInclusion.map`, `tensorUnit_obj`, `leftUnitor_def`, `tensorObj_obj`, `whiskerRight_hom`, `CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj`, `CategoryTheory.isoMk_hom_hom`
`obj` 📖	CompOp	20 math math: `hom_ext_iff`, `CategoryTheory.wideSubcategoryInclusion.obj`, `rightUnitor_def`, `id_def`, `associator_def`, `comp_def`, `whiskerLeft_hom`, `tensorHom_hom`, `tensorμ_hom`, `instIsMarkovKernelCarrierObjSFinKerStochHomHomHomWideSubcategory`, `CategoryTheory.MorphismProperty.counit_hom`, `CategoryTheory.isoMk_inv_hom`, `CategoryTheory.MorphismProperty.comul_hom`, `CategoryTheory.wideSubcategoryInclusion.map`, `tensorUnit_obj`, `leftUnitor_def`, `ext_iff`, `tensorObj_obj`, `whiskerRight_hom`, `CategoryTheory.isoMk_hom_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_def` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `category`	—	—
`ext` 📖	—	`obj`	—	—	—
`ext_iff` 📖	mathematical	—	`obj`	—	`ext`
`hom_ext` 📖	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj`	—	—	`CategoryTheory.InducedWideCategory.Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj`	—	`hom_ext`
`id_def` 📖	mathematical	—	`CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory` `obj` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `category`	—	—

CategoryTheory.wideSubcategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`faithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `CategoryTheory.WideSubcategory` `CategoryTheory.WideSubcategory.category` `CategoryTheory.wideSubcategoryInclusion`	—	—

CategoryTheory.wideSubcategoryInclusion

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.WideSubcategory` `CategoryTheory.WideSubcategory.category` `CategoryTheory.wideSubcategoryInclusion` `CategoryTheory.InducedWideCategory.Hom.hom` `CategoryTheory.WideSubcategory.obj`	—	—
`obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.WideSubcategory` `CategoryTheory.WideSubcategory.category` `CategoryTheory.wideSubcategoryInclusion` `CategoryTheory.WideSubcategory.obj`	—	—

---

← Back to Index