Basic

📁 Source: Mathlib/CategoryTheory/Monoidal/Free/Basic.lean

Statistics

Metric	Count
Definitions FreeMonoidalCategory, categoryFreeMonoidalCategory, homMk, instMonoidalCategory, instMonoidalProject, project, projectMap, projectMapAux, projectObj, setoidHom, instInhabitedFreeMonoidalCategory, default	12
Theorems inductionOn, mk_comp, mk_id, mk_l_hom, mk_l_inv, mk_tensor, mk_whiskerLeft, mk_whiskerRight, mk_α_hom, mk_α_inv, mk_ρ_hom, mk_ρ_inv, tensor_eq_tensor, unit_eq_unit	14
Total	26

CategoryTheory

Definitions

Name	Category	Theorems
FreeMonoidalCategory 📖	CompData	25 math math: FreeMonoidalCategory.mk_ρ_hom, FreeMonoidalCategory.mk_id, FreeMonoidalCategory.inclusion_obj, FreeMonoidalCategory.normalizeIsoAux_inv_app, FreeMonoidalCategory.tensor_eq_tensor, FreeMonoidalCategory.normalizeObj_tensor, FreeMonoidalCategory.normalize_naturality, FreeMonoidalCategory.mk_whiskerRight, FreeMonoidalCategory.normalizeObj_unitor, FreeMonoidalCategory.mk_comp, FreeMonoidalCategory.mk_l_inv, FreeMonoidalCategory.tensorFunc_map_app, FreeMonoidalCategory.inclusion_map, FreeMonoidalCategory.mk_l_hom, FreeMonoidalCategory.mk_α_hom, FreeMonoidalCategory.normalizeIsoApp_unitor, FreeMonoidalCategory.mk_ρ_inv, FreeMonoidalCategory.subsingleton_hom, FreeMonoidalCategory.mk_whiskerLeft, FreeMonoidalCategory.normalizeIsoAux_hom_app, FreeMonoidalCategory.mk_α_inv, FreeMonoidalCategory.normalizeIsoApp_tensor, FreeMonoidalCategory.unit_eq_unit, FreeMonoidalCategory.mk_tensor, FreeMonoidalCategory.tensorFunc_obj_map
instInhabitedFreeMonoidalCategory 📖	CompOp	—

CategoryTheory.FreeMonoidalCategory

Definitions

Name	Category	Theorems
categoryFreeMonoidalCategory 📖	CompOp	25 math math: mk_ρ_hom, mk_id, inclusion_obj, normalizeIsoAux_inv_app, tensor_eq_tensor, normalizeObj_tensor, normalize_naturality, mk_whiskerRight, normalizeObj_unitor, mk_comp, mk_l_inv, tensorFunc_map_app, inclusion_map, mk_l_hom, mk_α_hom, normalizeIsoApp_unitor, mk_ρ_inv, subsingleton_hom, mk_whiskerLeft, normalizeIsoAux_hom_app, mk_α_inv, normalizeIsoApp_tensor, unit_eq_unit, mk_tensor, tensorFunc_obj_map
homMk 📖	CompOp	—
instMonoidalCategory 📖	CompOp	20 math math: mk_ρ_hom, normalizeIsoAux_inv_app, tensor_eq_tensor, normalizeObj_tensor, normalize_naturality, mk_whiskerRight, normalizeObj_unitor, mk_l_inv, tensorFunc_map_app, mk_l_hom, mk_α_hom, normalizeIsoApp_unitor, mk_ρ_inv, mk_whiskerLeft, normalizeIsoAux_hom_app, mk_α_inv, normalizeIsoApp_tensor, unit_eq_unit, mk_tensor, tensorFunc_obj_map
instMonoidalProject 📖	CompOp	—
project 📖	CompOp	—
projectMap 📖	CompOp	—
projectMapAux 📖	CompOp	—
projectObj 📖	CompOp	—
setoidHom 📖	CompOp	11 math math: mk_ρ_hom, mk_id, mk_whiskerRight, mk_comp, mk_l_inv, mk_l_hom, mk_α_hom, mk_ρ_inv, mk_whiskerLeft, mk_α_inv, mk_tensor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_comp 📖	mathematical	—	Hom setoidHom Hom.comp CategoryTheory.CategoryStruct.comp CategoryTheory.FreeMonoidalCategory CategoryTheory.Category.toCategoryStruct categoryFreeMonoidalCategory	—	—
mk_id 📖	mathematical	—	Hom setoidHom Hom.id CategoryTheory.CategoryStruct.id CategoryTheory.FreeMonoidalCategory CategoryTheory.Category.toCategoryStruct categoryFreeMonoidalCategory	—	—
mk_l_hom 📖	mathematical	—	Hom tensor unit setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit Hom.l_hom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
mk_l_inv 📖	mathematical	—	Hom tensor unit setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit Hom.l_inv CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
mk_tensor 📖	mathematical	—	Hom tensor setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Hom.tensor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
mk_whiskerLeft 📖	mathematical	—	Hom tensor setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Hom.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
mk_whiskerRight 📖	mathematical	—	Hom tensor setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Hom.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
mk_α_hom 📖	mathematical	—	Hom tensor setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Hom.α_hom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
mk_α_inv 📖	mathematical	—	Hom tensor setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory Hom.α_inv CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	—
mk_ρ_hom 📖	mathematical	—	Hom tensor unit setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit Hom.ρ_hom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
mk_ρ_inv 📖	mathematical	—	Hom tensor unit setoidHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorUnit Hom.ρ_inv CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
tensor_eq_tensor 📖	mathematical	—	tensor CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
unit_eq_unit 📖	mathematical	—	unit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—

CategoryTheory.FreeMonoidalCategory.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inductionOn 📖	—	CategoryTheory.CategoryStruct.id CategoryTheory.FreeMonoidalCategory CategoryTheory.Category.toCategoryStruct CategoryTheory.FreeMonoidalCategory.categoryFreeMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.FreeMonoidalCategory.instMonoidalCategory CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—	—

CategoryTheory.instInhabitedFreeMonoidalCategory

Definitions

Name	Category	Theorems
default 📖	CompOp	—

---

← Back to Index