Coherence

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

Statistics

Metric	Count
Definitions NormalMonoidalObject, fullNormalize, fullNormalizeIso, inclusion, inclusionObj, instGroupoid, inverseAux, normalize, normalize', normalizeIso, normalizeIsoApp, normalizeIsoApp', normalizeIsoAux, normalizeMapAux, normalizeObj, normalizeObj', tensorFunc	17
Theorems inclusion_map, inclusion_obj, instSubsingletonHomCompDiscreteNormalMonoidalObject, normalizeIsoApp_eq, normalizeIsoApp_tensor, normalizeIsoApp_unitor, normalizeIsoAux_hom_app, normalizeIsoAux_inv_app, normalizeObj_congr, normalizeObj_tensor, normalizeObj_unitor, normalize_naturality, subsingleton_hom, tensorFunc_map_app, tensorFunc_obj_map	15
Total	32

CategoryTheory.FreeMonoidalCategory

Definitions

Name	Category	Theorems
NormalMonoidalObject 📖	CompData	11 math math: inclusion_obj, normalizeIsoAux_inv_app, normalize_naturality, tensorFunc_map_app, normalizeIsoApp_eq, inclusion_map, normalizeIsoApp_unitor, instSubsingletonHomCompDiscreteNormalMonoidalObject, normalizeIsoAux_hom_app, normalizeIsoApp_tensor, tensorFunc_obj_map
fullNormalize 📖	CompOp	—
fullNormalizeIso 📖	CompOp	—
inclusion 📖	CompOp	7 math math: inclusion_obj, normalize_naturality, tensorFunc_map_app, inclusion_map, normalizeIsoApp_unitor, normalizeIsoApp_tensor, tensorFunc_obj_map
inclusionObj 📖	CompOp	4 math math: inclusion_obj, normalizeIsoAux_inv_app, normalize_naturality, normalizeIsoAux_hom_app
instGroupoid 📖	CompOp	—
inverseAux 📖	CompOp	—
normalize 📖	CompOp	—
normalize' 📖	CompOp	3 math math: normalizeIsoAux_inv_app, normalizeIsoAux_hom_app, normalizeIsoApp_tensor
normalizeIso 📖	CompOp	—
normalizeIsoApp 📖	CompOp	5 math math: normalizeIsoAux_inv_app, normalizeIsoApp_eq, normalizeIsoApp_unitor, normalizeIsoAux_hom_app, normalizeIsoApp_tensor
normalizeIsoApp' 📖	CompOp	2 math math: normalize_naturality, normalizeIsoApp_eq
normalizeIsoAux 📖	CompOp	2 math math: normalizeIsoAux_inv_app, normalizeIsoAux_hom_app
normalizeMapAux 📖	CompOp	—
normalizeObj 📖	CompOp	5 math math: normalizeObj_tensor, normalizeObj_congr, normalize_naturality, normalizeObj_unitor, normalizeIsoApp_tensor
normalizeObj' 📖	CompOp	2 math math: normalizeIsoAux_inv_app, normalizeIsoAux_hom_app
tensorFunc 📖	CompOp	5 math math: normalizeIsoAux_inv_app, tensorFunc_map_app, normalizeIsoAux_hom_app, normalizeIsoApp_tensor, tensorFunc_obj_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inclusion_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory inclusion CategoryTheory.eqToHom CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Discrete.ext CategoryTheory.Discrete.eq_of_hom	—	—
inclusion_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory inclusion inclusionObj CategoryTheory.Discrete.as	—	—
instSubsingletonHomCompDiscreteNormalMonoidalObject 📖	mathematical	—	Quiver.Hom CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory	—	CategoryTheory.Discrete.instSubsingletonDiscreteHom
normalizeIsoApp_eq 📖	mathematical	—	normalizeIsoApp normalizeIsoApp' CategoryTheory.Discrete.as NormalMonoidalObject	—	normalizeIsoApp.eq_3 normalizeIsoApp'.eq_3
normalizeIsoApp_tensor 📖	mathematical	—	normalizeIsoApp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.Iso.trans CategoryTheory.Functor.obj CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory inclusion CategoryTheory.Discrete.as CategoryTheory.Functor CategoryTheory.Functor.category normalize' normalizeObj CategoryTheory.Iso.symm CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.whiskerRightIso tensorFunc	—	—
normalizeIsoApp_unitor 📖	mathematical	—	normalizeIsoApp CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.Functor.obj CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory inclusion CategoryTheory.Discrete.as	—	—
normalizeIsoAux_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorFunc normalize' CategoryTheory.Iso.hom normalizeIsoAux CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory inclusionObj CategoryTheory.Discrete.as normalizeObj' normalizeIsoApp	—	—
normalizeIsoAux_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category normalize' tensorFunc CategoryTheory.Iso.inv normalizeIsoAux CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory inclusionObj CategoryTheory.Discrete.as normalizeObj' normalizeIsoApp	—	—
normalizeObj_congr 📖	mathematical	—	normalizeObj	—	—
normalizeObj_tensor 📖	mathematical	—	normalizeObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
normalizeObj_unitor 📖	mathematical	—	normalizeObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory	—	—
normalize_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.FreeMonoidalCategory CategoryTheory.Category.toCategoryStruct categoryFreeMonoidalCategory CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory inclusionObj normalizeObj CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.hom normalizeIsoApp' CategoryTheory.Functor.obj CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory inclusion CategoryTheory.Functor.map CategoryTheory.eqToHom CategoryTheory.Discrete.ext normalizeObj_congr	—	Hom.inductionOn CategoryTheory.Discrete.ext normalizeObj_congr CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.Discrete.functor_map_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc CategoryTheory.MonoidalCategory.whiskerRightIso_trans CategoryTheory.Iso.trans_assoc CategoryTheory.MonoidalCategory.pentagon_inv_assoc CategoryTheory.MonoidalCategory.triangle_assoc_comp_right_assoc CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Iso.inv_hom_id CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Discrete.eq_of_hom CategoryTheory.MonoidalCategory.whiskerLeft_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.eqToHom_trans CategoryTheory.MonoidalCategory.associator_inv_naturality_right_assoc CategoryTheory.MonoidalCategory.whisker_exchange_assoc CategoryTheory.MonoidalCategory.associator_inv_naturality_middle_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc CategoryTheory.dcongr_arg CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.eqToHom_whiskerRight
subsingleton_hom 📖	mathematical	—	Quiver.IsThin CategoryTheory.FreeMonoidalCategory CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct categoryFreeMonoidalCategory	—	instSubsingletonHomCompDiscreteNormalMonoidalObject CategoryTheory.NatIso.naturality_2
tensorFunc_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorFunc CategoryTheory.Functor.map CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory inclusion CategoryTheory.Discrete.as	—	—
tensorFunc_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Discrete NormalMonoidalObject CategoryTheory.Pi.instCategoryComp CategoryTheory.discreteCategory CategoryTheory.FreeMonoidalCategory categoryFreeMonoidalCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category tensorFunc CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonoidalCategory inclusion	—	CategoryTheory.Discrete.functor_map_id CategoryTheory.MonoidalCategory.id_whiskerRight

---

← Back to Index