Documentation Verification Report

Mod_

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

Statistics

Metric	Count
Definitions `IsMod_Hom`, `ModObj`, `instTensorUnit`, `regular`, `smul`, `Mod_`, `hom`, `mk'`, `mk''`, `X`, `comap`, `comp`, `forget`, `homInhabited`, `id`, `instCategory`, `instInhabited`, `regular`, `scalarRestriction`, `Mod_Class`, `termγ`, `«termγ[_,_]»`, `«termγ[_]»`	23
Theorems `smul_hom`, `smul_hom_assoc`, `assoc_flip`, `ext`, `ext_iff`, `mul_smul`, `mul_smul'`, `mul_smul'_assoc`, `mul_smul_assoc`, `one_smul`, `one_smul'`, `one_smul'_assoc`, `one_smul_assoc`, `smul_def`, `smul_eq_mul`, `ext`, `ext_iff`, `isMod_Hom`, `mk''_hom`, `mk'_hom`, `assoc_flip`, `comap_map_hom`, `comap_obj_X`, `comap_obj_mod`, `comp_hom`, `comp_hom'`, `forget_map`, `forget_obj`, `hom_ext`, `hom_ext_iff`, `id_hom`, `id_hom'`, `regular_X`, `regular_mod_smul`, `scalarRestriction_hom`, `scalarRestriction_smul`, `instIsMod_HomComp`, `instIsMod_HomId`, `instIsMod_HomInvOfHom`	39
Total	62

CategoryTheory

Definitions

Name	Category	Theorems
`IsMod_Hom` 📖	CompData	5 math math: `Mod_.scalarRestriction_hom`, `instIsMod_HomComp`, `instIsMod_HomId`, `Mod_.Hom.isMod_Hom`, `instIsMod_HomInvOfHom`
`ModObj` 📖	CompData	—
`Mod_` 📖	CompData	7 math math: `Mod_.comap_obj_mod`, `Mod_.comap_map_hom`, `Mod_.comap_obj_X`, `Mod_.forget_obj`, `Mod_.comp_hom'`, `Mod_.forget_map`, `Mod_.id_hom'`
`Mod_Class` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsMod_HomComp` 📖	mathematical	—	`IsMod_Hom` `CategoryStruct.comp` `Category.toCategoryStruct`	—	`IsMod_Hom.smul_hom_assoc` `IsMod_Hom.smul_hom` `MonoidalCategory.MonoidalLeftAction.actionHomRight_comp` `Category.assoc`
`instIsMod_HomId` 📖	mathematical	—	`IsMod_Hom` `CategoryStruct.id` `Category.toCategoryStruct`	—	`Category.comp_id` `MonoidalCategory.MonoidalLeftAction.actionHomRight_id` `Category.id_comp`
`instIsMod_HomInvOfHom` 📖	mathematical	—	`IsMod_Hom` `Iso.inv`	—	`Category.assoc` `IsMod_Hom.smul_hom` `MonoidalCategory.MonoidalLeftAction.actionHomRight_inv_hom_assoc`

CategoryTheory.IsMod_Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smul_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.ModObj.smul` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`smul_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.ModObj.smul` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `smul_hom`

CategoryTheory.ModObj

Definitions

Name	Category	Theorems
`instTensorUnit` 📖	CompOp	1 math math: `smul_def`
`regular` 📖	CompOp	1 math math: `smul_eq_mul`
`smul` 📖	CompOp	18 math math: `one_smul_assoc`, `mul_smul_assoc`, `mul_smul'_assoc`, `CategoryTheory.IsMod_Hom.smul_hom`, `one_smul'_assoc`, `CategoryTheory.IsMod_Hom.smul_hom_assoc`, `smul_eq_mul`, `one_smul'`, `assoc_flip`, `one_smul`, `ext_iff`, `CategoryTheory.Mod_.regular_mod_smul`, `CategoryTheory.Mod_.scalarRestriction_smul`, `smul_def`, `CategoryTheory.Mod_.assoc_flip`, `mul_smul`, `mul_smul'`, `CategoryTheory.Mod_.trivialAction_mod_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_flip` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `smul` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul`	—	`mul_smul` `CategoryTheory.Iso.inv_hom_id_assoc`
`ext` 📖	—	`smul` `CategoryTheory.MonoidalCategory.selfLeftAction`	—	—	—
`ext_iff` 📖	mathematical	—	`smul` `CategoryTheory.MonoidalCategory.selfLeftAction`	—	`ext`
`mul_smul` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`mul_smul'`
`mul_smul'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`mul_smul'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mul_smul'`
`mul_smul_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `mul_smul`
`one_smul` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.one` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	`one_smul'`
`one_smul'` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.one` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`one_smul'_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.one` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `one_smul'`
`one_smul_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.one` `smul` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `one_smul`
`smul_def` 📖	mathematical	—	`smul` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonObj.instTensorUnit` `instTensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso`	—	—
`smul_eq_mul` 📖	mathematical	—	`smul` `CategoryTheory.MonoidalCategory.selfLeftAction` `regular` `CategoryTheory.MonObj.mul`	—	—

CategoryTheory.Mod_

Definitions

Name	Category	Theorems
`X` 📖	CompOp	12 math math: `comap_obj_mod`, `comap_map_hom`, `comap_obj_X`, `forget_obj`, `comp_hom'`, `Hom.isMod_Hom`, `trivialAction_X`, `assoc_flip`, `regular_X`, `id_hom`, `comp_hom`, `id_hom'`
`comap` 📖	CompOp	3 math math: `comap_obj_mod`, `comap_map_hom`, `comap_obj_X`
`comp` 📖	CompOp	1 math math: `comp_hom`
`forget` 📖	CompOp	2 math math: `forget_obj`, `forget_map`
`homInhabited` 📖	CompOp	—
`id` 📖	CompOp	1 math math: `id_hom`
`instCategory` 📖	CompOp	7 math math: `comap_obj_mod`, `comap_map_hom`, `comap_obj_X`, `forget_obj`, `comp_hom'`, `forget_map`, `id_hom'`
`instInhabited` 📖	CompOp	—
`regular` 📖	CompOp	2 math math: `regular_mod_smul`, `regular_X`
`scalarRestriction` 📖	CompOp	4 math math: `comap_obj_mod`, `comap_map_hom`, `scalarRestriction_hom`, `scalarRestriction_smul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc_flip` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `X` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.ModObj.smul` `mod` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `CategoryTheory.MonObj.mul`	—	`CategoryTheory.ModObj.mul_smul` `CategoryTheory.Iso.inv_hom_id_assoc`
`comap_map_hom` 📖	mathematical	—	`Hom.hom` `X` `scalarRestriction` `mod` `CategoryTheory.Functor.map` `CategoryTheory.Mod_` `instCategory` `comap`	—	—
`comap_obj_X` 📖	mathematical	—	`X` `CategoryTheory.Functor.obj` `CategoryTheory.Mod_` `instCategory` `comap`	—	—
`comap_obj_mod` 📖	mathematical	—	`mod` `CategoryTheory.Functor.obj` `CategoryTheory.Mod_` `instCategory` `comap` `scalarRestriction` `X`	—	—
`comp_hom` 📖	mathematical	—	`Hom.hom` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X`	—	—
`comp_hom'` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Mod_` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X`	—	—
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.Mod_` `instCategory` `forget` `Hom.hom`	—	—
`forget_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.Mod_` `instCategory` `forget` `X`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`id_hom` 📖	mathematical	—	`Hom.hom` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `X`	—	—
`id_hom'` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Mod_` `CategoryTheory.Category.toCategoryStruct` `instCategory` `X`	—	—
`regular_X` 📖	mathematical	—	`X` `CategoryTheory.MonoidalCategory.selfLeftAction` `regular`	—	—
`regular_mod_smul` 📖	mathematical	—	`CategoryTheory.ModObj.smul` `CategoryTheory.MonoidalCategory.selfLeftAction` `mod` `regular` `CategoryTheory.MonObj.mul`	—	—
`scalarRestriction_hom` 📖	mathematical	—	`CategoryTheory.IsMod_Hom` `scalarRestriction`	—	`CategoryTheory.Category.assoc` `CategoryTheory.IsMod_Hom.smul_hom` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.action_exchange_assoc`
`scalarRestriction_smul` 📖	mathematical	—	`CategoryTheory.ModObj.smul` `scalarRestriction` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft`	—	—

CategoryTheory.Mod_.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	11 math math: `CategoryTheory.Mod_.comap_map_hom`, `mk'_hom`, `CategoryTheory.Mod_.comp_hom'`, `isMod_Hom`, `CategoryTheory.Mod_.forget_map`, `mk''_hom`, `ext_iff`, `CategoryTheory.Mod_.id_hom`, `CategoryTheory.Mod_.hom_ext_iff`, `CategoryTheory.Mod_.comp_hom`, `CategoryTheory.Mod_.id_hom'`
`mk'` 📖	CompOp	1 math math: `mk'_hom`
`mk''` 📖	CompOp	1 math math: `mk''_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom`	—	—	—
`ext_iff` 📖	mathematical	—	`hom`	—	`ext`
`isMod_Hom` 📖	mathematical	—	`CategoryTheory.IsMod_Hom` `CategoryTheory.Mod_.X` `CategoryTheory.Mod_.mod` `hom`	—	—
`mk''_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ModObj.smul` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	`hom` `mk''`	—	—
`mk'_hom` 📖	mathematical	`Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Mod_.X` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ModObj.smul` `CategoryTheory.Mod_.mod` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	`hom` `mk'`	—	—

CategoryTheory.MonObj

Definitions

Name	Category	Theorems
`termγ` 📖	CompOp	—
`«termγ[_,_]»` 📖	CompOp	—
`«termγ[_]»` 📖	CompOp	—

---

← Back to Index