Bimon_

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

Statistics

Metric	Count
Definitions Bimon, equivMonComon, equivMonComonCounitIsoApp, equivMonComonCounitIsoAppX, equivMonComonCounitIsoAppXAux, equivMonComonUnitIsoApp, equivMonComonUnitIsoAppX, equivMonComonUnitIsoAppXAux, equivMon_Comon_, equivMon_Comon_CounitIsoApp, equivMon_Comon_CounitIsoAppX, equivMon_Comon_CounitIsoAppXAux, equivMon_Comon_UnitIsoApp, equivMon_Comon_UnitIsoAppX, equivMon_Comon_UnitIsoAppXAux, forget, instBimonObjXXMon, instCategory, mk', mk'X, ofMonComon, ofMonComonObj, ofMonComonObjX, ofMon_Comon_, ofMon_Comon_Obj, ofMon_Comon_ObjX, toComon, toComon_, toMon, toMonComon, toMonComonObj, toMon_, toMon_Comon_, toMon_Comon_obj, toTrivial, trivial, trivialTo, BimonObj, toComonObj, toMonObj, Bimon_, Bimon_Class, IsBimonHom, IsBimon_Hom	44
Theorems BimonObjAux_comul, BimonObjAux_counit, Bimon_ClassAux_comul, Bimon_ClassAux_counit, mul_def, comp_hom', compatibility, compatibility_assoc, equivMonComonCounitIsoAppXAux_hom, equivMonComonCounitIsoAppXAux_inv, equivMonComonCounitIsoAppX_hom_hom, equivMonComonCounitIsoAppX_inv_hom, equivMonComonCounitIsoApp_hom_hom_hom, equivMonComonCounitIsoApp_inv_hom_hom, equivMonComonUnitIsoAppXAux_hom, equivMonComonUnitIsoAppXAux_inv, equivMonComonUnitIsoAppX_hom_hom, equivMonComonUnitIsoAppX_inv_hom, equivMonComonUnitIsoApp_hom_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, ext, ext_iff, id_hom', instIsComonHomHomEquivMonComonCounitIsoAppXAux, instIsComonHomMonHomEquivMonComonUnitIsoAppX, instIsMonHomComonHomEquivMonComonCounitIsoAppX, instIsMonHomHomEquivMonComonUnitIsoAppXAux, mk'X_X, mk'_X, mul_counit, mul_counit_assoc, ofMonComonObjX_X, ofMonComonObjX_mul, ofMonComonObjX_one, ofMonComonObj_X, ofMonComonObj_comon_comul_hom, ofMonComonObj_comon_counit_hom, ofMonComon_map_hom, ofMonComon_obj, ofMonComon_toMonComon_obj_comul, ofMonComon_toMonComon_obj_counit, ofMon_Comon_ObjX_mul, ofMon_Comon_ObjX_one, ofMon_Comon_toMon_Comon_obj_comul, ofMon_Comon_toMon_Comon_obj_counit, one_comul, one_comul_assoc, toComon_forget, toComon_map_hom, toComon_obj_X, toComon_obj_comon_comul, toComon_obj_comon_counit, toMonComonObj_X, toMonComonObj_mon_mul_hom, toMonComonObj_mon_one_hom, toMonComon_map_hom, toMonComon_obj, toMonComon_ofMonComon_obj_mul, toMonComon_ofMonComon_obj_one, toMon_Comon_ofMon_Comon_obj_mul, toMon_Comon_ofMon_Comon_obj_one, toMon_forget, toTrivial_hom, trivialTo_hom, trivial_X_X, trivial_X_mon_mul, trivial_X_mon_one, trivial_comon_comul_hom, trivial_comon_counit_hom, mul_comul, mul_comul_assoc, mul_counit, mul_counit_assoc, one_comul, one_comul_assoc, one_counit, one_counit_assoc, toIsComonHom, toIsMonHom	79
Total	123

CategoryTheory

Definitions

Name	Category	Theorems
Bimon 📖	CompOp	43 math math: Bimon.toMonComonObj_mon_mul_hom, Bimon.Bimon_ClassAux_comul, Bimon.equivMonComonUnitIsoAppX_hom_hom, Bimon.toMonComon_ofMonComon_obj_one, Bimon.toMon_forget, Bimon.equivMonComonUnitIsoAppXAux_hom, Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, Bimon.equivMonComonUnitIsoApp_hom_hom_hom, Bimon.toComon_obj_comon_counit, Bimon.toComon_map_hom, Bimon.toComon_obj_X, Bimon.equivMonComonCounitIsoAppXAux_inv, Bimon.toComon_forget, Bimon.Bimon_ClassAux_counit, Bimon.equivMonComonUnitIsoAppX_inv_hom, Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, Bimon.BimonObjAux_counit, Bimon.ofMonComon_toMonComon_obj_counit, Bimon.ofMon_Comon_toMon_Comon_obj_comul, Bimon.equivMonComonUnitIsoAppXAux_inv, Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, Bimon.equivMonComonCounitIsoAppX_hom_hom, Bimon.equivMonComonUnitIsoApp_inv_hom_hom, Bimon.ofMon_Comon_toMon_Comon_obj_counit, Bimon.id_hom', Bimon.ofMonComon_map_hom, Bimon.ofMonComon_obj, Bimon.toMonComon_obj, Bimon.equivMonComonCounitIsoAppX_inv_hom, Bimon.toMonComonObj_mon_one_hom, Bimon.toMonComon_ofMonComon_obj_mul, Bimon.BimonObjAux_comul, Bimon.equivMonComonCounitIsoApp_hom_hom_hom, Bimon.ofMonComon_toMonComon_obj_comul, Bimon.toMonComon_map_hom, Bimon.equivMonComonCounitIsoAppXAux_hom, Bimon.toMon_Comon_ofMon_Comon_obj_mul, Bimon.comp_hom', Bimon.toMonComonObj_X, Bimon.toMon_Comon_ofMon_Comon_obj_one, Bimon.equivMonComonCounitIsoApp_inv_hom_hom, Bimon.toComon_obj_comon_comul
BimonObj 📖	CompData	—
Bimon_ 📖	CompOp	—
Bimon_Class 📖	CompOp	—
IsBimonHom 📖	CompData	—
IsBimon_Hom 📖	MathDef	—

CategoryTheory.Bimon

Definitions

Name	Category	Theorems
equivMonComon 📖	CompOp	—
equivMonComonCounitIsoApp 📖	CompOp	2 math math: equivMonComonCounitIsoApp_hom_hom_hom, equivMonComonCounitIsoApp_inv_hom_hom
equivMonComonCounitIsoAppX 📖	CompOp	3 math math: instIsMonHomComonHomEquivMonComonCounitIsoAppX, equivMonComonCounitIsoAppX_hom_hom, equivMonComonCounitIsoAppX_inv_hom
equivMonComonCounitIsoAppXAux 📖	CompOp	3 math math: instIsComonHomHomEquivMonComonCounitIsoAppXAux, equivMonComonCounitIsoAppXAux_inv, equivMonComonCounitIsoAppXAux_hom
equivMonComonUnitIsoApp 📖	CompOp	2 math math: equivMonComonUnitIsoApp_hom_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom
equivMonComonUnitIsoAppX 📖	CompOp	3 math math: equivMonComonUnitIsoAppX_hom_hom, equivMonComonUnitIsoAppX_inv_hom, instIsComonHomMonHomEquivMonComonUnitIsoAppX
equivMonComonUnitIsoAppXAux 📖	CompOp	3 math math: equivMonComonUnitIsoAppXAux_hom, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux
equivMon_Comon_ 📖	CompOp	—
equivMon_Comon_CounitIsoApp 📖	CompOp	—
equivMon_Comon_CounitIsoAppX 📖	CompOp	—
equivMon_Comon_CounitIsoAppXAux 📖	CompOp	—
equivMon_Comon_UnitIsoApp 📖	CompOp	—
equivMon_Comon_UnitIsoAppX 📖	CompOp	—
equivMon_Comon_UnitIsoAppXAux 📖	CompOp	—
forget 📖	CompOp	2 math math: toMon_forget, toComon_forget
instBimonObjXXMon 📖	CompOp	—
instCategory 📖	CompOp	43 math math: toMonComonObj_mon_mul_hom, Bimon_ClassAux_comul, equivMonComonUnitIsoAppX_hom_hom, toMonComon_ofMonComon_obj_one, toMon_forget, equivMonComonUnitIsoAppXAux_hom, instIsMonHomComonHomEquivMonComonCounitIsoAppX, instIsComonHomHomEquivMonComonCounitIsoAppXAux, equivMonComonUnitIsoApp_hom_hom_hom, toComon_obj_comon_counit, toComon_map_hom, toComon_obj_X, equivMonComonCounitIsoAppXAux_inv, toComon_forget, Bimon_ClassAux_counit, equivMonComonUnitIsoAppX_inv_hom, instIsComonHomMonHomEquivMonComonUnitIsoAppX, BimonObjAux_counit, ofMonComon_toMonComon_obj_counit, ofMon_Comon_toMon_Comon_obj_comul, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, ofMon_Comon_toMon_Comon_obj_counit, id_hom', ofMonComon_map_hom, ofMonComon_obj, toMonComon_obj, equivMonComonCounitIsoAppX_inv_hom, toMonComonObj_mon_one_hom, toMonComon_ofMonComon_obj_mul, BimonObjAux_comul, equivMonComonCounitIsoApp_hom_hom_hom, ofMonComon_toMonComon_obj_comul, toMonComon_map_hom, equivMonComonCounitIsoAppXAux_hom, toMon_Comon_ofMon_Comon_obj_mul, comp_hom', toMonComonObj_X, toMon_Comon_ofMon_Comon_obj_one, equivMonComonCounitIsoApp_inv_hom_hom, toComon_obj_comon_comul
mk' 📖	CompOp	1 math math: mk'_X
mk'X 📖	CompOp	2 math math: mk'X_X, mk'_X
ofMonComon 📖	CompOp	26 math math: equivMonComonUnitIsoAppX_hom_hom, toMonComon_ofMonComon_obj_one, equivMonComonUnitIsoAppXAux_hom, instIsMonHomComonHomEquivMonComonCounitIsoAppX, instIsComonHomHomEquivMonComonCounitIsoAppXAux, equivMonComonUnitIsoApp_hom_hom_hom, equivMonComonCounitIsoAppXAux_inv, equivMonComonUnitIsoAppX_inv_hom, instIsComonHomMonHomEquivMonComonUnitIsoAppX, ofMonComon_toMonComon_obj_counit, ofMon_Comon_toMon_Comon_obj_comul, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, ofMon_Comon_toMon_Comon_obj_counit, ofMonComon_map_hom, ofMonComon_obj, equivMonComonCounitIsoAppX_inv_hom, toMonComon_ofMonComon_obj_mul, equivMonComonCounitIsoApp_hom_hom_hom, ofMonComon_toMonComon_obj_comul, equivMonComonCounitIsoAppXAux_hom, toMon_Comon_ofMon_Comon_obj_mul, toMon_Comon_ofMon_Comon_obj_one, equivMonComonCounitIsoApp_inv_hom_hom
ofMonComonObj 📖	CompOp	5 math math: ofMonComonObj_comon_comul_hom, ofMonComonObj_comon_counit_hom, ofMonComon_map_hom, ofMonComon_obj, ofMonComonObj_X
ofMonComonObjX 📖	CompOp	8 math math: ofMonComonObjX_mul, ofMonComonObj_comon_comul_hom, ofMon_Comon_ObjX_one, ofMon_Comon_ObjX_mul, ofMonComonObj_comon_counit_hom, ofMonComonObjX_one, ofMonComonObjX_X, ofMonComonObj_X
ofMon_Comon_ 📖	CompOp	—
ofMon_Comon_Obj 📖	CompOp	—
ofMon_Comon_ObjX 📖	CompOp	—
toComon 📖	CompOp	13 math math: toMonComonObj_mon_mul_hom, Bimon_ClassAux_comul, toComon_obj_comon_counit, toComon_map_hom, toComon_obj_X, toComon_forget, Bimon_ClassAux_counit, BimonObjAux_counit, toMonComonObj_mon_one_hom, BimonObjAux_comul, toMonComon_map_hom, toMonComonObj_X, toComon_obj_comon_comul
toComon_ 📖	CompOp	—
toMon 📖	CompOp	1 math math: toMon_forget
toMonComon 📖	CompOp	26 math math: equivMonComonUnitIsoAppX_hom_hom, toMonComon_ofMonComon_obj_one, equivMonComonUnitIsoAppXAux_hom, instIsMonHomComonHomEquivMonComonCounitIsoAppX, instIsComonHomHomEquivMonComonCounitIsoAppXAux, equivMonComonUnitIsoApp_hom_hom_hom, equivMonComonCounitIsoAppXAux_inv, equivMonComonUnitIsoAppX_inv_hom, instIsComonHomMonHomEquivMonComonUnitIsoAppX, ofMonComon_toMonComon_obj_counit, ofMon_Comon_toMon_Comon_obj_comul, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, ofMon_Comon_toMon_Comon_obj_counit, toMonComon_obj, equivMonComonCounitIsoAppX_inv_hom, toMonComon_ofMonComon_obj_mul, equivMonComonCounitIsoApp_hom_hom_hom, ofMonComon_toMonComon_obj_comul, toMonComon_map_hom, equivMonComonCounitIsoAppXAux_hom, toMon_Comon_ofMon_Comon_obj_mul, toMon_Comon_ofMon_Comon_obj_one, equivMonComonCounitIsoApp_inv_hom_hom
toMonComonObj 📖	CompOp	5 math math: toMonComonObj_mon_mul_hom, toMonComon_obj, toMonComonObj_mon_one_hom, toMonComon_map_hom, toMonComonObj_X
toMon_ 📖	CompOp	—
toMon_Comon_ 📖	CompOp	—
toMon_Comon_obj 📖	CompOp	—
toTrivial 📖	CompOp	1 math math: toTrivial_hom
trivial 📖	CompOp	7 math math: trivial_comon_counit_hom, toTrivial_hom, trivial_X_X, trivial_comon_comul_hom, trivialTo_hom, trivial_X_mon_mul, trivial_X_mon_one
trivialTo 📖	CompOp	1 math math: trivialTo_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
BimonObjAux_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Comon.comon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Category.comp_id
BimonObjAux_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Comon.comon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Category.comp_id
Bimon_ClassAux_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Comon.comon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	BimonObjAux_comul
Bimon_ClassAux_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Comon.comon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	BimonObjAux_counit
comp_hom' 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.CategoryStruct.comp CategoryTheory.Bimon CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comon.X	—	—
compatibility 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj	—	CategoryTheory.BimonObj.mul_comul CategoryTheory.Category.assoc
compatibility_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' compatibility
equivMonComonCounitIsoAppXAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon equivMonComonCounitIsoAppXAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonCounitIsoAppXAux_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon equivMonComonCounitIsoAppXAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonCounitIsoAppX_hom_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Iso.hom equivMonComonCounitIsoAppX CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comon.X	—	—
equivMonComonCounitIsoAppX_inv_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Iso.inv equivMonComonCounitIsoAppX CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comon.X	—	—
equivMonComonCounitIsoApp_hom_hom_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon.mon CategoryTheory.Iso.hom equivMonComonCounitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comon.X	—	—
equivMonComonCounitIsoApp_inv_hom_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Mon.Hom.hom CategoryTheory.Mon.mon CategoryTheory.Iso.inv equivMonComonCounitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Comon.X	—	—
equivMonComonUnitIsoAppXAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon equivMonComonUnitIsoAppXAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonUnitIsoAppXAux_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon equivMonComonUnitIsoAppXAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonUnitIsoAppX_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Mon.mon CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Iso.hom equivMonComonUnitIsoAppX CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonUnitIsoAppX_inv_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.Iso.inv equivMonComonUnitIsoAppX CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
equivMonComonUnitIsoApp_hom_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Comon.Hom.hom CategoryTheory.Iso.hom equivMonComonUnitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
equivMonComonUnitIsoApp_inv_hom_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Comon.Hom.hom CategoryTheory.Iso.inv equivMonComonUnitIsoApp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
ext 📖	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Comon.Hom.hom	—	—	CategoryTheory.Comon.Hom.ext CategoryTheory.Mon.Hom.ext
ext_iff 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Comon.Hom.hom	—	ext
id_hom' 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.CategoryStruct.id CategoryTheory.Bimon CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Comon.X	—	—
instIsComonHomHomEquivMonComonCounitIsoAppXAux 📖	mathematical	—	CategoryTheory.IsComonHom CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Comon.comon CategoryTheory.Iso.hom equivMonComonCounitIsoAppXAux	—	CategoryTheory.IsComonHom.hom_counit CategoryTheory.instIsComonHomId CategoryTheory.Category.comp_id CategoryTheory.IsComonHom.hom_comul CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight
instIsComonHomMonHomEquivMonComonUnitIsoAppX 📖	mathematical	—	CategoryTheory.IsComonHom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Comon.comon CategoryTheory.Iso.hom equivMonComonUnitIsoAppX	—	CategoryTheory.Mon.Hom.ext' toComon_obj_comon_counit CategoryTheory.Category.id_comp toComon_obj_comon_comul CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id
instIsMonHomComonHomEquivMonComonCounitIsoAppX 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Mon.mon CategoryTheory.Iso.hom equivMonComonCounitIsoAppX	—	CategoryTheory.Comon.ext CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight
instIsMonHomHomEquivMonComonUnitIsoAppXAux 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.Iso.hom equivMonComonUnitIsoAppXAux	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight
mk'X_X 📖	mathematical	—	CategoryTheory.Mon.X mk'X	—	—
mk'_X 📖	mathematical	—	CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal mk' mk'X	—	—
mul_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.ComonObj.counit CategoryTheory.BimonObj.toComonObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.BimonObj.mul_counit
mul_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit CategoryTheory.BimonObj.toComonObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_counit
ofMonComonObjX_X 📖	mathematical	—	CategoryTheory.Mon.X ofMonComonObjX CategoryTheory.Comon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal	—	—
ofMonComonObjX_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X ofMonComonObjX CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.CategoryStruct.id CategoryTheory.Comon.Hom.hom	—	—
ofMonComonObjX_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X ofMonComonObjX CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.CategoryStruct.id CategoryTheory.Comon.Hom.hom	—	—
ofMonComonObj_X 📖	mathematical	—	CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal ofMonComonObj ofMonComonObjX	—	—
ofMonComonObj_comon_comul_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom ofMonComonObjX CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal CategoryTheory.ComonObj.comul CategoryTheory.Comon.comon ofMonComonObj CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal	—	—
ofMonComonObj_comon_counit_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom ofMonComonObjX CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal CategoryTheory.ComonObj.counit CategoryTheory.Comon.comon ofMonComonObj CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal	—	—
ofMonComon_map_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal ofMonComonObj CategoryTheory.Functor.map CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Bimon instCategory ofMonComon CategoryTheory.Functor.mapMon CategoryTheory.Comon.forget CategoryTheory.Functor.Monoidal.toLaxMonoidal CategoryTheory.Comon.instMonoidalForget	—	—
ofMonComon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Mon.instCategory CategoryTheory.Bimon instCategory ofMonComon ofMonComonObj	—	—
ofMonComon_toMonComon_obj_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Comon.comon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
ofMonComon_toMonComon_obj_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Comon.comon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
ofMon_Comon_ObjX_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X ofMonComonObjX CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.CategoryStruct.id CategoryTheory.Comon.Hom.hom	—	ofMonComonObjX_mul
ofMon_Comon_ObjX_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X ofMonComonObjX CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.CategoryStruct.id CategoryTheory.Comon.Hom.hom	—	ofMonComonObjX_one
ofMon_Comon_toMon_Comon_obj_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Comon.comon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	ofMonComon_toMonComon_obj_comul
ofMon_Comon_toMon_Comon_obj_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Comon.X CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory ofMonComon toMonComon CategoryTheory.Comon.comon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	ofMonComon_toMonComon_obj_counit
one_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.one CategoryTheory.BimonObj.toMonObj CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.BimonObj.one_comul
one_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one CategoryTheory.BimonObj.toMonObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ComonObj.comul CategoryTheory.BimonObj.toComonObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_comul
toComon_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Comon.forget forget	—	—
toComon_map_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.forget CategoryTheory.Comon.X CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj.instComonObj CategoryTheory.Comon.comon CategoryTheory.Functor.Monoidal.toOplaxMonoidal CategoryTheory.Mon.instMonoidalForget CategoryTheory.Functor.map CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Mon.Hom.hom	—	—
toComon_obj_X 📖	mathematical	—	CategoryTheory.Comon.X CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Mon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal	—	—
toComon_obj_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.forget CategoryTheory.Comon.X CategoryTheory.Mon.monMonoidal CategoryTheory.Comon.comon CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Category.comp_id
toComon_obj_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.forget CategoryTheory.Comon.X CategoryTheory.Mon.monMonoidal CategoryTheory.Comon.comon CategoryTheory.Bimon instCategory CategoryTheory.Comon CategoryTheory.Comon.instCategory toComon CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Category.comp_id
toMonComonObj_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComonObj CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory toComon	—	—
toMonComonObj_mon_mul_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory toComon CategoryTheory.MonObj.mul CategoryTheory.Mon.mon toMonComonObj CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal	—	—
toMonComonObj_mon_one_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Comon.monoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory toComon CategoryTheory.MonObj.one CategoryTheory.Mon.mon toMonComonObj CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal	—	—
toMonComon_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComonObj CategoryTheory.Functor.map CategoryTheory.Bimon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory toMonComon toComon	—	—
toMonComon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Mon CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal CategoryTheory.Mon.instCategory toMonComon toMonComonObj	—	—
toMonComon_ofMonComon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
toMonComon_ofMonComon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
toMon_Comon_ofMon_Comon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	toMonComon_ofMonComon_obj_mul
toMon_Comon_ofMon_Comon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal CategoryTheory.Functor.obj CategoryTheory.Bimon instCategory CategoryTheory.Functor.comp CategoryTheory.Comon CategoryTheory.Comon.instCategory CategoryTheory.Comon.monoidal toMonComon ofMonComon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	toMonComon_ofMonComon_obj_one
toMon_forget 📖	mathematical	—	CategoryTheory.Functor.comp CategoryTheory.Bimon instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory toMon CategoryTheory.Mon.forget forget	—	—
toTrivial_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal trivial toTrivial CategoryTheory.ComonObj.counit CategoryTheory.Comon.X CategoryTheory.Comon.comon	—	—
trivialTo_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal trivial trivialTo Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.trivial CategoryTheory.Comon.X Unique.instInhabited CategoryTheory.Mon.uniqueHomFromTrivial	—	—
trivial_X_X 📖	mathematical	—	CategoryTheory.Mon.X CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal trivial CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
trivial_X_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.mon CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal trivial CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_X_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.mon CategoryTheory.Comon.X CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Mon.monMonoidal trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
trivial_comon_comul_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ComonObj.comul CategoryTheory.Comon.comon trivial CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_comon_counit_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal CategoryTheory.ComonObj.counit CategoryTheory.Comon.comon trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Bimon.Mon_Class.tensorObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_def 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.tensorObj.instTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonObj.tensorObj.mul_def

CategoryTheory.BimonObj

Definitions

Name	Category	Theorems
toComonObj 📖	CompOp	26 math math: one_comul, CategoryTheory.Bimon.compatibility_assoc, mul_counit_assoc, CategoryTheory.HopfObj.antipode_left, CategoryTheory.HopfObj.antipode_comul, CategoryTheory.Bimon.one_comul, CategoryTheory.HopfObj.antipode_comul₂, mul_comul_assoc, CategoryTheory.HopfObj.antipode_left_assoc, one_counit_assoc, mul_counit, one_comul_assoc, CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.Bimon.mul_counit, CategoryTheory.HopfObj.antipode_right_assoc, one_counit, CategoryTheory.Bimon.one_comul_assoc, CategoryTheory.HopfObj.antipode_comul₁, CategoryTheory.HopfObj.mul_antipode₂, CategoryTheory.HopfObj.antipode_counit, mul_comul, CategoryTheory.Bimon.mul_counit_assoc, CategoryTheory.HopfObj.antipode_right, CategoryTheory.Bimon.compatibility, CategoryTheory.IsBimonHom.toIsComonHom, CategoryTheory.HopfObj.antipode_counit_assoc
toMonObj 📖	CompOp	26 math math: one_comul, CategoryTheory.HopfObj.mul_antipode, CategoryTheory.Bimon.compatibility_assoc, mul_counit_assoc, CategoryTheory.HopfObj.one_antipode, CategoryTheory.HopfObj.antipode_left, CategoryTheory.Bimon.one_comul, CategoryTheory.HopfObj.antipode_comul₂, mul_comul_assoc, CategoryTheory.HopfObj.antipode_left_assoc, one_counit_assoc, mul_counit, one_comul_assoc, CategoryTheory.IsBimonHom.toIsMonHom, CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.Bimon.mul_counit, CategoryTheory.HopfObj.antipode_right_assoc, one_counit, CategoryTheory.Bimon.one_comul_assoc, CategoryTheory.HopfObj.antipode_comul₁, CategoryTheory.HopfObj.mul_antipode₂, mul_comul, CategoryTheory.Bimon.mul_counit_assoc, CategoryTheory.HopfObj.antipode_right, CategoryTheory.Bimon.compatibility, CategoryTheory.HopfObj.one_antipode_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul toMonObj CategoryTheory.ComonObj.comul toComonObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.tensorμ	—	—
mul_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul toMonObj CategoryTheory.ComonObj.comul toComonObj CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.tensorμ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_comul
mul_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonObj.mul toMonObj CategoryTheory.ComonObj.counit toComonObj CategoryTheory.Comon.instComonObjTensorObj	—	—
mul_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul toMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.ComonObj.counit toComonObj CategoryTheory.Comon.instComonObjTensorObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_counit
one_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.one toMonObj CategoryTheory.ComonObj.comul toComonObj CategoryTheory.Mon.instMonObjTensorObj	—	—
one_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one toMonObj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ComonObj.comul toComonObj CategoryTheory.Mon.instMonObjTensorObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_comul
one_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one toMonObj CategoryTheory.ComonObj.counit toComonObj CategoryTheory.CategoryStruct.id	—	—
one_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one toMonObj CategoryTheory.ComonObj.counit toComonObj	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' one_counit

CategoryTheory.IsBimonHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsComonHom 📖	mathematical	—	CategoryTheory.IsComonHom CategoryTheory.BimonObj.toComonObj	—	—
toIsMonHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.BimonObj.toMonObj	—	—

---

← Back to Index