Comon_

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

Statistics

Metric	Count
Definitions Comon, ComonToMonOpOp, ComonToMonOpOpObj, ComonToMonOpOpObjMon, Comon_EquivMon_OpOp, Comon_ToMon_OpOp, Comon_ToMon_OpOpObj, Comon_ToMon_OpOpObjMon, hom, mk', MonOpOpToComon, MonOpOpToComonObj, MonOpOpToComonObjComon, Mon_OpOpToComonObj, Mon_OpOpToComonObjComon, Mon_OpOpToComon_, X, comon, comp, forget, homInhabited, id, instCategory, instComonObjTensorObj, instInhabited, instMonoidalForget, mkIso, mkIso', monoidal, trivial, uniqueHomToTrivial, ComonObj, comul, counit, instTensorUnit, termΔ, termε, «termΔ[_]», «termε[_]», Comon_, mapComon, instComonObj, IsCommComonObj, IsComonHom, IsComon_Hom	45
Theorems ComonToMonOpOpObj_X, ComonToMonOpOpObj_mon_mul, ComonToMonOpOpObj_mon_one, ComonToMonOpOp_map, ComonToMonOpOp_obj, Comon_EquivMon_OpOp_counitIso, Comon_EquivMon_OpOp_functor, Comon_EquivMon_OpOp_inverse, Comon_EquivMon_OpOp_unitIso, ext, ext_iff, isComonHom_hom, MonOpOpToComonObj_X, MonOpOpToComonObj_comon_comul, MonOpOpToComonObj_comon_counit, MonOpOpToComon_map_hom, MonOpOpToComon_obj, comp_hom, comp_hom', ext, ext_iff, forget_faithful, forget_map, forget_obj, forget_δ, forget_ε, forget_η, forget_μ, id_hom, id_hom', instHasTerminal, instIsComonHomHom, instIsIsoHomOfMapForget, instReflectsIsomorphismsForget, mkIso'_hom_hom, mkIso'_inv_hom, mkIso_hom_hom, mkIso_inv_hom, monoidal_associator_hom_hom, monoidal_associator_inv_hom, monoidal_leftUnitor_hom_hom, monoidal_leftUnitor_inv_hom, monoidal_rightUnitor_hom_hom, monoidal_rightUnitor_inv_hom, monoidal_tensorHom_hom, monoidal_tensorObj_X, monoidal_tensorObj_comon_comul, monoidal_tensorObj_comon_counit, monoidal_tensorUnit_X, monoidal_tensorUnit_comon_comul, monoidal_tensorUnit_comon_counit, monoidal_whiskerLeft_hom, monoidal_whiskerRight_hom, tensorObj_X, tensorObj_comul, tensorObj_comul', tensorObj_counit, trivial_X, trivial_comon_comul, trivial_comon_counit, uniqueHomToTrivial_default_hom, comul_assoc, comul_assoc_assoc, comul_assoc_flip, comul_assoc_flip_assoc, comul_counit, comul_counit_assoc, comul_counit_hom, comul_counit_hom_assoc, counit_comul, counit_comul_assoc, counit_comul_hom, counit_comul_hom_assoc, instTensorUnit_comul, instTensorUnit_counit, instIsComon_Hom, mapComon_map_hom, mapComon_obj_X, mapComon_obj_comon_comul, mapComon_obj_comon_counit, Δ_def, Δ_def_assoc, ε_def, ε_def_assoc, comul_comm, comul_comm_assoc, hom_comul, hom_comul_assoc, hom_counit, hom_counit_assoc, instIsComonHomComp, instIsComonHomId, instIsComonHomInv, instIsComonHomInvOfHom	94
Total	139

CategoryTheory

Definitions

Name	Category	Theorems
Comon 📖	CompData	122 math math: comonEquiv_unitIso, Comon.monoidal_tensorUnit_X, Bimon.toMonComonObj_mon_mul_hom, Bimon.Bimon_ClassAux_comul, Bimon.equivMonComonUnitIsoAppX_hom_hom, Functor.mapComon_obj_X, Bimon.ofMonComonObjX_mul, Comon.MonOpOpToComon_obj, Comon.uniqueHomToTrivial_default_hom, Comon.ComonToMonOpOp_obj, Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom, Bimon.toMonComon_ofMonComon_obj_one, Comon.Comon_EquivMon_OpOp_counitIso, Bimon.equivMonComonUnitIsoAppXAux_hom, Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj, CommComon.comp_hom, comonEquiv_functor, Comon.monoidal_rightUnitor_inv_hom, Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, Bimon.equivMonComonUnitIsoApp_hom_hom_hom, Bimon.toComon_obj_comon_counit, Bimon.toComon_map_hom, CoalgCat.comonEquivalence_inverse, Bimon.ofMonComonObj_comon_comul_hom, CoalgCat.comonEquivalence_counitIso, Comon.Comon_EquivMon_OpOp_functor, Bimon.toComon_obj_X, Comon.MonOpOpToComon_map_hom, Comon.instHasTerminal, Comon.forget_η, Bimon.equivMonComonCounitIsoAppXAux_inv, CommComon.forget₂Comon_map, Functor.mapComon_map_hom, Comon.ComonToMonOpOp_map, Comon.forget_δ, Bimon.ofMon_Comon_ObjX_one, Comon.monoidal_whiskerLeft_hom, Comon.mkIso'_hom_hom, Bimon.toComon_forget, Comon.mkIso_hom_hom, Comon.monoidal_leftUnitor_hom_hom, Bimon.ofMon_Comon_ObjX_mul, Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, Bimon.Bimon_ClassAux_counit, Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X, Comon.mkIso_inv_hom, Bimon.equivMonComonUnitIsoAppX_inv_hom, Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, Bimon.BimonObjAux_counit, Functor.mapComon_obj_comon_comul, Comon.monoidal_whiskerRight_hom, CoalgCat.comonEquivalence_functor, Bimon.ofMonComon_toMonComon_obj_counit, isoCartesianComon_hom_hom, Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, Monoidal.comonFunctorCategoryEquivalence_unitIso, CommComon.hom_ext_iff, Comon.monoidal_associator_hom_hom, Bimon.ofMon_Comon_toMon_Comon_obj_comul, Bimon.equivMonComonUnitIsoAppXAux_inv, Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, Monoidal.comonFunctorCategoryEquivalence_functor, CoalgCat.comonEquivalence_unitIso, Bimon.equivMonComonCounitIsoAppX_hom_hom, Monoidal.ComonFunctorCategoryEquivalence.functor_obj, Comon.Comon_EquivMon_OpOp_unitIso, Bimon.equivMonComonUnitIsoApp_inv_hom_hom, Bimon.ofMon_Comon_toMon_Comon_obj_counit, Bimon.ofMonComonObj_comon_counit_hom, Bimon.ofMonComon_map_hom, Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom, Bimon.ofMonComon_obj, Comon.forget_map, Functor.mapComon_obj_comon_counit, Comon.monoidal_tensorUnit_comon_comul, Comon.instReflectsIsomorphismsForget, Bimon.ofMonComonObjX_one, Bimon.toMonComon_obj, Bimon.equivMonComonCounitIsoAppX_inv_hom, Bimon.toMonComonObj_mon_one_hom, Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, Monoidal.comonFunctorCategoryEquivalence_counitIso, Bimon.toMonComon_ofMonComon_obj_mul, Bimon.BimonObjAux_comul, Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, CommComon.id_hom, Bimon.equivMonComonCounitIsoApp_hom_hom_hom, Bimon.ofMonComon_toMonComon_obj_comul, Comon.monoidal_leftUnitor_inv_hom, Bimon.ofMonComonObjX_X, Comon.monoidal_rightUnitor_hom_hom, Comon.monoidal_tensorObj_X, CoalgCat.toComon_map_hom, Comon.mkIso'_inv_hom, Comon.forget_faithful, Comon.monoidal_associator_inv_hom, Comon.Comon_EquivMon_OpOp_inverse, Bimon.toMonComon_map_hom, CommComon.forget₂Comon_obj_comon, Monoidal.comonFunctorCategoryEquivalence_inverse, Comon.monoidal_tensorUnit_comon_counit, Comon.forget_μ, Bimon.equivMonComonCounitIsoAppXAux_hom, Comon.monoidal_tensorHom_hom, Comon.forget_ε, isoCartesianComon_inv_hom, Bimon.toMon_Comon_ofMon_Comon_obj_mul, Comon.comp_hom', Bimon.toMonComonObj_X, Comon.tensorObj_X, Bimon.toMon_Comon_ofMon_Comon_obj_one, comonEquiv_inverse, Bimon.equivMonComonCounitIsoApp_inv_hom_hom, Comon.monoidal_tensorObj_comon_counit, Comon.forget_obj, CommComon.forget₂Comon_obj_X, CoalgCat.toComon_obj, Comon.id_hom', Bimon.toComon_obj_comon_comul, comonEquiv_counitIso, Comon.monoidal_tensorObj_comon_comul
ComonObj 📖	CompData	—
Comon_ 📖	CompOp	—
IsCommComonObj 📖	CompData	4 math math: CartesianCopyDiscard.instIsCommComonObjOfCartesian, CommComon.comm, CommComon.instCommComonObjUnit, CopyDiscardCategory.isCommComonObj
IsComonHom 📖	CompData	10 math math: Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, instIsComonHomComp, Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, Functor.map.instIsComon_Hom, instIsComonHomId, instIsComonHomInvOfHom, instIsComonHomInv, Comon.Hom.isComonHom_hom, IsBimonHom.toIsComonHom, Comon.instIsComonHomHom
IsComon_Hom 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsComonHomComp 📖	mathematical	—	IsComonHom CategoryStruct.comp Category.toCategoryStruct	—	Category.assoc IsComonHom.hom_counit IsComonHom.hom_comul IsComonHom.hom_comul_assoc MonoidalCategory.tensorHom_comp_tensorHom
instIsComonHomId 📖	mathematical	—	IsComonHom CategoryStruct.id Category.toCategoryStruct	—	Category.id_comp MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.comp_id
instIsComonHomInv 📖	mathematical	—	IsComonHom inv	—	IsComonHom.hom_counit IsComonHom.hom_comul_assoc MonoidalCategory.tensorHom_comp_tensorHom IsIso.hom_inv_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.comp_id
instIsComonHomInvOfHom 📖	mathematical	—	IsComonHom Iso.inv	—	IsComonHom.hom_counit IsComonHom.hom_comul_assoc MonoidalCategory.tensorHom_comp_tensorHom Iso.hom_inv_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.comp_id

CategoryTheory.Comon

Definitions

Name	Category	Theorems
ComonToMonOpOp 📖	CompOp	5 math math: ComonToMonOpOp_obj, Comon_EquivMon_OpOp_counitIso, Comon_EquivMon_OpOp_functor, ComonToMonOpOp_map, Comon_EquivMon_OpOp_unitIso
ComonToMonOpOpObj 📖	CompOp	7 math math: ComonToMonOpOp_obj, ComonToMonOpOp_map, ComonToMonOpOpObj_mon_mul, monoidal_tensorObj_comon_counit, ComonToMonOpOpObj_X, monoidal_tensorObj_comon_comul, ComonToMonOpOpObj_mon_one
ComonToMonOpOpObjMon 📖	CompOp	—
Comon_EquivMon_OpOp 📖	CompOp	15 math math: Comon_EquivMon_OpOp_counitIso, monoidal_rightUnitor_inv_hom, Comon_EquivMon_OpOp_functor, monoidal_whiskerLeft_hom, monoidal_leftUnitor_hom_hom, monoidal_whiskerRight_hom, monoidal_associator_hom_hom, Comon_EquivMon_OpOp_unitIso, monoidal_leftUnitor_inv_hom, monoidal_rightUnitor_hom_hom, monoidal_associator_inv_hom, Comon_EquivMon_OpOp_inverse, monoidal_tensorHom_hom, monoidal_tensorObj_comon_counit, monoidal_tensorObj_comon_comul
Comon_ToMon_OpOp 📖	CompOp	—
Comon_ToMon_OpOpObj 📖	CompOp	—
Comon_ToMon_OpOpObjMon 📖	CompOp	—
MonOpOpToComon 📖	CompOp	5 math math: MonOpOpToComon_obj, Comon_EquivMon_OpOp_counitIso, MonOpOpToComon_map_hom, Comon_EquivMon_OpOp_unitIso, Comon_EquivMon_OpOp_inverse
MonOpOpToComonObj 📖	CompOp	5 math math: MonOpOpToComon_obj, MonOpOpToComon_map_hom, MonOpOpToComonObj_comon_comul, MonOpOpToComonObj_X, MonOpOpToComonObj_comon_counit
MonOpOpToComonObjComon 📖	CompOp	—
Mon_OpOpToComonObj 📖	CompOp	—
Mon_OpOpToComonObjComon 📖	CompOp	—
Mon_OpOpToComon_ 📖	CompOp	—
X 📖	CompOp	101 math math: monoidal_tensorUnit_X, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Functor.mapComon_obj_X, CategoryTheory.Bimon.ofMonComonObjX_mul, CategoryTheory.Bimon.ext_iff, uniqueHomToTrivial_default_hom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, CategoryTheory.CommComon.comp_hom, monoidal_rightUnitor_inv_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Bimon.toComon_map_hom, CategoryTheory.Bimon.trivial_X_X, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CategoryTheory.Bimon.toComon_obj_X, id_hom, comp_hom, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv, CategoryTheory.Functor.mapComon_map_hom, ComonToMonOpOp_map, CoalgCat.toComonObj_X, forget_δ, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, monoidal_whiskerLeft_hom, mkIso'_hom_hom, monoidal_leftUnitor_hom_hom, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.CommComon.toComon_X, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Functor.mapComon_obj_comon_comul, monoidal_whiskerRight_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, CategoryTheory.isoCartesianComon_hom_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_X, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, monoidal_associator_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, trivial_X, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Bimon.id_hom', CategoryTheory.Bimon.trivialTo_hom, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Functor.mapComon_obj_comon_counit, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, monoidal_leftUnitor_inv_hom, CategoryTheory.Bimon.ofMonComonObjX_X, MonOpOpToComonObj_X, monoidal_rightUnitor_hom_hom, monoidal_tensorObj_X, ComonToMonOpOpObj_mon_mul, CategoryTheory.Bimon.mk'_X, mkIso'_inv_hom, CategoryTheory.Bimon.ofMonComonObj_X, monoidal_associator_inv_hom, forget_μ, instIsIsoHomOfMapForget, Hom.isComonHom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom, monoidal_tensorHom_hom, CategoryTheory.Bimon.trivial_X_mon_mul, CategoryTheory.isoCartesianComon_inv_hom, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, comp_hom', CategoryTheory.Bimon.comp_hom', tensorObj_X, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, monoidal_tensorObj_comon_counit, forget_obj, CategoryTheory.CommComon.forget₂Comon_obj_X, instIsComonHomHom, ComonToMonOpOpObj_X, id_hom', CategoryTheory.Bimon.toComon_obj_comon_comul, monoidal_tensorObj_comon_comul, CategoryTheory.Bimon.trivial_X_mon_one, ComonToMonOpOpObj_mon_one
comon 📖	CompOp	41 math math: CategoryTheory.Bimon.Bimon_ClassAux_comul, uniqueHomToTrivial_default_hom, CategoryTheory.Bimon.trivial_comon_counit_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Bimon.toComon_map_hom, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CategoryTheory.Bimon.trivial_comon_comul_hom, CategoryTheory.Functor.mapComon_map_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit, CategoryTheory.Bimon.BimonObjAux_counit, MonOpOpToComonObj_comon_comul, CategoryTheory.Functor.mapComon_obj_comon_comul, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Functor.mapComon_obj_comon_counit, monoidal_tensorUnit_comon_comul, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, ComonToMonOpOpObj_mon_mul, trivial_comon_counit, CategoryTheory.CommComon.forget₂Comon_obj_comon, monoidal_tensorUnit_comon_counit, Hom.isComonHom_hom, MonOpOpToComonObj_comon_counit, monoidal_tensorObj_comon_counit, instIsComonHomHom, trivial_comon_comul, CategoryTheory.Bimon.toComon_obj_comon_comul, monoidal_tensorObj_comon_comul, ComonToMonOpOpObj_mon_one
comp 📖	CompOp	1 math math: comp_hom
forget 📖	CompOp	16 math math: CategoryTheory.comonEquiv_unitIso, CategoryTheory.comonEquiv_functor, forget_η, forget_δ, CategoryTheory.Bimon.toComon_forget, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X, CategoryTheory.Bimon.ofMonComon_map_hom, forget_map, instReflectsIsomorphismsForget, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, forget_faithful, forget_μ, forget_ε, forget_obj, CategoryTheory.comonEquiv_counitIso
homInhabited 📖	CompOp	—
id 📖	CompOp	1 math math: id_hom
instCategory 📖	CompOp	122 math math: CategoryTheory.comonEquiv_unitIso, monoidal_tensorUnit_X, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Functor.mapComon_obj_X, CategoryTheory.Bimon.ofMonComonObjX_mul, MonOpOpToComon_obj, uniqueHomToTrivial_default_hom, ComonToMonOpOp_obj, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, Comon_EquivMon_OpOp_counitIso, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_obj, CategoryTheory.CommComon.comp_hom, CategoryTheory.comonEquiv_functor, monoidal_rightUnitor_inv_hom, CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Bimon.toComon_map_hom, CoalgCat.comonEquivalence_inverse, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CoalgCat.comonEquivalence_counitIso, Comon_EquivMon_OpOp_functor, CategoryTheory.Bimon.toComon_obj_X, MonOpOpToComon_map_hom, instHasTerminal, forget_η, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv, CategoryTheory.CommComon.forget₂Comon_map, CategoryTheory.Functor.mapComon_map_hom, ComonToMonOpOp_map, forget_δ, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, monoidal_whiskerLeft_hom, mkIso'_hom_hom, CategoryTheory.Bimon.toComon_forget, mkIso_hom_hom, monoidal_leftUnitor_hom_hom, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_X, mkIso_inv_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Functor.mapComon_obj_comon_comul, monoidal_whiskerRight_hom, CoalgCat.comonEquivalence_functor, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, CategoryTheory.isoCartesianComon_hom_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_unitIso, CategoryTheory.CommComon.hom_ext_iff, monoidal_associator_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_functor, CoalgCat.comonEquivalence_unitIso, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_obj, Comon_EquivMon_OpOp_unitIso, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Bimon.ofMonComon_obj, forget_map, CategoryTheory.Functor.mapComon_obj_comon_counit, monoidal_tensorUnit_comon_comul, instReflectsIsomorphismsForget, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Bimon.toMonComon_obj, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_counitIso, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, CategoryTheory.CommComon.id_hom, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, monoidal_leftUnitor_inv_hom, CategoryTheory.Bimon.ofMonComonObjX_X, monoidal_rightUnitor_hom_hom, monoidal_tensorObj_X, CoalgCat.toComon_map_hom, mkIso'_inv_hom, forget_faithful, monoidal_associator_inv_hom, Comon_EquivMon_OpOp_inverse, CategoryTheory.Bimon.toMonComon_map_hom, CategoryTheory.CommComon.forget₂Comon_obj_comon, CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_inverse, monoidal_tensorUnit_comon_counit, forget_μ, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom, monoidal_tensorHom_hom, forget_ε, CategoryTheory.isoCartesianComon_inv_hom, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, comp_hom', CategoryTheory.Bimon.toMonComonObj_X, tensorObj_X, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, CategoryTheory.comonEquiv_inverse, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, monoidal_tensorObj_comon_counit, forget_obj, CategoryTheory.CommComon.forget₂Comon_obj_X, CoalgCat.toComon_obj, id_hom', CategoryTheory.Bimon.toComon_obj_comon_comul, CategoryTheory.comonEquiv_counitIso, monoidal_tensorObj_comon_comul
instComonObjTensorObj 📖	CompOp	5 math math: tensorObj_comul', tensorObj_comul, CategoryTheory.BimonObj.mul_counit_assoc, tensorObj_counit, CategoryTheory.BimonObj.mul_counit
instInhabited 📖	CompOp	—
instMonoidalForget 📖	CompOp	5 math math: forget_η, forget_δ, CategoryTheory.Bimon.ofMonComon_map_hom, forget_μ, forget_ε
mkIso 📖	CompOp	2 math math: mkIso_hom_hom, mkIso_inv_hom
mkIso' 📖	CompOp	2 math math: mkIso'_hom_hom, mkIso'_inv_hom
monoidal 📖	CompOp	58 math math: monoidal_tensorUnit_X, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Bimon.ofMonComonObjX_mul, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, monoidal_rightUnitor_inv_hom, CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, forget_η, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv, forget_δ, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, monoidal_whiskerLeft_hom, monoidal_leftUnitor_hom_hom, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, monoidal_whiskerRight_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, monoidal_associator_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Bimon.ofMonComon_obj, monoidal_tensorUnit_comon_comul, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Bimon.toMonComon_obj, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, monoidal_leftUnitor_inv_hom, CategoryTheory.Bimon.ofMonComonObjX_X, monoidal_rightUnitor_hom_hom, monoidal_tensorObj_X, monoidal_associator_inv_hom, CategoryTheory.Bimon.toMonComon_map_hom, monoidal_tensorUnit_comon_counit, forget_μ, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom, monoidal_tensorHom_hom, forget_ε, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Bimon.toMonComonObj_X, tensorObj_X, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, monoidal_tensorObj_comon_counit, monoidal_tensorObj_comon_comul
trivial 📖	CompOp	4 math math: uniqueHomToTrivial_default_hom, trivial_X, trivial_comon_counit, trivial_comon_comul
uniqueHomToTrivial 📖	CompOp	1 math math: uniqueHomToTrivial_default_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ComonToMonOpOpObj_X 📖	mathematical	—	CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp ComonToMonOpOpObj Opposite.op X	—	—
ComonToMonOpOpObj_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op X CategoryTheory.Mon.mon ComonToMonOpOpObj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul comon	—	—
ComonToMonOpOpObj_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op X CategoryTheory.Mon.mon ComonToMonOpOpObj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit comon	—	—
ComonToMonOpOp_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comon instCategory Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory ComonToMonOpOp Opposite.op Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop ComonToMonOpOpObj Quiver.Hom.op X Hom.hom	—	—
ComonToMonOpOp_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comon instCategory Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory ComonToMonOpOp Opposite.op ComonToMonOpOpObj	—	—
Comon_EquivMon_OpOp_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Comon Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp instCategory CategoryTheory.Mon.instCategory Comon_EquivMon_OpOp CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.comp MonOpOpToComon ComonToMonOpOp CategoryTheory.Functor.id CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
Comon_EquivMon_OpOp_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Comon Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp instCategory CategoryTheory.Mon.instCategory Comon_EquivMon_OpOp ComonToMonOpOp	—	—
Comon_EquivMon_OpOp_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Comon Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp instCategory CategoryTheory.Mon.instCategory Comon_EquivMon_OpOp MonOpOpToComon	—	—
Comon_EquivMon_OpOp_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Comon Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp instCategory CategoryTheory.Mon.instCategory Comon_EquivMon_OpOp CategoryTheory.NatIso.ofComponents CategoryTheory.Functor.id CategoryTheory.Functor.comp ComonToMonOpOp MonOpOpToComon CategoryTheory.Iso.refl CategoryTheory.Functor.obj	—	—
MonOpOpToComonObj_X 📖	mathematical	—	X MonOpOpToComonObj Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp	—	—
MonOpOpToComonObj_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp comon MonOpOpToComonObj Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.Mon.mon	—	—
MonOpOpToComonObj_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp comon MonOpOpToComonObj Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one CategoryTheory.Mon.mon	—	—
MonOpOpToComon_map_hom 📖	mathematical	—	Hom.hom MonOpOpToComonObj Opposite.unop CategoryTheory.Mon Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Functor.map CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory MonOpOpToComon Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X CategoryTheory.Mon.Hom.hom	—	—
MonOpOpToComon_obj 📖	mathematical	—	CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory MonOpOpToComon MonOpOpToComonObj Opposite.unop	—	—
comp_hom 📖	mathematical	—	Hom.hom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X	—	—
comp_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Comon CategoryTheory.Category.toCategoryStruct instCategory X	—	—
ext 📖	—	Hom.hom	—	—	Hom.ext
ext_iff 📖	mathematical	—	Hom.hom	—	ext
forget_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Comon instCategory forget	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Comon instCategory forget Hom.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Comon instCategory forget X	—	—
forget_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Comon instCategory monoidal forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
forget_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Comon instCategory monoidal forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Comon instCategory monoidal forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Comon instCategory monoidal forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
id_hom 📖	mathematical	—	Hom.hom id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
id_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Comon CategoryTheory.Category.toCategoryStruct instCategory X	—	—
instHasTerminal 📖	mathematical	—	CategoryTheory.Limits.HasTerminal CategoryTheory.Comon instCategory	—	CategoryTheory.Limits.hasTerminal_of_unique Unique.instSubsingleton
instIsComonHomHom 📖	mathematical	—	CategoryTheory.IsComonHom X comon Hom.hom	—	Hom.isComonHom_hom
instIsIsoHomOfMapForget 📖	mathematical	—	CategoryTheory.IsIso X Hom.hom	—	—
instReflectsIsomorphismsForget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.Comon instCategory forget	—	instIsIsoHomOfMapForget CategoryTheory.instIsComonHomInv instIsComonHomHom ext CategoryTheory.IsIso.hom_inv_id CategoryTheory.IsIso.inv_hom_id
mkIso'_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.hom CategoryTheory.Comon instCategory mkIso' X	—	—
mkIso'_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Comon instCategory mkIso' X	—	—
mkIso_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.ComonObj.counit comon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorHom	Hom.hom CategoryTheory.Comon instCategory mkIso	—	—
mkIso_inv_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Iso.hom CategoryTheory.ComonObj.counit comon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorHom	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Comon instCategory mkIso	—	—
monoidal_associator_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator monoidal X	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
monoidal_associator_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator monoidal X	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id
monoidal_leftUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor monoidal X	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
monoidal_leftUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor monoidal X	—	CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
monoidal_rightUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor monoidal X	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
monoidal_rightUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor monoidal X	—	CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
monoidal_tensorHom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.tensorHom monoidal X	—	—
monoidal_tensorObj_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidal	—	—
monoidal_tensorObj_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Functor.obj CategoryTheory.Comon instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp comon monoidal Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op X CategoryTheory.MonObj.mul CategoryTheory.Mon.mon ComonToMonOpOpObj	—	—
monoidal_tensorObj_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Functor.obj CategoryTheory.Comon instCategory CategoryTheory.Equivalence.inverse CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp comon monoidal Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit Opposite.op X CategoryTheory.MonObj.one CategoryTheory.Mon.mon ComonToMonOpOpObj	—	—
monoidal_tensorUnit_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Comon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidal	—	—
monoidal_tensorUnit_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite comon CategoryTheory.Comon instCategory monoidal CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
monoidal_tensorUnit_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit Opposite.unop CategoryTheory.Mon.X Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon.instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite comon CategoryTheory.Comon instCategory monoidal CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
monoidal_whiskerLeft_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.whiskerLeft monoidal X	—	—
monoidal_whiskerRight_hom 📖	mathematical	—	Hom.hom CategoryTheory.Functor.obj Opposite CategoryTheory.Mon CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp CategoryTheory.Mon.instCategory CategoryTheory.Comon instCategory CategoryTheory.Equivalence.functor CategoryTheory.Equivalence.symm Comon_EquivMon_OpOp CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.monMonoidal instBraidedCategoryOpposite CategoryTheory.Equivalence.inverse CategoryTheory.MonoidalCategoryStruct.whiskerRight monoidal X	—	—
tensorObj_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Comon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monoidal	—	—
tensorObj_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instComonObjTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.tensorμ	—	tensorObj_comul' CategoryTheory.Category.assoc
tensorObj_comul' 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instComonObjTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop Opposite CategoryTheory.Category.opposite CategoryTheory.monoidalCategoryOp Opposite.op CategoryTheory.MonoidalCategoryStruct.tensorHom Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.MonoidalCategory.tensorμ instBraidedCategoryOpposite	—	—
tensorObj_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instComonObjTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_X 📖	mathematical	—	X trivial CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
trivial_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comon trivial CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comon trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
uniqueHomToTrivial_default_hom 📖	mathematical	—	Hom.hom trivial Quiver.Hom CategoryTheory.Comon CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory Unique.toInhabited uniqueHomToTrivial CategoryTheory.ComonObj.counit X comon	—	—

CategoryTheory.Comon.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	56 math math: CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.ofMonComonObjX_mul, CategoryTheory.Bimon.ext_iff, CategoryTheory.Comon.uniqueHomToTrivial_default_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom, CategoryTheory.CommComon.comp_hom, CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Bimon.toComon_map_hom, ext_iff, CategoryTheory.Comon.MonOpOpToComon_map_hom, CategoryTheory.Comon.id_hom, CategoryTheory.Comon.comp_hom, CategoryTheory.Functor.mapComon_map_hom, CategoryTheory.Comon.ComonToMonOpOp_map, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, CategoryTheory.Comon.monoidal_whiskerLeft_hom, CategoryTheory.Comon.mkIso'_hom_hom, CategoryTheory.Comon.mkIso_hom_hom, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, CategoryTheory.Comon.ext_iff, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Comon.mkIso_inv_hom, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.isoCartesianComon_hom_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, CategoryTheory.CommComon.hom_ext_iff, CategoryTheory.Comon.monoidal_associator_hom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.id_hom', CategoryTheory.Bimon.trivialTo_hom, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Comon.forget_map, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, CategoryTheory.CommComon.id_hom, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, CoalgCat.toComon_map_hom, CategoryTheory.Comon.mkIso'_inv_hom, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comon.instIsIsoHomOfMapForget, isComonHom_hom, CategoryTheory.Comon.monoidal_tensorHom_hom, CategoryTheory.isoCartesianComon_inv_hom, CategoryTheory.Comon.comp_hom', CategoryTheory.Bimon.comp_hom', CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CategoryTheory.Comon.instIsComonHomHom, CategoryTheory.Comon.id_hom'
mk' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
isComonHom_hom 📖	mathematical	—	CategoryTheory.IsComonHom CategoryTheory.Comon.X CategoryTheory.Comon.comon hom	—	—

CategoryTheory.ComonObj

Definitions

Name	Category	Theorems
comul 📖	CompOp	61 math math: CategoryTheory.Comon.tensorObj_comul', CategoryTheory.CommComon.trivial_comon_comul, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Comon.tensorObj_comul, CategoryTheory.BimonObj.one_comul, CategoryTheory.comul_eq_lift, CategoryTheory.CopyDiscardCategory.copy_unit, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CategoryTheory.CopyDiscardCategory.copy_tensor, CategoryTheory.Bimon.compatibility_assoc, CategoryTheory.IsComonHom.hom_comul, comul_counit, CategoryTheory.Bimon.trivial_comon_comul_hom, CategoryTheory.HopfObj.antipode_left, CategoryTheory.Functor.obj.Δ_def_assoc, CategoryTheory.IsComonHom.hom_comul_assoc, CoalgCat.comul_def, CategoryTheory.HopfObj.antipode_comul, CategoryTheory.Bimon.one_comul, counit_comul_assoc, counit_comul_hom, CategoryTheory.HopfObj.antipode_comul₂, CategoryTheory.BimonObj.mul_comul_assoc, CategoryTheory.Comon.MonOpOpToComonObj_comon_comul, CategoryTheory.Functor.mapComon_obj_comon_comul, CategoryTheory.HopfObj.antipode_left_assoc, CoalgCat.ofComonObjCoalgebraStruct_comul, comul_assoc_flip, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.BimonObj.one_comul_assoc, CategoryTheory.Conv.mul_eq, CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.HopfObj.antipode_right_assoc, CategoryTheory.IsCommComonObj.comul_comm_assoc, comul_counit_hom_assoc, CategoryTheory.Comon.monoidal_tensorUnit_comon_comul, counit_comul_hom_assoc, comul_counit_assoc, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_comul_app, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul, comul_assoc, CategoryTheory.Bimon.one_comul_assoc, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, CategoryTheory.HopfObj.antipode_comul₁, CategoryTheory.Comon.ComonToMonOpOpObj_mon_mul, comul_assoc_assoc, CategoryTheory.IsCommComonObj.comul_comm, comul_counit_hom, CategoryTheory.HopfObj.mul_antipode₂, counit_comul, CategoryTheory.BimonObj.mul_comul, comul_assoc_flip_assoc, CategoryTheory.HopfObj.antipode_right, CategoryTheory.Bimon.compatibility, CategoryTheory.Functor.obj.Δ_def, CategoryTheory.Deterministic.copy_natural, CategoryTheory.Comon.trivial_comon_comul, CategoryTheory.Bimon.toComon_obj_comon_comul, instTensorUnit_comul, CategoryTheory.Comon.monoidal_tensorObj_comon_comul
counit 📖	CompOp	59 math math: CategoryTheory.counit_eq_toUnit, CategoryTheory.Comon.uniqueHomToTrivial_default_hom, CategoryTheory.Deterministic.discard_natural, CategoryTheory.MarkovCategory.eq_discard, CategoryTheory.Bimon.trivial_comon_counit_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Functor.obj.ε_def_assoc, comul_counit, CategoryTheory.BimonObj.mul_counit_assoc, CategoryTheory.HopfObj.antipode_left, CategoryTheory.Comon.tensorObj_counit, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverseObj_comon_counit_app, CategoryTheory.Bimon.Bimon_ClassAux_counit, counit_comul_assoc, counit_comul_hom, CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_counit, CategoryTheory.HopfObj.antipode_comul₂, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.HopfObj.antipode_left_assoc, CategoryTheory.IsComonHom.hom_counit, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, CategoryTheory.BimonObj.one_counit_assoc, CategoryTheory.Functor.obj.ε_def, CategoryTheory.BimonObj.mul_counit, CategoryTheory.Conv.one_eq, CategoryTheory.CopyDiscardCategory.discard_unit, instTensorUnit_counit, CategoryTheory.Bicategory.Comonad.counit_def, CategoryTheory.MarkovCategory.discard_natural, CoalgCat.counit_def, CategoryTheory.IsComonHom.hom_counit_assoc, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.CommComon.trivial_comon_counit, CategoryTheory.MarkovCategory.discard_natural_assoc, CategoryTheory.Bimon.mul_counit, CategoryTheory.HopfObj.antipode_right_assoc, CategoryTheory.BimonObj.one_counit, comul_counit_hom_assoc, CategoryTheory.Functor.mapComon_obj_comon_counit, counit_comul_hom_assoc, comul_counit_assoc, CategoryTheory.HopfObj.antipode_comul₁, comul_counit_hom, CategoryTheory.HopfObj.mul_antipode₂, CategoryTheory.Comon.trivial_comon_counit, counit_comul, CategoryTheory.HopfObj.antipode_counit, CoalgCat.ofComonObjCoalgebraStruct_counit, CategoryTheory.CopyDiscardCategory.discard_tensor, CategoryTheory.Comon.monoidal_tensorUnit_comon_counit, CategoryTheory.Bimon.mul_counit_assoc, CategoryTheory.HopfObj.antipode_right, CategoryTheory.Comon.MonOpOpToComonObj_comon_counit, CategoryTheory.HopfObj.antipode_counit_assoc, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, CategoryTheory.Comon.ComonToMonOpOpObj_mon_one
instTensorUnit 📖	CompOp	3 math math: CategoryTheory.CommComon.instCommComonObjUnit, instTensorUnit_counit, instTensorUnit_comul
termΔ 📖	CompOp	—
termε 📖	CompOp	—
«termΔ[_]» 📖	CompOp	—
«termε[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	—
comul_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_assoc
comul_assoc_flip 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	comul_assoc_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
comul_assoc_flip_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_assoc_flip
comul_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit comul CategoryTheory.MonoidalCategoryStruct.whiskerLeft counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
comul_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_counit
comul_counit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit comul CategoryTheory.MonoidalCategoryStruct.tensorHom counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality CategoryTheory.MonoidalCategory.tensorHom_def' comul_counit_assoc
comul_counit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_counit_hom
counit_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit comul CategoryTheory.MonoidalCategoryStruct.whiskerRight counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
counit_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_comul
counit_comul_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit comul CategoryTheory.MonoidalCategoryStruct.tensorHom counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality CategoryTheory.MonoidalCategory.tensorHom_def counit_comul_assoc
counit_comul_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom counit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' counit_comul_hom
instTensorUnit_comul 📖	mathematical	—	comul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
instTensorUnit_counit 📖	mathematical	—	counit CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapComon 📖	CompOp	4 math math: mapComon_obj_X, mapComon_map_hom, mapComon_obj_comon_comul, mapComon_obj_comon_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapComon_map_hom 📖	mathematical	—	CategoryTheory.Comon.Hom.hom obj CategoryTheory.Comon.X obj.instComonObj CategoryTheory.Comon.comon map CategoryTheory.Comon CategoryTheory.Comon.instCategory mapComon	—	—
mapComon_obj_X 📖	mathematical	—	CategoryTheory.Comon.X obj CategoryTheory.Comon CategoryTheory.Comon.instCategory mapComon	—	—
mapComon_obj_comon_comul 📖	mathematical	—	CategoryTheory.ComonObj.comul obj CategoryTheory.Comon.X CategoryTheory.Comon.comon CategoryTheory.Comon CategoryTheory.Comon.instCategory mapComon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct map OplaxMonoidal.δ	—	—
mapComon_obj_comon_counit 📖	mathematical	—	CategoryTheory.ComonObj.counit obj CategoryTheory.Comon.X CategoryTheory.Comon.comon CategoryTheory.Comon CategoryTheory.Comon.instCategory mapComon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct map OplaxMonoidal.η	—	—

CategoryTheory.Functor.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsComon_Hom 📖	mathematical	—	CategoryTheory.IsComonHom CategoryTheory.Functor.obj CategoryTheory.Functor.obj.instComonObj CategoryTheory.Functor.map	—	CategoryTheory.Functor.map_comp_assoc CategoryTheory.IsComonHom.hom_counit CategoryTheory.Category.assoc CategoryTheory.Functor.OplaxMonoidal.δ_natural CategoryTheory.IsComonHom.hom_comul

CategoryTheory.Functor.obj

Definitions

Name	Category	Theorems
instComonObj 📖	CompOp	7 math math: CategoryTheory.Bimon.toComon_map_hom, ε_def_assoc, CategoryTheory.Functor.mapComon_map_hom, Δ_def_assoc, CategoryTheory.Functor.map.instIsComon_Hom, ε_def, Δ_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Δ_def 📖	mathematical	—	CategoryTheory.ComonObj.comul CategoryTheory.Functor.obj instComonObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ	—	—
Δ_def_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul instComonObj CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.δ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' Δ_def
ε_def 📖	mathematical	—	CategoryTheory.ComonObj.counit CategoryTheory.Functor.obj instComonObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η	—	—
ε_def_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit instComonObj CategoryTheory.Functor.map CategoryTheory.Functor.OplaxMonoidal.η	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ε_def

CategoryTheory.IsCommComonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	—
comul_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comul_comm

CategoryTheory.IsComonHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_comul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
hom_comul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.comul CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_comul
hom_counit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit	—	—
hom_counit_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.ComonObj.counit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' hom_counit

---

← Back to Index