Bimon_

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

Statistics

Metric	Count
Definitions Bimon, equivMonComon, equivMonComonCounitIsoApp, equivMonComonCounitIsoAppX, equivMonComonCounitIsoAppXAux, equivMonComonUnitIsoApp, equivMonComonUnitIsoAppX, equivMonComonUnitIsoAppXAux, forget, instBimonObjXXMon, instCategory, mk', mk'X, ofMonComon, ofMonComonObj, ofMonComonObjX, toComon, toMon, toMonComon, toMonComonObj, toTrivial, trivial, trivialTo, BimonObj, toComonObj, toMonObj, IsBimonHom	27
Theorems BimonObjAux_comul, BimonObjAux_counit, 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, 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_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	70
Total	97

CategoryTheory

Definitions

Name	Category	Theorems
Bimon 📖	CompOp	37 math math: Bimon.toMonComonObj_mon_mul_hom, 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.equivMonComonUnitIsoAppX_inv_hom, Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, Bimon.BimonObjAux_counit, Bimon.ofMonComon_toMonComon_obj_counit, Bimon.equivMonComonUnitIsoAppXAux_inv, Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, Bimon.equivMonComonCounitIsoAppX_hom_hom, Bimon.equivMonComonUnitIsoApp_inv_hom_hom, 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.comp_hom', Bimon.toMonComonObj_X, Bimon.equivMonComonCounitIsoApp_inv_hom_hom, Bimon.toComon_obj_comon_comul
BimonObj 📖	CompData	—
IsBimonHom 📖	CompData	—

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
forget 📖	CompOp	2 math math: toMon_forget, toComon_forget
instBimonObjXXMon 📖	CompOp	—
instCategory 📖	CompOp	37 math math: toMonComonObj_mon_mul_hom, 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, equivMonComonUnitIsoAppX_inv_hom, instIsComonHomMonHomEquivMonComonUnitIsoAppX, BimonObjAux_counit, ofMonComon_toMonComon_obj_counit, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, 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, comp_hom', toMonComonObj_X, 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	22 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, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, ofMonComon_map_hom, ofMonComon_obj, equivMonComonCounitIsoAppX_inv_hom, toMonComon_ofMonComon_obj_mul, equivMonComonCounitIsoApp_hom_hom_hom, ofMonComon_toMonComon_obj_comul, equivMonComonCounitIsoAppXAux_hom, 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	6 math math: ofMonComonObjX_mul, ofMonComonObj_comon_comul_hom, ofMonComonObj_comon_counit_hom, ofMonComonObjX_one, ofMonComonObjX_X, ofMonComonObj_X
toComon 📖	CompOp	11 math math: toMonComonObj_mon_mul_hom, toComon_obj_comon_counit, toComon_map_hom, toComon_obj_X, toComon_forget, BimonObjAux_counit, toMonComonObj_mon_one_hom, BimonObjAux_comul, toMonComon_map_hom, toMonComonObj_X, toComon_obj_comon_comul
toMon 📖	CompOp	1 math math: toMon_forget
toMonComon 📖	CompOp	22 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, equivMonComonUnitIsoAppXAux_inv, instIsMonHomHomEquivMonComonUnitIsoAppXAux, equivMonComonCounitIsoAppX_hom_hom, equivMonComonUnitIsoApp_inv_hom_hom, toMonComon_obj, equivMonComonCounitIsoAppX_inv_hom, toMonComon_ofMonComon_obj_mul, equivMonComonCounitIsoApp_hom_hom_hom, ofMonComon_toMonComon_obj_comul, toMonComon_map_hom, equivMonComonCounitIsoAppXAux_hom, equivMonComonCounitIsoApp_inv_hom_hom
toMonComonObj 📖	CompOp	5 math math: toMonComonObj_mon_mul_hom, toMonComon_obj, toMonComonObj_mon_one_hom, toMonComon_map_hom, toMonComonObj_X
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
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	—	—
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_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.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