Mon_

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

Statistics

Metric	Count
Definitions mapMon, mapMon, mapMon, monObj, mon_Class, instBraidedMonMapMon, instLaxBraidedMonMapMon, instLaxMonoidalMonMapMon, instMonoidalMonMapMon, mapMon, mapMonCompIso, mapMonFunctor, mapMonIdIso, mapMonNatIso, mapMonNatTrans, monObjObj, mon_ClassObj, IsCommMon, IsCommMonObj, IsMonHom, IsMon_Hom, Mon, counitIso, counitIsoAux, instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj, laxMonoidalToMon, monToLaxMonoidal, monToLaxMonoidalObj, unitIso, hom, mk', X, comp, equivLaxMonoidalFunctorPUnit, forget, homInhabited, id, instCategory, instInhabited, instMonObjTensorObj, instMonoidalForget, instSymmetricCategory, mkIso, mkIso', mon, monMonoidal, monMonoidalStruct, trivial, uniqueHomFromTrivial, MonObj, instTensorUnit, mul, ofIso, one, instTensorObj, termη, termμ, «termη[_]», «termμ[_]», Mon_Class	60
Theorems mapMon_counit, mapMon_unit, mapMon_counitIso, mapMon_functor, mapMon_inverse, mapMon_unitIso, mapMon, mapMon, isMonHom_preimage, mapMon_preimage_hom, monObj_mul, monObj_one, comp_mapMon_mul, comp_mapMon_one, essImage_mapMon, id_mapMon_mul, id_mapMon_one, instIsMonHomε, instIsMonHomμ, instIsMonHom, mapMonCompIso_hom_app_hom, mapMonCompIso_inv_app_hom, mapMonFunctor_map_app_hom, mapMonFunctor_obj, mapMonIdIso_hom_app_hom, mapMonIdIso_inv_app_hom, mapMonNatIso_hom_app_hom, mapMonNatIso_inv_app_hom, mapMonNatTrans_app_hom, mapMon_map_hom, mapMon_obj_X, mapMon_obj_mon_mul, mapMon_obj_mon_one, η_def, η_def_assoc, μ_def, μ_def_assoc, instTensorUnit, mul_comm, mul_comm', mul_comm'_assoc, mul_comm_assoc, mul_hom, mul_hom_assoc, one_hom, one_hom_assoc, associator_hom_comp_tensorHom_tensorHom, associator_hom_comp_tensorHom_tensorHom_assoc, associator_hom_comp_tensorHom_tensorHom_comp, associator_hom_comp_tensorHom_tensorHom_comp_assoc, associator_inv_comp_tensorHom_tensorHom, associator_inv_comp_tensorHom_tensorHom_assoc, associator_inv_comp_tensorHom_tensorHom_comp, associator_inv_comp_tensorHom_tensorHom_comp_assoc, eq_mul_one, eq_one_mul, leftUnitor_inv_one_tensor_mul, leftUnitor_inv_one_tensor_mul_assoc, mul_assoc_hom, mul_assoc_hom_assoc, mul_assoc_inv, mul_assoc_inv_assoc, rightUnitor_inv_tensor_one_mul, rightUnitor_inv_tensor_one_mul_assoc, counitIsoAux_IsMon_Hom, counitIsoAux_hom, counitIsoAux_inv, counitIso_hom_app_hom, counitIso_inv_app_hom, isMonHom_counitIsoAux, laxMonoidalToMon_map, laxMonoidalToMon_obj, monToLaxMonoidalObj_map, monToLaxMonoidalObj_obj, monToLaxMonoidalObj_ε, monToLaxMonoidalObj_μ, monToLaxMonoidal_laxMonoidalToMon_obj_mul, monToLaxMonoidal_laxMonoidalToMon_obj_one, monToLaxMonoidal_map_hom_app, monToLaxMonoidal_obj, unitIso_hom_app_hom_app, unitIso_inv_app_hom_app, ext, ext', ext'_iff, ext_iff, isMonHom_hom, associator_hom_hom, associator_inv_hom, braiding_hom_hom, braiding_inv_hom, comp_hom, comp_hom', equivLaxMonoidalFunctorPUnit_counitIso, equivLaxMonoidalFunctorPUnit_functor, equivLaxMonoidalFunctorPUnit_inverse, equivLaxMonoidalFunctorPUnit_unitIso, forget_faithful, forget_map, forget_obj, forget_δ, forget_ε, forget_η, forget_μ, hom_injective, id_hom, id_hom', instHasInitial, instIsIsoHom, instIsIsoHomOfMapForget, instIsMonHomHom, instReflectsIsomorphismsForget, leftUnitor_hom_hom, leftUnitor_inv_hom, mkIso'_hom_hom, mkIso'_inv_hom, mkIso_hom_hom, mkIso_inv_hom, monMonoidalStruct_tensorHom_hom, monMonoidalStruct_tensorObj_X, mul_def, one_def, rightUnitor_hom_hom, rightUnitor_inv_hom, tensorObj_mul, tensorObj_one, tensorUnit_X, tensorUnit_mul, tensorUnit_one, tensor_mul, tensor_one, trivial_X, trivial_mon_mul, trivial_mon_one, uniqueHomFromTrivial_default_hom, whiskerLeft_hom, whiskerRight_hom, Mon_tensor_mul_assoc, Mon_tensor_mul_one, Mon_tensor_one_mul, ext, ext_iff, instIsMonHomHomAssociator, instIsMonHomHomBraiding, instIsMonHomHomLeftUnitor, instIsMonHomHomRightUnitor, instIsMonHomId, instIsMonHomTensorHom, instIsMonHomWhiskerLeft, instIsMonHomWhiskerRight, mul_assoc, mul_assoc_assoc, mul_assoc_flip, mul_assoc_flip_assoc, mul_associator, mul_braiding, mul_def, mul_leftUnitor, mul_mul_mul_comm, mul_mul_mul_comm', mul_mul_mul_comm'_assoc, mul_mul_mul_comm_assoc, mul_one, mul_one_assoc, mul_one_hom, mul_rightUnitor, ofIso_mul, ofIso_one, one_associator, one_braiding, one_def, one_leftUnitor, one_mul, one_mul_assoc, one_mul_hom, one_rightUnitor, mul_def, one_def, mul_mul_mul_comm, mul_mul_mul_comm', instIsCommMonObjTensorObj, instIsMonHomComp, instIsMonHomHomAsIso, instIsMonHomId, instIsMonHomInvOfHom, isMonHom_ofIso	186
Total	246

CategoryTheory

Definitions

Name	Category	Theorems
IsCommMon 📖	MathDef	—
IsCommMonObj 📖	CompData	19 math math: AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral, CommGrp.comm, IsCommMonObj.instTensorUnit, Over.isCommMonObj_mk_pullbackSnd, Preadditive.instIsCommMonObj, IsCommMonObj.ofRepresentableBy, isCommMonObj_iff_commutator_eq_toUnit_η, IsCommMon.ofRepresentableBy, AlgebraicGeometry.Scheme.isCommMonObj_asOver_pullback, Functor.isCommMonObj_obj, isCommMonObj_iff_isMulCommutative, Mon.instIsCommMonObj, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, CommGrpObj.toIsCommMonObj, Grp.instIsCommMonObj, instIsCommMonObjTensorObj, CommMon.comm, instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm, AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed
IsMonHom 📖	CompData	38 math math: MonObj.instIsMonHomHomAssociator, Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, MonObj.instIsMonHomHomBraiding, instIsMonHomHomAsIso, Mon.instIsMonHomHom, MonObj.instIsMonHomOne, MonObj.instIsMonHomToUnit, MonObj.instIsMonHomTensorHom, Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, MonObj.instIsMonHomId, MonObj.mop_isMonHom, Functor.instIsMonHomμ, instIsMonHomComp, MonObj.instIsMonHomSnd, Grp.instIsMonHom, AlgebraicGeometry.Scheme.isMonHom_fst_id_right, Functor.map.instIsMonHom, MonObj.instIsMonHomHomLeftUnitor, MonObj.instIsMonHomLift, MonObj.instIsMonHomFst, instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom, isMonHom_ofIso, instIsMonHomInvOfIsCommMonObj, Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, instIsMonHomInvHomOfIsCommMonObj, IsBimonHom.toIsMonHom, MonObj.instIsMonHomHomRightUnitor, Functor.instIsMonHomε, instIsMonHomId, Functor.FullyFaithful.isMonHom_preimage, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, MonObj.instIsMonHomWhiskerLeft, instIsMonHomInvOfHom, MonObj.instIsMonHomWhiskerRight, Mon.Hom.isMonHom_hom, Over.isMonHom_pullbackFst_id_right, MonObj.instIsMonHomMulOfIsCommMonObj, MonObj.unmop_isMonHom
IsMon_Hom 📖	MathDef	—
Mon 📖	CompData	378 math math: Grp.mkIso_inv_hom, Grp.Hom.hom_div, Grp.comp', Monoidal.MonFunctorCategoryEquivalence.inverse_obj, Grp.mkIso_hom_hom, Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, Grp.instIsIsoHomHomMon, Grp.homMk'_hom, Bimon.toMonComonObj_mon_mul_hom, Bimon.Bimon_ClassAux_comul, Functor.mapMonNatTrans_app_hom, Bimon.equivMonComonUnitIsoAppX_hom_hom, Functor.FullyFaithful.mapMon_preimage_hom, CommMon.comp_hom, Grp.Hom.hom_hom_zpow, Equivalence.mapMon_inverse, Mon.EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, Functor.mapCommMonNatIso_inv_app_hom_hom, Mon.forget_obj, instFullMonFunctorOppositeMonCatYonedaMon, Mon.leftUnitor_inv_hom, Functor.mapCommMon_obj_mon_mul, Mon.forget_μ, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, Adjunction.mapMon_unit, Grp.id', Bimon.ext_iff, Mon.equivLaxMonoidalFunctorPUnit_inverse, Comon.MonOpOpToComon_obj, CommMon.forget_map, Functor.FullyFaithful.mapGrp_preimage, Comon.ComonToMonOpOp_obj, Functor.mapMon_obj_mon_mul, CommGrp.mkIso_inv_hom, Mon.forget_ε, Bimon.toMonComon_ofMonComon_obj_one, Grp.whiskerLeft_hom_hom, Functor.mapGrpIdIso_hom_app_hom_hom, Bimon.toMon_forget, Comon.Comon_EquivMon_OpOp_counitIso, MonObj.mopEquivCompForgetIso_hom_app_unmop, Bimon.equivMonComonUnitIsoAppXAux_hom, Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, Grp.leftUnitor_hom_hom, Functor.mapCommMonNatTrans_app_hom_hom, Comon.monoidal_rightUnitor_inv_hom, Monad.monadMonEquiv_counitIso_hom_app_hom, Bimon.trivial_comon_counit_hom, Bimon.toTrivial_hom, Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, Bimon.equivMonComonUnitIsoApp_hom_hom_hom, Mon.rightUnitor_inv_hom, CommMon.mkIso'_inv_hom_hom, Grp.ε_def, Grp.rightUnitor_hom_hom_hom, Bimon.toComon_obj_comon_counit, Mon.mkIso_hom_hom, Bimon.toComon_map_hom, Grp.lift_hom, Grp.hom_mul, Bimon.trivial_X_X, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, Bimon.ofMonComonObj_comon_comul_hom, Monad.monadToMon_obj, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, Functor.mapMonCompIso_hom_app_hom, Mon.limitConeIsLimit_lift_hom, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, Grp.Hom.hom_zpow, Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, Comon.Comon_EquivMon_OpOp_functor, Bimon.toComon_obj_X, Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, Bimon.trivial_comon_comul_hom, Comon.MonOpOpToComon_map_hom, Grp.associator_inv_hom_hom, Monad.monToMonad_obj, Functor.mapCommMonNatIso_hom_app_hom_hom, MonObj.mopEquiv_functor_obj_mon_one_unmop, Grp.Hom.hom_hom_div, Grp.leftUnitor_hom_hom_hom, CommGrp.instIsIsoMonHomGrp, Grp.forget_map, Monoidal.monFunctorCategoryEquivalence_unitIso, Mon.tensorObj_one, Mon.lift_hom, Mon.whiskerRight_hom, Grp.mkIso_hom_hom_hom, CommMon.instIsIsoHomHomMon, Bimon.equivMonComonCounitIsoAppXAux_inv, CommGrp.forget₂CommMon_map_hom, essImage_yonedaMon, Comon.ComonToMonOpOp_map, Mon.forget_faithful, Grp.rightUnitor_inv_hom_hom, Grp.forget₂Mon_map_hom, Comon.monoidal_whiskerLeft_hom, Equivalence.mapMon_unitIso, Monoidal.monFunctorCategoryEquivalence_functor, Mon.tensorUnit_X, instFaithfulMonFunctorOppositeMonCatYonedaMon, Mon.limit_mon_mul, Functor.mapMon_obj_X, Grp.whiskerRight_hom_hom, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, Functor.mapMonNatIso_hom_app_hom, Grp.Hom.hom_hom_inv, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, Comon.monoidal_leftUnitor_hom_hom, Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, Mon.fst_hom, CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, Grp.μ_def, Functor.mapMonNatIso_inv_app_hom, Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, Grp.snd_hom, Monoidal.MonFunctorCategoryEquivalence.functor_obj, Monad.monadToMon_map_hom, Mon.mkIso_inv_hom, Bimon.Bimon_ClassAux_counit, Grp.whiskerLeft_hom, Bimon.equivMonComonUnitIsoAppX_inv_hom, Adjunction.mapMon_counit, Functor.mapMonFunctor_obj, Functor.mapGrpNatIso_hom_app_hom_hom, Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, Functor.mapCommMonCompIso_inv_app_hom_hom, Functor.comp_mapMon_mul, Functor.mapCommMonIdIso_hom_app_hom_hom, Grp.leftUnitor_inv_hom_hom, yonedaMon_map_app, Mon.instReflectsIsomorphismsForget, Mon.associator_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, MonObj.mopEquiv_inverse_map_hom, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, Bimon.BimonObjAux_counit, Grp.rightUnitor_inv_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, Functor.mapMonFunctor_map_app_hom, Functor.mapMon_obj_mon_one, Functor.mapMonIdIso_hom_app_hom, Comon.monoidal_whiskerRight_hom, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom, CommGrp.hom_ext_iff, Grp.forget₂Mon_obj_mul, MonObj.mopEquiv_inverse_obj_X, Mon.tensorObj_mul, Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app, Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, Grp.Hom.hom_pow, Grp.δ_def, Bimon.ofMonComon_toMonComon_obj_counit, Mon.whiskerLeft_hom, Grp.associator_hom_hom_hom, CommMon.mkIso_inv_hom_hom, Mon.limitCone_π_app_hom, Grp.braiding_inv_hom, Grp.mkIso'_hom_hom_hom, Grp.id_hom, Comon.monoidal_associator_hom_hom, Mon.equivLaxMonoidalFunctorPUnit_counitIso, Functor.mapGrpCompIso_hom_app_hom_hom, Mon.equivLaxMonoidalFunctorPUnit_unitIso, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj, Mon.EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app, Grp.fst_hom, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, Bimon.ofMon_Comon_toMon_Comon_obj_comul, Bimon.equivMonComonUnitIsoAppXAux_inv, CommGrp.mkIso_inv_hom_hom_hom, CommGrp.mkIso'_inv_hom_hom_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, Mon.instIsCommMonObj, Mon.Hom.hom_mul, Monoidal.MonFunctorCategoryEquivalence.inverseObj_X, Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, Mon.associator_inv_hom, CommMon.forget₂Mon_obj_mul, Bimon.equivMonComonCounitIsoAppX_hom_hom, Monad.monToMonad_map_toNatTrans, Mon.mkIso'_inv_hom, Mon.uniqueHomFromTrivial_default_hom, Comon.Comon_EquivMon_OpOp_unitIso, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, MonObj.mopEquiv_functor_map_hom_unmop, Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom, MonObj.mopEquivCompForgetIso_inv_app_unmop, Mon.equivLaxMonoidalFunctorPUnit_functor, Functor.mapCommMon_map_hom_hom, Functor.FullyFaithful.mapCommMon_preimage, Bimon.equivMonComonUnitIsoApp_inv_hom_hom, Bimon.ofMon_Comon_toMon_Comon_obj_counit, Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, Functor.mapGrp_map_hom_hom, CommGrp.forget₂Grp_map_hom, Grp.comp_hom_hom, Bimon.id_hom', Functor.mapMonIdIso_inv_app_hom, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, Bimon.trivialTo_hom, Equivalence.mapMon_counitIso, Bimon.ofMonComonObj_comon_counit_hom, MonObj.mopEquiv_unitIso_hom_app_hom, Grp.braiding_inv_hom_hom, Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CommGrp.mkIso_hom_hom, Functor.mapCommMon_obj_mon_one, Bimon.ofMonComon_map_hom, Functor.Full.mapMon, Mon.tensorUnit_one, MonObj.mopEquiv_functor_obj_X_unmop, Grp.Hom.hom_mul, Mon.Hom.hom_pow, Grp.rightUnitor_hom_hom, Monad.monadMonEquiv_inverse, Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, Bimon.ofMonComon_obj, Grp.forget₂Mon_obj_X, Grp.hom_ext_iff, Grp.homMk''_hom_hom, Comon.monoidal_tensorUnit_comon_comul, CommMon.id_hom, Grp.forget₂Mon_comp_forget, Bimon.toMonComon_obj, Functor.mapMon_map_hom, Functor.FullyFaithful.mapCommGrp_preimage, Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, Mon.leftUnitor_hom_hom, Mon.hasLimitsOfShape, Bimon.equivMonComonCounitIsoAppX_inv_hom, Functor.mapGrpIdIso_inv_app_hom_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, Mon.EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, Bimon.toMonComonObj_mon_one_hom, Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CommGrp.mkIso_hom_hom_hom_hom, CommMon.homMk_hom, Grp.leftUnitor_inv_hom, Functor.id_mapMon_mul, CommMon.mkIso_hom_hom_hom, Equivalence.mapMon_functor, Bimon.toMonComon_ofMonComon_obj_mul, Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, MonObj.mopEquiv_functor_obj_mon_mul_unmop, Bimon.BimonObjAux_comul, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, Functor.mapMonCompIso_inv_app_hom, Mon.limit_X, CommMon.hom_ext_iff, Grp.mkIso_inv_hom_hom, Bimon.equivMonComonCounitIsoApp_hom_hom_hom, Grp.snd_hom_hom, Functor.mapGrpNatTrans_app_hom_hom, Bimon.ofMonComon_toMonComon_obj_comul, Comon.monoidal_leftUnitor_inv_hom, Monoidal.monFunctorCategoryEquivalence_counitIso, CommMon.instFullMonForget₂Mon, Grp.hom_one, Grp.forget₂Mon_obj_one, Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, Mon.forget_preservesLimitsOfShape, Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, Mon.comp_hom', Grp.associator_inv_hom, Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, Mon.braiding_inv_hom, Grp.homMk_hom_hom, Comon.monoidal_rightUnitor_hom_hom, Functor.essImage_mapMon, Mon.forget_η, Monad.monadMonEquiv_counitIso_inv_app_hom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, Bimon.mk'_X, Functor.mapGrpNatIso_inv_app_hom_hom, commBialgCatEquivComonCommAlgCat_inverse_obj, Mon.hom_mul, Mon.limitCone_pt, Functor.mapGrpCompIso_inv_app_hom_hom, Grp.Hom.hom_inv, CommMon.forget₂Mon_comp_forget, Mon.limit_mon_one, Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, MonObj.mopEquiv_inverse_obj_mon_one, Grp.instFaithfulMonForget₂Mon, Monad.monadMonEquiv_functor, Mon.forget_δ, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, Mon.rightUnitor_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, Bimon.ofMonComonObj_X, Grp.braiding_hom_hom, Functor.mapCommGrp_map_hom_hom_hom, Grp.η_def, Comon.monoidal_associator_inv_hom, Comon.Comon_EquivMon_OpOp_inverse, Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, Bimon.toMonComon_map_hom, Grp.associator_hom_hom, Preadditive.commGrpEquivalence_inverse_map, Mon.forget_map, Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, Functor.mapCommGrpNatTrans_app_hom_hom_hom, Functor.mapCommMonIdIso_inv_app_hom_hom, Comon.monoidal_tensorUnit_comon_counit, MonObj.mopEquiv_unitIso_inv_app_hom, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CommMon.forget₂Mon_obj_X, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, yonedaGrp_map_app, Bimon.equivMonComonCounitIsoAppXAux_hom, Mon.monMonoidalStruct_tensorHom_hom, CommGrp.mkIso'_hom_hom_hom_hom, Grp.whiskerRight_hom, Mon.braiding_hom_hom, Grp.tensorHom_hom, Monoidal.MonFunctorCategoryEquivalence.functorObj_obj, CommMon.mkIso'_hom_hom_hom, Grp.Hom.hom_one, CommMon.instFaithfulMonForget₂Mon, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, Grp.fst_hom_hom, Grp.mkIso'_inv_hom_hom, Comon.monoidal_tensorHom_hom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, Functor.id_mapMon_one, Bimon.trivial_X_mon_mul, CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, Bimon.toMon_Comon_ofMon_Comon_obj_mul, Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, Bimon.comp_hom', Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, Grp.braiding_hom_hom_hom, Bimon.toMon_Comon_ofMon_Comon_obj_one, Mon.tensorUnit_mul, Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CommMon.forget₂Mon_map_hom, Comon.monoidal_tensorObj_comon_counit, Mon.tensor_one, Mon.hom_one, yonedaMon_obj, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, Mon.mkIso'_hom_hom, Mon.monMonoidalStruct_tensorObj_X, Mon.EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app, Monoidal.monFunctorCategoryEquivalence_inverse, Functor.comp_mapMon_one, Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CommMon.forget₂Mon_obj_one, Grp.comp_hom, Mon.id_hom', Grp.instFullMonForget₂Mon, Grp.id_hom_hom, Functor.Faithful.mapMon, Bimon.toComon_obj_comon_comul, Mon.snd_hom, Mon.Hom.hom_one, CommGrp.forget_map, Mon.instHasInitial, Comon.monoidal_tensorObj_comon_comul, Bimon.trivial_X_mon_one, Mon.tensor_mul, Functor.mapCommMonCompIso_hom_app_hom_hom, MonObj.mopEquiv_inverse_obj_mon_mul
MonObj 📖	CompData	2 math math: GrpObj.toMon_Class_injective, GrpObj.toMonObj_injective
Mon_Class 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsCommMonObjTensorObj 📖	mathematical	—	IsCommMonObj SymmetricCategory.toBraidedCategory MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Mon.instMonObjTensorObj	—	Iso.isIso_hom BraidedCategory.braiding_tensor_right_hom BraidedCategory.braiding_tensor_left_hom SymmetricCategory.braiding_swap_eq_inv_braiding MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc Category.assoc MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc Iso.inv_hom_id_assoc Iso.hom_inv_id_assoc MonoidalCategory.hom_inv_whiskerRight_assoc Iso.inv_hom_id Category.comp_id MonoidalCategory.whiskerLeft_isIso IsIso.comp_isIso Iso.isIso_inv MonoidalCategory.whiskerRight_isIso IsIso.Iso.inv_hom MonoidalCategory.inv_whiskerLeft IsIso.inv_comp MonoidalCategory.inv_whiskerRight IsIso.Iso.inv_inv MonoidalCategory.hom_inv_whiskerRight MonoidalCategory.pentagon_inv_assoc MonoidalCategory.tensorHom_comp_tensorHom IsCommMonObj.mul_comm
instIsMonHomComp 📖	mathematical	—	IsMonHom CategoryStruct.comp Category.toCategoryStruct	—	IsMonHom.one_hom_assoc IsMonHom.one_hom IsMonHom.mul_hom_assoc IsMonHom.mul_hom MonoidalCategory.tensorHom_comp_tensorHom_assoc
instIsMonHomHomAsIso 📖	mathematical	—	IsMonHom Iso.hom asIso	—	—
instIsMonHomId 📖	mathematical	—	IsMonHom CategoryStruct.id Category.toCategoryStruct	—	Category.comp_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.id_comp
instIsMonHomInvOfHom 📖	mathematical	—	IsMonHom Iso.inv	—	IsMonHom.one_hom Category.assoc IsMonHom.mul_hom MonoidalCategory.tensorHom_comp_tensorHom_assoc Iso.inv_hom_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.id_comp
isMonHom_ofIso 📖	mathematical	—	IsMonHom MonObj.ofIso Iso.hom	—	MonoidalCategory.tensorHom_comp_tensorHom_assoc Iso.hom_inv_id MonoidalCategory.tensorHom_id MonoidalCategory.id_whiskerRight Category.id_comp

CategoryTheory.Adjunction

Definitions

Name	Category	Theorems
mapMon 📖	CompOp	2 math math: mapMon_unit, mapMon_counit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMon_counit 📖	mathematical	—	counit CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal mapMon CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Functor.id CategoryTheory.Iso.inv CategoryTheory.Functor.mapMonCompIso CategoryTheory.Functor.LaxMonoidal.id CategoryTheory.Functor.mapMonNatTrans IsMonoidal.instIsMonoidalCounit CategoryTheory.Iso.hom CategoryTheory.Functor.mapMonIdIso	—	—
mapMon_unit 📖	mathematical	—	unit CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal mapMon CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.LaxMonoidal.id CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor.mapMonIdIso CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Functor.mapMonNatTrans IsMonoidal.instIsMonoidalUnit CategoryTheory.Iso.hom CategoryTheory.Functor.mapMonCompIso	—	—

CategoryTheory.Equivalence

Definitions

Name	Category	Theorems
mapMon 📖	CompOp	4 math math: mapMon_inverse, mapMon_unitIso, mapMon_counitIso, mapMon_functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMon_counitIso 📖	mathematical	—	counitIso CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.mapMon inverse CategoryTheory.Functor.Monoidal.toLaxMonoidal functor CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Functor.id CategoryTheory.Iso.symm CategoryTheory.Functor.mapMonCompIso CategoryTheory.Functor.LaxMonoidal.id CategoryTheory.Functor.mapMonNatIso CategoryTheory.Adjunction.Equivalence.instIsMonoidalCounit CategoryTheory.Functor.mapMonIdIso	—	—
mapMon_functor 📖	mathematical	—	functor CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	—
mapMon_inverse 📖	mathematical	—	inverse CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	—
mapMon_unitIso 📖	mathematical	—	unitIso CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.Iso.trans CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.id CategoryTheory.Functor.mapMon CategoryTheory.Functor.LaxMonoidal.id CategoryTheory.Functor.comp functor CategoryTheory.Functor.Monoidal.toLaxMonoidal inverse CategoryTheory.Iso.symm CategoryTheory.Functor.mapMonIdIso CategoryTheory.Functor.LaxMonoidal.comp CategoryTheory.Functor.mapMonNatIso CategoryTheory.Adjunction.Equivalence.instIsMonoidalUnit CategoryTheory.Functor.mapMonCompIso	—	—

CategoryTheory.Functor

Definitions

Name	Category	Theorems
instBraidedMonMapMon 📖	CompOp	—
instLaxBraidedMonMapMon 📖	CompOp	—
instLaxMonoidalMonMapMon 📖	CompOp	—
instMonoidalMonMapMon 📖	CompOp	—
mapMon 📖	CompOp	39 math math: mapMonNatTrans_app_hom, FullyFaithful.mapMon_preimage_hom, CategoryTheory.Equivalence.mapMon_inverse, mapCommMon_obj_mon_mul, CategoryTheory.Adjunction.mapMon_unit, FullyFaithful.mapGrp_preimage, mapMon_obj_mon_mul, mapMonCompIso_hom_app_hom, CategoryTheory.Equivalence.mapMon_unitIso, mapMon_obj_X, mapMonNatIso_hom_app_hom, mapMonNatIso_inv_app_hom, CategoryTheory.Adjunction.mapMon_counit, mapMonFunctor_obj, comp_mapMon_mul, mapMonFunctor_map_app_hom, mapMon_obj_mon_one, mapMonIdIso_hom_app_hom, mapCommMon_map_hom_hom, FullyFaithful.mapCommMon_preimage, mapGrp_map_hom_hom, mapMonIdIso_inv_app_hom, CategoryTheory.Equivalence.mapMon_counitIso, mapCommMon_obj_mon_one, CategoryTheory.Bimon.ofMonComon_map_hom, Full.mapMon, mapMon_map_hom, FullyFaithful.mapCommGrp_preimage, id_mapMon_mul, CategoryTheory.Equivalence.mapMon_functor, mapMonCompIso_inv_app_hom, mapGrpNatTrans_app_hom_hom, essImage_mapMon, mapCommGrp_map_hom_hom_hom, mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, id_mapMon_one, comp_mapMon_one, Faithful.mapMon
mapMonCompIso 📖	CompOp	6 math math: CategoryTheory.Adjunction.mapMon_unit, mapMonCompIso_hom_app_hom, CategoryTheory.Equivalence.mapMon_unitIso, CategoryTheory.Adjunction.mapMon_counit, CategoryTheory.Equivalence.mapMon_counitIso, mapMonCompIso_inv_app_hom
mapMonFunctor 📖	CompOp	3 math math: mapMonFunctor_obj, mapMonFunctor_map_app_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map
mapMonIdIso 📖	CompOp	6 math math: CategoryTheory.Adjunction.mapMon_unit, CategoryTheory.Equivalence.mapMon_unitIso, CategoryTheory.Adjunction.mapMon_counit, mapMonIdIso_hom_app_hom, mapMonIdIso_inv_app_hom, CategoryTheory.Equivalence.mapMon_counitIso
mapMonNatIso 📖	CompOp	4 math math: CategoryTheory.Equivalence.mapMon_unitIso, mapMonNatIso_hom_app_hom, mapMonNatIso_inv_app_hom, CategoryTheory.Equivalence.mapMon_counitIso
mapMonNatTrans 📖	CompOp	3 math math: mapMonNatTrans_app_hom, CategoryTheory.Adjunction.mapMon_unit, CategoryTheory.Adjunction.mapMon_counit
monObjObj 📖	CompOp	14 math math: map_mul, FullyFaithful.homMulEquiv_apply, instIsMonHomμ, map.instIsMonHom, obj.η_def_assoc, obj.η_def, isCommMonObj_obj, FullyFaithful.homMulEquiv_symm_apply, obj.μ_def, instIsMonHomε, mapMon_map_hom, obj.μ_def_assoc, homMonoidHom_apply, map_one
mon_ClassObj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_mapMon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon comp LaxMonoidal.comp CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ map	—	—
comp_mapMon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon comp LaxMonoidal.comp CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε map	—	—
essImage_mapMon 📖	mathematical	—	essImage CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon Monoidal.toLaxMonoidal CategoryTheory.Mon.X	—	FullyFaithful.map_preimage Monoidal.ε_η_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id Monoidal.μ_δ_assoc
id_mapMon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon id LaxMonoidal.id CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
id_mapMon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon id LaxMonoidal.id CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
instIsMonHomε 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct obj CategoryTheory.MonObj.instTensorUnit monObjObj LaxMonoidal.ε	—	CategoryTheory.Category.id_comp map_id CategoryTheory.Category.comp_id LaxMonoidal.ε_tensorHom_comp_μ_assoc CategoryTheory.MonoidalCategory.id_whiskerLeft LaxMonoidal.left_unitality CategoryTheory.Iso.map_inv_hom_id CategoryTheory.Category.assoc LaxMonoidal.left_unitality_inv_assoc
instIsMonHomμ 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct obj CategoryTheory.Mon.instMonObjTensorObj monObjObj LaxBraided.toLaxMonoidal LaxMonoidal.μ	—	CategoryTheory.MonoidalCategory.leftUnitor_inv_comp_tensorHom_assoc CategoryTheory.Category.assoc LaxMonoidal.μ_natural LaxMonoidal.left_unitality_inv_assoc CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ_assoc map_comp
mapMonCompIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon comp LaxMonoidal.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapMonCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mapMonCompIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory comp mapMon LaxMonoidal.comp CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapMonCompIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mapMonFunctor_map_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.LaxMonoidalFunctor.laxMonoidal CategoryTheory.NatTrans.app map CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Functor category mapMonFunctor CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.Mon.X	—	—
mapMonFunctor_obj 📖	mathematical	—	obj CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Functor CategoryTheory.Mon CategoryTheory.Mon.instCategory category mapMonFunctor mapMon CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.LaxMonoidalFunctor.laxMonoidal	—	—
mapMonIdIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon id LaxMonoidal.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapMonIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mapMonIdIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory id mapMon LaxMonoidal.id CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapMonIdIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
mapMonNatIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor category mapMonNatIso CategoryTheory.Mon.X	—	—
mapMonNatIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor category mapMonNatIso CategoryTheory.Mon.X	—	—
mapMonNatTrans_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.NatTrans.app mapMonNatTrans CategoryTheory.Mon.X	—	—
mapMon_map_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom obj CategoryTheory.Mon.X monObjObj CategoryTheory.Mon.mon map CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon	—	—
mapMon_obj_X 📖	mathematical	—	CategoryTheory.Mon.X obj CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon	—	—
mapMon_obj_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul obj CategoryTheory.Mon.X CategoryTheory.Mon.mon CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.μ map	—	—
mapMon_obj_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one obj CategoryTheory.Mon.X CategoryTheory.Mon.mon CategoryTheory.Mon CategoryTheory.Mon.instCategory mapMon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct LaxMonoidal.ε map	—	—

CategoryTheory.Functor.Faithful

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMon 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon	—	CategoryTheory.Mon.Hom.ext map_injective

CategoryTheory.Functor.Full

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapMon 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal	—	CategoryTheory.Functor.map_surjective CategoryTheory.Functor.map_injective CategoryTheory.Functor.map_comp CategoryTheory.Category.assoc CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Functor.Monoidal.instIsIsoε CategoryTheory.IsMonHom.one_hom CategoryTheory.Mon.instIsMonHomHom CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc CategoryTheory.Functor.Monoidal.instIsIsoμ CategoryTheory.IsMonHom.mul_hom CategoryTheory.Mon.Hom.ext

CategoryTheory.Functor.FullyFaithful

Definitions

Name	Category	Theorems
mapMon 📖	CompOp	4 math math: mapMon_preimage_hom, mapGrp_preimage, mapCommMon_preimage, mapCommGrp_preimage
monObj 📖	CompOp	2 math math: monObj_mul, monObj_one
mon_Class 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMonHom_preimage 📖	mathematical	—	CategoryTheory.IsMonHom preimage	—	map_injective CategoryTheory.Functor.map_comp map_preimage CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Functor.Monoidal.instIsIsoε CategoryTheory.IsMonHom.one_hom CategoryTheory.Functor.Monoidal.instIsIsoμ CategoryTheory.IsMonHom.mul_hom
mapMon_preimage_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom preimage CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.mapMon CategoryTheory.Functor.Monoidal.toLaxMonoidal mapMon CategoryTheory.Mon.X CategoryTheory.Functor.obj	—	—
monObj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul monObj preimage CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.δ	—	—
monObj_one 📖	mathematical	—	CategoryTheory.MonObj.one monObj preimage CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.OplaxMonoidal.η	—	—

CategoryTheory.Functor.map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMonHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Functor.obj CategoryTheory.Functor.monObjObj CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc CategoryTheory.IsMonHom.one_hom CategoryTheory.IsMonHom.mul_hom CategoryTheory.Functor.LaxMonoidal.μ_natural_assoc

CategoryTheory.Functor.obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
η_def 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Functor.obj CategoryTheory.Functor.monObjObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.map	—	—
η_def_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonObj.one CategoryTheory.Functor.monObjObj CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' η_def
μ_def 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Functor.obj CategoryTheory.Functor.monObjObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.map	—	—
μ_def_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Functor.obj CategoryTheory.MonObj.mul CategoryTheory.Functor.monObjObj CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' μ_def

CategoryTheory.IsCommMonObj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTensorUnit 📖	mathematical	—	CategoryTheory.IsCommMonObj CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.instTensorUnit	—	CategoryTheory.braiding_leftUnitor CategoryTheory.MonoidalCategory.unitors_equal
mul_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul	—	—
mul_comm' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc mul_comm
mul_comm'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_comm'
mul_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonObj.mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_comm

CategoryTheory.IsMonHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
mul_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_hom
one_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one	—	—
one_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonObj.one	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_hom

CategoryTheory.Mathlib.Tactic.MonTauto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_comp_tensorHom_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.associator_conjugation CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
associator_hom_comp_tensorHom_tensorHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_comp_tensorHom_tensorHom
associator_hom_comp_tensorHom_tensorHom_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp CategoryTheory.Iso.inv_hom_id
associator_hom_comp_tensorHom_tensorHom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_hom_comp_tensorHom_tensorHom_comp
associator_inv_comp_tensorHom_tensorHom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.MonoidalCategory.associator_conjugation CategoryTheory.Iso.inv_hom_id_assoc
associator_inv_comp_tensorHom_tensorHom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_comp_tensorHom_tensorHom
associator_inv_comp_tensorHom_tensorHom_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.Iso.hom_inv_id_assoc
associator_inv_comp_tensorHom_tensorHom_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' associator_inv_comp_tensorHom_tensorHom_comp
eq_mul_one 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id CategoryTheory.MonObj.one CategoryTheory.MonObj.mul	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonObj.mul_one
eq_one_mul 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.CategoryStruct.id CategoryTheory.MonObj.mul	—	CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonObj.one_mul
leftUnitor_inv_one_tensor_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.mul	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.MonObj.one_mul CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc
leftUnitor_inv_one_tensor_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftUnitor_inv_one_tensor_mul
mul_assoc_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonObj.mul_assoc
mul_assoc_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_assoc_hom
mul_assoc_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.CategoryStruct.id	—	CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.MonObj.mul_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.whiskerLeft_comp
mul_assoc_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_assoc_inv
rightUnitor_inv_tensor_one_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.mul	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.assoc CategoryTheory.MonObj.mul_one CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc
rightUnitor_inv_tensor_one_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightUnitor_inv_tensor_one_mul

CategoryTheory.Mon

Definitions

Name	Category	Theorems
X 📖	CompOp	229 math math: CategoryTheory.Grp.Hom.hom_div, id_hom, CategoryTheory.Grp.instIsIsoHomHomMon, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Functor.mapMonNatTrans_app_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, Bimod.TensorBimod.π_tensor_id_actRight, Bimod.AssociatorBimod.hom_left_act_hom', CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom, CategoryTheory.CommMon.comp_hom, Bimod.RightUnitorBimod.hom_right_act_hom', Bimod.LeftUnitorBimod.hom_right_act_hom', CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.Monad.ofMon_η, EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, forget_obj, leftUnitor_inv_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, forget_μ, CategoryTheory.Bimon.ofMonComonObjX_mul, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, hom_injective, Bimod.whiskerLeft_hom, CategoryTheory.Functor.mapMon_obj_mon_mul, Bimod.TensorBimod.right_assoc', instIsMonHomHom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.Grp.whiskerLeft_hom_hom, MonObj.mopEquivCompForgetIso_hom_app_unmop, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, Bimod.TensorBimod.whiskerLeft_π_actLeft, CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom, Bimod.actRight_one, CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, rightUnitor_inv_hom, Bimod.left_assoc_assoc, CategoryTheory.Bimon.mk'X_X, Bimod.right_assoc, CategoryTheory.Bimon.trivial_X_X, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, Bimod.TensorBimod.actRight_one', CategoryTheory.Functor.mapMonCompIso_hom_app_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Grp.Hom.hom_zpow, CategoryTheory.Bimon.toComon_obj_X, CategoryTheory.Comon.MonOpOpToComon_map_hom, MonObj.mopEquiv_functor_obj_mon_one_unmop, CategoryTheory.Grp.Hom.hom_hom_div, tensorObj_one, lift_hom, whiskerRight_hom, CategoryTheory.CommMon.instIsIsoHomHomMon, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv, Bimod.TensorBimod.middle_assoc', CategoryTheory.Bimon.ofMon_Comon_ObjX_one, tensorUnit_X, limit_mon_mul, CategoryTheory.Functor.mapMon_obj_X, CategoryTheory.Grp.whiskerRight_hom_hom, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CategoryTheory.Functor.mapMonNatIso_hom_app_hom, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, Bimod.right_assoc_assoc, fst_hom, CategoryTheory.Functor.mapMonNatIso_inv_app_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj, Bimod.Hom.left_act_hom, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Grp.whiskerLeft_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.yonedaMon_map_app, associator_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, MonObj.mopEquiv_inverse_map_hom, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, Bimod.middle_assoc_assoc, CategoryTheory.Comon.MonOpOpToComonObj_comon_comul, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_obj, CategoryTheory.Functor.mapMonFunctor_map_app_hom, CategoryTheory.CommMon.toMon_X, CategoryTheory.Functor.mapMon_obj_mon_one, CategoryTheory.Functor.mapMonIdIso_hom_app_hom, Bimod.one_actLeft_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Grp.forget₂Mon_obj_mul, MonObj.mopEquiv_inverse_obj_X, tensorObj_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, whiskerLeft_hom, CategoryTheory.Grp.toMon_X, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, Hom.hom_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_map, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ, associator_inv_hom, CategoryTheory.CommMon.forget₂Mon_obj_mul, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, Bimod.regular_X, uniqueHomFromTrivial_default_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, MonObj.mopEquiv_functor_map_hom_unmop, MonObj.mopEquivCompForgetIso_inv_app_unmop, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.Grp.comp_hom_hom, CategoryTheory.Functor.mapMonIdIso_inv_app_hom, Bimod.one_actLeft, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, Bimod.TensorBimod.left_assoc', MonObj.mopEquiv_unitIso_hom_app_hom, CategoryTheory.Functor.mapCommMon_obj_mon_one, tensorUnit_one, MonObj.mopEquiv_functor_obj_X_unmop, Hom.hom_pow, CategoryTheory.Grp.forget₂Mon_obj_X, Bimod.left_assoc, Bimod.regular_actRight, Bimod.Hom.left_act_hom_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_X, CategoryTheory.Comon.monoidal_tensorUnit_comon_comul, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Functor.mapMon_map_hom, leftUnitor_hom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CategoryTheory.Functor.id_mapMon_mul, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, Bimod.RightUnitorBimod.hom_left_act_hom', MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.Monad.ofMon_μ, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, CategoryTheory.Functor.mapMonCompIso_inv_app_hom, limit_X, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Mod_.trivialAction_X, Bimod.actRight_one_assoc, CategoryTheory.Bimon.ofMonComonObjX_X, Bimod.middle_assoc, CategoryTheory.Comon.MonOpOpToComonObj_X, comp_hom', CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, braiding_inv_hom, CategoryTheory.Functor.essImage_mapMon, CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, commBialgCatEquivComonCommAlgCat_inverse_obj, hom_mul, CategoryTheory.Monad.ofMon_obj, Bimod.TensorBimod.one_act_left', comp_hom, trivial_X, CategoryTheory.Grp.Hom.hom_inv, limit_mon_one, MonObj.mopEquiv_inverse_obj_mon_one, Bimod.whiskerRight_hom, forget_δ, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, rightUnitor_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, Bimod.Hom.right_act_hom, instIsIsoHom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, CategoryTheory.Monad.toMon_X, Hom.isMonHom_hom, Bimod.regular_actLeft, CategoryTheory.Comon.monoidal_tensorUnit_comon_counit, MonObj.mopEquiv_unitIso_inv_app_hom, Bimod.Hom.right_act_hom_assoc, CategoryTheory.CommMon.forget₂Mon_obj_X, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom, monMonoidalStruct_tensorHom_hom, CategoryTheory.Grp.whiskerRight_hom, instIsIsoHomOfMapForget, braiding_hom_hom, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, Bimod.AssociatorBimod.hom_right_act_hom', CategoryTheory.Mod_.trivialAction_mod_smul, CategoryTheory.Functor.id_mapMon_one, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Comon.MonOpOpToComonObj_comon_counit, CategoryTheory.Bimon.toMonComonObj_X, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, tensorUnit_mul, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, tensor_one, hom_one, CategoryTheory.yonedaMon_obj, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, monMonoidalStruct_tensorObj_X, CategoryTheory.Functor.comp_mapMon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.CommMon.forget₂Mon_obj_one, CategoryTheory.Grp.comp_hom, id_hom', CategoryTheory.Comon.ComonToMonOpOpObj_X, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε, snd_hom, Hom.hom_one, Bimod.LeftUnitorBimod.hom_left_act_hom', CategoryTheory.Comon.monoidal_tensorObj_comon_comul, tensor_mul, MonObj.mopEquiv_inverse_obj_mon_mul
comp 📖	CompOp	1 math math: comp_hom
equivLaxMonoidalFunctorPUnit 📖	CompOp	4 math math: equivLaxMonoidalFunctorPUnit_inverse, equivLaxMonoidalFunctorPUnit_counitIso, equivLaxMonoidalFunctorPUnit_unitIso, equivLaxMonoidalFunctorPUnit_functor
forget 📖	CompOp	27 math math: forget_obj, forget_μ, forget_ε, CategoryTheory.Bimon.toMon_forget, MonObj.mopEquivCompForgetIso_hom_app_unmop, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Bimon.toComon_map_hom, limitConeIsLimit_lift_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, forget_faithful, limit_mon_mul, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, instReflectsIsomorphismsForget, limitCone_π_app_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X, MonObj.mopEquivCompForgetIso_inv_app_unmop, CategoryTheory.Grp.forget₂Mon_comp_forget, limit_X, forget_preservesLimitsOfShape, forget_η, CategoryTheory.CommMon.forget₂Mon_comp_forget, limit_mon_one, forget_δ, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, forget_map, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, CategoryTheory.Bimon.toComon_obj_comon_comul
homInhabited 📖	CompOp	—
id 📖	CompOp	1 math math: id_hom
instCategory 📖	CompOp	378 math math: CategoryTheory.Grp.mkIso_inv_hom, CategoryTheory.Grp.Hom.hom_div, CategoryTheory.Grp.comp', CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_obj, CategoryTheory.Grp.mkIso_hom_hom, CategoryTheory.Monad.monadMonEquiv_unitIso_inv_app_toNatTrans_app, CategoryTheory.Grp.instIsIsoHomHomMon, CategoryTheory.Grp.homMk'_hom, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Functor.mapMonNatTrans_app_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom, CategoryTheory.CommMon.comp_hom, CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.Equivalence.mapMon_inverse, EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, forget_obj, CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon, leftUnitor_inv_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, forget_μ, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CategoryTheory.Adjunction.mapMon_unit, CategoryTheory.Grp.id', CategoryTheory.Bimon.ext_iff, equivLaxMonoidalFunctorPUnit_inverse, CategoryTheory.Comon.MonOpOpToComon_obj, CategoryTheory.CommMon.forget_map, CategoryTheory.Functor.FullyFaithful.mapGrp_preimage, CategoryTheory.Comon.ComonToMonOpOp_obj, CategoryTheory.Functor.mapMon_obj_mon_mul, CategoryTheory.CommGrp.mkIso_inv_hom, forget_ε, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.Grp.whiskerLeft_hom_hom, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.Bimon.toMon_forget, CategoryTheory.Comon.Comon_EquivMon_OpOp_counitIso, MonObj.mopEquivCompForgetIso_hom_app_unmop, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.Grp.leftUnitor_hom_hom, CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom, CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom, CategoryTheory.Bimon.trivial_comon_counit_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, rightUnitor_inv_hom, CategoryTheory.CommMon.mkIso'_inv_hom_hom, CategoryTheory.Grp.ε_def, CategoryTheory.Grp.rightUnitor_hom_hom_hom, CategoryTheory.Bimon.toComon_obj_comon_counit, mkIso_hom_hom, CategoryTheory.Bimon.toComon_map_hom, CategoryTheory.Grp.lift_hom, CategoryTheory.Grp.hom_mul, CategoryTheory.Bimon.trivial_X_X, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CategoryTheory.Monad.monadToMon_obj, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, CategoryTheory.Functor.mapMonCompIso_hom_app_hom, limitConeIsLimit_lift_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Grp.Hom.hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Comon.Comon_EquivMon_OpOp_functor, CategoryTheory.Bimon.toComon_obj_X, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Bimon.trivial_comon_comul_hom, CategoryTheory.Comon.MonOpOpToComon_map_hom, CategoryTheory.Grp.associator_inv_hom_hom, CategoryTheory.Monad.monToMonad_obj, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, MonObj.mopEquiv_functor_obj_mon_one_unmop, CategoryTheory.Grp.Hom.hom_hom_div, CategoryTheory.Grp.leftUnitor_hom_hom_hom, CategoryTheory.CommGrp.instIsIsoMonHomGrp, CategoryTheory.Grp.forget_map, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_unitIso, tensorObj_one, lift_hom, whiskerRight_hom, CategoryTheory.Grp.mkIso_hom_hom_hom, CategoryTheory.CommMon.instIsIsoHomHomMon, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv, CategoryTheory.CommGrp.forget₂CommMon_map_hom, CategoryTheory.essImage_yonedaMon, CategoryTheory.Comon.ComonToMonOpOp_map, forget_faithful, CategoryTheory.Grp.rightUnitor_inv_hom_hom, CategoryTheory.Grp.forget₂Mon_map_hom, CategoryTheory.Comon.monoidal_whiskerLeft_hom, CategoryTheory.Equivalence.mapMon_unitIso, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_functor, tensorUnit_X, CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon, limit_mon_mul, CategoryTheory.Functor.mapMon_obj_X, CategoryTheory.Grp.whiskerRight_hom_hom, commBialgCatEquivComonCommAlgCat_functor_obj_unop_X, CategoryTheory.Functor.mapMonNatIso_hom_app_hom, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, fst_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.Grp.μ_def, CategoryTheory.Functor.mapMonNatIso_inv_app_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Grp.snd_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj, CategoryTheory.Monad.monadToMon_map_hom, mkIso_inv_hom, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Grp.whiskerLeft_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Adjunction.mapMon_counit, CategoryTheory.Functor.mapMonFunctor_obj, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Grp.leftUnitor_inv_hom_hom, CategoryTheory.yonedaMon_map_app, instReflectsIsomorphismsForget, associator_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, MonObj.mopEquiv_inverse_map_hom, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Grp.rightUnitor_inv_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_obj_carrier, CategoryTheory.Functor.mapMonFunctor_map_app_hom, CategoryTheory.Functor.mapMon_obj_mon_one, CategoryTheory.Functor.mapMonIdIso_hom_app_hom, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.CommGrp.hom_ext_iff, CategoryTheory.Grp.forget₂Mon_obj_mul, MonObj.mopEquiv_inverse_obj_X, tensorObj_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, CategoryTheory.Grp.Hom.hom_pow, CategoryTheory.Grp.δ_def, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit, whiskerLeft_hom, CategoryTheory.Grp.associator_hom_hom_hom, CategoryTheory.CommMon.mkIso_inv_hom_hom, limitCone_π_app_hom, CategoryTheory.Grp.braiding_inv_hom, CategoryTheory.Grp.mkIso'_hom_hom_hom, CategoryTheory.Grp.id_hom, CategoryTheory.Comon.monoidal_associator_hom_hom, equivLaxMonoidalFunctorPUnit_counitIso, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, equivLaxMonoidalFunctorPUnit_unitIso, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj, EquivLaxMonoidalFunctorPUnit.unitIso_hom_app_hom_app, CategoryTheory.Grp.fst_hom, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, instIsCommMonObj, Hom.hom_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_X, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, associator_inv_hom, CategoryTheory.CommMon.forget₂Mon_obj_mul, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom, CategoryTheory.Monad.monToMonad_map_toNatTrans, mkIso'_inv_hom, uniqueHomFromTrivial_default_hom, CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso, EquivLaxMonoidalFunctorPUnit.counitIsoAux_inv, MonObj.mopEquiv_functor_map_hom_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom, MonObj.mopEquivCompForgetIso_inv_app_unmop, equivLaxMonoidalFunctorPUnit_functor, CategoryTheory.Functor.mapCommMon_map_hom_hom, CategoryTheory.Functor.FullyFaithful.mapCommMon_preimage, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.ofMon_Comon_toMon_Comon_obj_counit, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.CommGrp.forget₂Grp_map_hom, CategoryTheory.Grp.comp_hom_hom, CategoryTheory.Bimon.id_hom', CategoryTheory.Functor.mapMonIdIso_inv_app_hom, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, CategoryTheory.Bimon.trivialTo_hom, CategoryTheory.Equivalence.mapMon_counitIso, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, MonObj.mopEquiv_unitIso_hom_app_hom, CategoryTheory.Grp.braiding_inv_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom, CategoryTheory.Functor.mapCommMon_obj_mon_one, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Functor.Full.mapMon, tensorUnit_one, MonObj.mopEquiv_functor_obj_X_unmop, CategoryTheory.Grp.Hom.hom_mul, Hom.hom_pow, CategoryTheory.Grp.rightUnitor_hom_hom, CategoryTheory.Monad.monadMonEquiv_inverse, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Bimon.ofMonComon_obj, CategoryTheory.Grp.forget₂Mon_obj_X, CategoryTheory.Grp.hom_ext_iff, CategoryTheory.Grp.homMk''_hom_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_comul, CategoryTheory.CommMon.id_hom, CategoryTheory.Grp.forget₂Mon_comp_forget, CategoryTheory.Bimon.toMonComon_obj, CategoryTheory.Functor.mapMon_map_hom, CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, leftUnitor_hom_hom, hasLimitsOfShape, CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom, CategoryTheory.CommMon.homMk_hom, CategoryTheory.Grp.leftUnitor_inv_hom, CategoryTheory.Functor.id_mapMon_mul, CategoryTheory.CommMon.mkIso_hom_hom_hom, CategoryTheory.Equivalence.mapMon_functor, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.Bimon.BimonObjAux_comul, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isAddCommGroup, CategoryTheory.Functor.mapMonCompIso_inv_app_hom, limit_X, CategoryTheory.CommMon.hom_ext_iff, CategoryTheory.Grp.mkIso_inv_hom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Grp.snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_counitIso, CategoryTheory.CommMon.instFullMonForget₂Mon, CategoryTheory.Grp.hom_one, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, forget_preservesLimitsOfShape, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, comp_hom', CategoryTheory.Grp.associator_inv_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, braiding_inv_hom, CategoryTheory.Grp.homMk_hom_hom, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, CategoryTheory.Functor.essImage_mapMon, forget_η, CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, CategoryTheory.Bimon.mk'_X, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, commBialgCatEquivComonCommAlgCat_inverse_obj, hom_mul, limitCone_pt, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.Grp.Hom.hom_inv, CategoryTheory.CommMon.forget₂Mon_comp_forget, limit_mon_one, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, MonObj.mopEquiv_inverse_obj_mon_one, CategoryTheory.Grp.instFaithfulMonForget₂Mon, CategoryTheory.Monad.monadMonEquiv_functor, forget_δ, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, rightUnitor_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_carrier, CategoryTheory.Bimon.ofMonComonObj_X, CategoryTheory.Grp.braiding_hom_hom, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Grp.η_def, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comon.Comon_EquivMon_OpOp_inverse, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, CategoryTheory.Bimon.toMonComon_map_hom, CategoryTheory.Grp.associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, forget_map, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_counit, MonObj.mopEquiv_unitIso_inv_app_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, CategoryTheory.CommMon.forget₂Mon_obj_X, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, CategoryTheory.Monad.monadMonEquiv_unitIso_hom_app_toNatTrans_app, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_X_isModule, EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj, CategoryTheory.yonedaGrp_map_app, CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom, monMonoidalStruct_tensorHom_hom, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, CategoryTheory.Grp.whiskerRight_hom, braiding_hom_hom, CategoryTheory.Grp.tensorHom_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_obj, CategoryTheory.CommMon.mkIso'_hom_hom_hom, CategoryTheory.Grp.Hom.hom_one, CategoryTheory.CommMon.instFaithfulMonForget₂Mon, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CategoryTheory.Grp.fst_hom_hom, CategoryTheory.Grp.mkIso'_inv_hom_hom, CategoryTheory.Comon.monoidal_tensorHom_hom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, CategoryTheory.Functor.id_mapMon_one, CategoryTheory.Bimon.trivial_X_mon_mul, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.Bimon.comp_hom', CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, CategoryTheory.Grp.braiding_hom_hom_hom, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, tensorUnit_mul, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CategoryTheory.CommMon.forget₂Mon_map_hom, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, tensor_one, hom_one, CategoryTheory.yonedaMon_obj, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, mkIso'_hom_hom, monMonoidalStruct_tensorObj_X, EquivLaxMonoidalFunctorPUnit.unitIso_inv_app_hom_app, CategoryTheory.Monoidal.monFunctorCategoryEquivalence_inverse, CategoryTheory.Functor.comp_mapMon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CategoryTheory.CommMon.forget₂Mon_obj_one, CategoryTheory.Grp.comp_hom, id_hom', CategoryTheory.Grp.instFullMonForget₂Mon, CategoryTheory.Grp.id_hom_hom, CategoryTheory.Functor.Faithful.mapMon, CategoryTheory.Bimon.toComon_obj_comon_comul, snd_hom, Hom.hom_one, CategoryTheory.CommGrp.forget_map, instHasInitial, CategoryTheory.Comon.monoidal_tensorObj_comon_comul, CategoryTheory.Bimon.trivial_X_mon_one, tensor_mul, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom, MonObj.mopEquiv_inverse_obj_mon_mul
instInhabited 📖	CompOp	—
instMonObjTensorObj 📖	CompOp	14 math math: CategoryTheory.MonObj.instIsMonHomHomBraiding, CategoryTheory.BimonObj.one_comul, CategoryTheory.Functor.instIsMonHomμ, CategoryTheory.MonObj.instIsMonHomSnd, CategoryTheory.MonObj.instIsMonHomLift, CategoryTheory.MonObj.instIsMonHomFst, CategoryTheory.BimonObj.one_comul_assoc, CategoryTheory.Grp.tensorObj_mul, CategoryTheory.Grp.tensorObj_one, mul_def, CategoryTheory.MonObj.mul_braiding, CategoryTheory.instIsCommMonObjTensorObj, one_def, CategoryTheory.MonObj.instIsMonHomMulOfIsCommMonObj
instMonoidalForget 📖	CompOp	5 math math: forget_μ, forget_ε, CategoryTheory.Bimon.toComon_map_hom, forget_η, forget_δ
instSymmetricCategory 📖	CompOp	3 math math: instIsCommMonObj, braiding_inv_hom, braiding_hom_hom
mkIso 📖	CompOp	2 math math: mkIso_hom_hom, mkIso_inv_hom
mkIso' 📖	CompOp	2 math math: mkIso'_inv_hom, mkIso'_hom_hom
mon 📖	CompOp	103 math math: CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Monad.ofMon_η, EquivLaxMonoidalFunctorPUnit.isMonHom_counitIsoAux, CategoryTheory.Bimon.ofMonComonObjX_mul, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CategoryTheory.Functor.mapMon_obj_mon_mul, Bimod.TensorBimod.right_assoc', instIsMonHomHom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, Bimod.actRight_one, CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX, Bimod.left_assoc_assoc, Bimod.right_assoc, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, Bimod.TensorBimod.actRight_one', trivial_mon_mul, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one, MonObj.mopEquiv_functor_obj_mon_one_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_mul, tensorObj_one, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, limit_mon_mul, Bimod.right_assoc_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_obj, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.yonedaMon_map_app, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, MonObj.mopEquiv_inverse_map_hom, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, CategoryTheory.Monad.toMon_mon, CategoryTheory.Comon.MonOpOpToComonObj_comon_comul, CategoryTheory.Functor.mapMon_obj_mon_one, Bimod.one_actLeft_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.Grp.forget₂Mon_obj_mul, tensorObj_mul, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, ModuleCat.MonModuleEquivalenceAlgebra.inverse_obj_mon, Hom.hom_mul, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ, CategoryTheory.CommMon.forget₂Mon_obj_mul, uniqueHomFromTrivial_default_hom, MonObj.mopEquiv_functor_map_hom_unmop, Bimod.one_actLeft, instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier, Bimod.TensorBimod.left_assoc', trivial_mon_one, tensorUnit_one, Hom.hom_pow, Bimod.left_assoc, Bimod.regular_actRight, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Functor.mapMon_map_hom, EquivLaxMonoidalFunctorPUnit.counitIsoAux_IsMon_Hom, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Functor.id_mapMon_mul, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.Monad.ofMon_μ, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Grp.forget₂Mon_obj_one, CategoryTheory.Mod_.trivialAction_X, Bimod.actRight_one_assoc, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.Comon.ComonToMonOpOpObj_mon_mul, commBialgCatEquivComonCommAlgCat_inverse_obj, hom_mul, Bimod.TensorBimod.one_act_left', limit_mon_one, MonObj.mopEquiv_inverse_obj_mon_one, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, Hom.isMonHom_hom, Bimod.regular_actLeft, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, monMonoidalStruct_tensorHom_hom, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CategoryTheory.Mod_.trivialAction_mod_smul, CategoryTheory.Functor.id_mapMon_one, CategoryTheory.Bimon.trivial_X_mon_mul, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Comon.MonOpOpToComonObj_comon_counit, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, tensorUnit_mul, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, tensor_one, hom_one, CategoryTheory.yonedaMon_obj, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, CategoryTheory.Functor.comp_mapMon_one, CategoryTheory.CommMon.forget₂Mon_obj_one, EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε, Hom.hom_one, CategoryTheory.Comon.monoidal_tensorObj_comon_comul, CategoryTheory.Bimon.trivial_X_mon_one, tensor_mul, MonObj.mopEquiv_inverse_obj_mon_mul, CategoryTheory.Comon.ComonToMonOpOpObj_mon_one
monMonoidal 📖	CompOp	63 math math: CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, forget_μ, CategoryTheory.Bimon.ext_iff, forget_ε, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom, CategoryTheory.Comon.monoidal_rightUnitor_inv_hom, CategoryTheory.Bimon.trivial_comon_counit_hom, CategoryTheory.Bimon.toTrivial_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Grp.ε_def, 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, CategoryTheory.Bimon.trivial_comon_comul_hom, CategoryTheory.Comon.monoidal_whiskerLeft_hom, CategoryTheory.Comon.monoidal_leftUnitor_hom_hom, CategoryTheory.Grp.μ_def, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Comon.monoidal_whiskerRight_hom, CategoryTheory.Grp.δ_def, CategoryTheory.Comon.monoidal_associator_hom_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv, instIsCommMonObj, CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Bimon.id_hom', CategoryTheory.Bimon.trivialTo_hom, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, CategoryTheory.Bimon.ofMonComon_map_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_comul, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Comon.monoidal_leftUnitor_inv_hom, braiding_inv_hom, CategoryTheory.Comon.monoidal_rightUnitor_hom_hom, forget_η, CategoryTheory.Bimon.mk'_X, hom_mul, forget_δ, CategoryTheory.Bimon.ofMonComonObj_X, CategoryTheory.Grp.η_def, CategoryTheory.Comon.monoidal_associator_inv_hom, CategoryTheory.Comon.monoidal_tensorUnit_comon_counit, braiding_hom_hom, CategoryTheory.Comon.monoidal_tensorHom_hom, CategoryTheory.Bimon.trivial_X_mon_mul, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Bimon.comp_hom', CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, hom_one, CategoryTheory.Bimon.toComon_obj_comon_comul, CategoryTheory.Comon.monoidal_tensorObj_comon_comul, CategoryTheory.Bimon.trivial_X_mon_one
monMonoidalStruct 📖	CompOp	18 math math: leftUnitor_inv_hom, rightUnitor_inv_hom, tensorObj_one, whiskerRight_hom, tensorUnit_X, associator_hom_hom, tensorObj_mul, whiskerLeft_hom, associator_inv_hom, tensorUnit_one, leftUnitor_hom_hom, rightUnitor_hom_hom, monMonoidalStruct_tensorHom_hom, CategoryTheory.Grp.tensorHom_hom, tensorUnit_mul, tensor_one, monMonoidalStruct_tensorObj_X, tensor_mul
trivial 📖	CompOp	7 math math: trivial_mon_mul, uniqueHomFromTrivial_default_hom, CategoryTheory.Bimon.trivialTo_hom, trivial_mon_one, EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_map, trivial_X, EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj
uniqueHomFromTrivial 📖	CompOp	2 math math: uniqueHomFromTrivial_default_hom, CategoryTheory.Bimon.trivialTo_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
associator_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
associator_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
braiding_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monMonoidal CategoryTheory.SymmetricCategory.toBraidedCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding instSymmetricCategory X	—	—
braiding_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct monMonoidal CategoryTheory.SymmetricCategory.toBraidedCategory CategoryTheory.Iso.inv CategoryTheory.BraidedCategory.braiding instSymmetricCategory X	—	—
comp_hom 📖	mathematical	—	Hom.hom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X	—	—
comp_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp CategoryTheory.Mon CategoryTheory.Category.toCategoryStruct instCategory X	—	—
equivLaxMonoidalFunctorPUnit_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Mon CategoryTheory.LaxMonoidalFunctor.instCategory instCategory equivLaxMonoidalFunctorPUnit EquivLaxMonoidalFunctorPUnit.counitIso	—	—
equivLaxMonoidalFunctorPUnit_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Mon CategoryTheory.LaxMonoidalFunctor.instCategory instCategory equivLaxMonoidalFunctorPUnit EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon	—	—
equivLaxMonoidalFunctorPUnit_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Mon CategoryTheory.LaxMonoidalFunctor.instCategory instCategory equivLaxMonoidalFunctorPUnit EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal	—	—
equivLaxMonoidalFunctorPUnit_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Mon CategoryTheory.LaxMonoidalFunctor.instCategory instCategory equivLaxMonoidalFunctorPUnit EquivLaxMonoidalFunctorPUnit.unitIso	—	—
forget_faithful 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.Mon instCategory forget	—	Hom.ext'
forget_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Mon instCategory forget Hom.hom	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Mon instCategory forget X	—	—
forget_δ 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.δ CategoryTheory.Mon instCategory monMonoidal 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.Mon instCategory monMonoidal forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_η 📖	mathematical	—	CategoryTheory.Functor.OplaxMonoidal.η CategoryTheory.Mon instCategory monMonoidal forget CategoryTheory.Functor.Monoidal.toOplaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
forget_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Mon instCategory monMonoidal forget CategoryTheory.Functor.Monoidal.toLaxMonoidal instMonoidalForget CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
hom_injective 📖	mathematical	—	Hom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X Hom.hom	—	Hom.ext
id_hom 📖	mathematical	—	Hom.hom id CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
id_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id CategoryTheory.Mon CategoryTheory.Category.toCategoryStruct instCategory X	—	—
instHasInitial 📖	mathematical	—	CategoryTheory.Limits.HasInitial CategoryTheory.Mon instCategory	—	CategoryTheory.Limits.hasInitial_of_unique Unique.instSubsingleton
instIsIsoHom 📖	mathematical	—	CategoryTheory.IsIso X Hom.hom	—	CategoryTheory.Functor.map_isIso
instIsIsoHomOfMapForget 📖	mathematical	—	CategoryTheory.IsIso X Hom.hom	—	—
instIsMonHomHom 📖	mathematical	—	CategoryTheory.IsMonHom X mon Hom.hom	—	Hom.isMonHom_hom
instReflectsIsomorphismsForget 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CategoryTheory.Mon instCategory forget	—	instIsIsoHomOfMapForget CategoryTheory.IsMonHom.one_hom instIsMonHomHom CategoryTheory.Category.assoc CategoryTheory.IsMonHom.mul_hom CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp Hom.ext' CategoryTheory.IsIso.hom_inv_id
leftUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
leftUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
mkIso'_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.hom CategoryTheory.Mon instCategory mkIso'	—	—
mkIso'_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Mon instCategory mkIso'	—	—
mkIso_hom_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one mon CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	Hom.hom CategoryTheory.Mon instCategory mkIso	—	—
mkIso_inv_hom 📖	mathematical	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one mon CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorHom	Hom.hom CategoryTheory.Iso.inv CategoryTheory.Mon instCategory mkIso	—	—
monMonoidalStruct_tensorHom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.MonObj.tensorObj.instTensorObj mon CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Mon instCategory monMonoidalStruct	—	—
monMonoidalStruct_tensorObj_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
mul_def 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonObjTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
one_def 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instMonObjTensorObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
rightUnitor_hom_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
rightUnitor_inv_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.rightUnitor CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
tensorObj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
tensorObj_one 📖	mathematical	—	CategoryTheory.MonObj.one X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
tensorUnit_X 📖	mathematical	—	X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensorUnit_mul 📖	mathematical	—	CategoryTheory.MonObj.mul X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
tensorUnit_one 📖	mathematical	—	CategoryTheory.MonObj.one X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
tensor_mul 📖	mathematical	—	CategoryTheory.MonObj.mul X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
tensor_one 📖	mathematical	—	CategoryTheory.MonObj.one X CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom	—	—
trivial_X 📖	mathematical	—	X trivial CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	—
trivial_mon_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct mon trivial CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
trivial_mon_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct mon trivial CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
uniqueHomFromTrivial_default_hom 📖	mathematical	—	Hom.hom trivial Quiver.Hom CategoryTheory.Mon CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory Unique.toInhabited uniqueHomFromTrivial CategoryTheory.MonObj.one X mon	—	—
whiskerLeft_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—
whiskerRight_hom 📖	mathematical	—	Hom.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Mon instCategory monMonoidalStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X	—	—

CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	3 math math: CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_counitIso, counitIso_inv_app_hom, counitIso_hom_app_hom
counitIsoAux 📖	CompOp	4 math math: isMonHom_counitIsoAux, counitIsoAux_inv, counitIsoAux_hom, counitIsoAux_IsMon_Hom
instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj 📖	CompOp	4 math math: monToLaxMonoidal_map_hom_app, monToLaxMonoidal_obj, monToLaxMonoidalObj_μ, monToLaxMonoidalObj_ε
laxMonoidalToMon 📖	CompOp	13 math math: isMonHom_counitIsoAux, monToLaxMonoidal_laxMonoidalToMon_obj_one, unitIso_hom_app_hom_app, counitIso_inv_app_hom, counitIsoAux_inv, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_functor, counitIso_hom_app_hom, counitIsoAux_hom, counitIsoAux_IsMon_Hom, laxMonoidalToMon_map, monToLaxMonoidal_laxMonoidalToMon_obj_mul, laxMonoidalToMon_obj, unitIso_inv_app_hom_app
monToLaxMonoidal 📖	CompOp	13 math math: isMonHom_counitIsoAux, CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_inverse, monToLaxMonoidal_map_hom_app, monToLaxMonoidal_laxMonoidalToMon_obj_one, monToLaxMonoidal_obj, unitIso_hom_app_hom_app, counitIso_inv_app_hom, counitIsoAux_inv, counitIso_hom_app_hom, counitIsoAux_hom, counitIsoAux_IsMon_Hom, monToLaxMonoidal_laxMonoidalToMon_obj_mul, unitIso_inv_app_hom_app
monToLaxMonoidalObj 📖	CompOp	6 math math: monToLaxMonoidal_map_hom_app, monToLaxMonoidalObj_obj, monToLaxMonoidal_obj, monToLaxMonoidalObj_map, monToLaxMonoidalObj_μ, monToLaxMonoidalObj_ε
unitIso 📖	CompOp	3 math math: CategoryTheory.Mon.equivLaxMonoidalFunctorPUnit_unitIso, unitIso_hom_app_hom_app, unitIso_inv_app_hom_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIsoAux_IsMon_Hom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Functor.id CategoryTheory.Mon.mon CategoryTheory.Iso.hom counitIsoAux	—	isMonHom_counitIsoAux
counitIsoAux_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Functor.id counitIsoAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
counitIsoAux_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Functor.id counitIsoAux CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
counitIso_hom_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
counitIso_inv_app_hom 📖	mathematical	—	CategoryTheory.Mon.Hom.hom CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
isMonHom_counitIsoAux 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Functor.id CategoryTheory.Mon.mon CategoryTheory.Iso.hom counitIsoAux	—	CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp
laxMonoidalToMon_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory laxMonoidalToMon CategoryTheory.NatTrans.app CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.mapMonFunctor CategoryTheory.Mon.trivial	—	—
laxMonoidalToMon_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Mon CategoryTheory.Mon.instCategory laxMonoidalToMon CategoryTheory.Functor.mapMon CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.LaxMonoidalFunctor.laxMonoidal CategoryTheory.Mon.trivial	—	—
monToLaxMonoidalObj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Discrete CategoryTheory.discreteCategory monToLaxMonoidalObj CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Mon.X	—	—
monToLaxMonoidalObj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Discrete CategoryTheory.discreteCategory monToLaxMonoidalObj CategoryTheory.Mon.X	—	—
monToLaxMonoidalObj_ε 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup monToLaxMonoidalObj instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj CategoryTheory.MonObj.one CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
monToLaxMonoidalObj_μ 📖	mathematical	—	CategoryTheory.Functor.LaxMonoidal.μ CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup monToLaxMonoidalObj instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
monToLaxMonoidal_laxMonoidalToMon_obj_mul 📖	mathematical	—	CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
monToLaxMonoidal_laxMonoidalToMon_obj_one 📖	mathematical	—	CategoryTheory.MonObj.one CategoryTheory.Mon.X CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.Functor.comp CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal laxMonoidalToMon CategoryTheory.Mon.mon CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.CategoryStruct.id	—	—
monToLaxMonoidal_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.of monToLaxMonoidalObj instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.Functor.map CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal CategoryTheory.Mon.Hom.hom	—	—
monToLaxMonoidal_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Mon CategoryTheory.Mon.instCategory CategoryTheory.LaxMonoidalFunctor CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.LaxMonoidalFunctor.instCategory monToLaxMonoidal CategoryTheory.LaxMonoidalFunctor.of monToLaxMonoidalObj instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj	—	—
unitIso_hom_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Functor.obj CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Functor.id CategoryTheory.Functor.comp CategoryTheory.Mon CategoryTheory.Mon.instCategory laxMonoidalToMon monToLaxMonoidal CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Discrete.functor_map_id
unitIso_inv_app_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.LaxMonoidalFunctor.toFunctor CategoryTheory.Discrete.addMonoidal SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup PUnit.addCommGroup CategoryTheory.Functor.obj CategoryTheory.LaxMonoidalFunctor CategoryTheory.LaxMonoidalFunctor.instCategory CategoryTheory.Functor.comp CategoryTheory.Mon CategoryTheory.Mon.instCategory laxMonoidalToMon monToLaxMonoidal CategoryTheory.Functor.id CategoryTheory.LaxMonoidalFunctor.Hom.hom CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct	—	CategoryTheory.Discrete.functor_map_id

CategoryTheory.Mon.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	204 math math: CategoryTheory.Grp.mkIso_inv_hom, CategoryTheory.Grp.Hom.hom_div, CategoryTheory.Grp.mkIso_hom_hom, CategoryTheory.Mon.id_hom, CategoryTheory.Grp.instIsIsoHomHomMon, CategoryTheory.Bimon.Bimon_ClassAux_comul, CategoryTheory.Functor.mapMonNatTrans_app_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom, CategoryTheory.Functor.FullyFaithful.mapMon_preimage_hom, CategoryTheory.CommMon.comp_hom, CategoryTheory.Grp.Hom.hom_hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom, CategoryTheory.Functor.mapCommMonNatIso_inv_app_hom_hom, CategoryTheory.Mon.leftUnitor_inv_hom, commBialgCatEquivComonCommAlgCat_unitIso_inv_app, CategoryTheory.Bimon.ext_iff, CategoryTheory.CommMon.forget_map, CategoryTheory.Mon.hom_injective, CategoryTheory.CommGrp.mkIso_inv_hom, CategoryTheory.Mon.instIsMonHomHom, CategoryTheory.Grp.whiskerLeft_hom_hom, CategoryTheory.Functor.mapGrpIdIso_hom_app_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_inv_app_app_hom_hom, CategoryTheory.Grp.leftUnitor_hom_hom, CategoryTheory.Functor.mapCommMonNatTrans_app_hom_hom, CategoryTheory.Monad.monadMonEquiv_counitIso_hom_app_hom, CategoryTheory.Bimon.trivial_comon_counit_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom, CategoryTheory.Mon.rightUnitor_inv_hom, CategoryTheory.CommMon.mkIso'_inv_hom_hom, CategoryTheory.Grp.rightUnitor_hom_hom_hom, CategoryTheory.Bimon.toComon_obj_comon_counit, CategoryTheory.Mon.mkIso_hom_hom, CategoryTheory.Bimon.toComon_map_hom, CategoryTheory.Grp.hom_mul, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_map_hom_app, CategoryTheory.Functor.mapMonCompIso_hom_app_hom, CategoryTheory.Mon.limitConeIsLimit_lift_hom, CategoryTheory.Grp.Hom.hom_zpow, CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_inv_app_hom_hom_app, CategoryTheory.Bimon.trivial_comon_comul_hom, CategoryTheory.Comon.MonOpOpToComon_map_hom, CategoryTheory.Grp.associator_inv_hom_hom, CategoryTheory.Functor.mapCommMonNatIso_hom_app_hom_hom, CategoryTheory.Grp.Hom.hom_hom_div, CategoryTheory.Grp.leftUnitor_hom_hom_hom, CategoryTheory.Grp.forget_map, CategoryTheory.Mon.lift_hom, CategoryTheory.Mon.whiskerRight_hom, CategoryTheory.Grp.mkIso_hom_hom_hom, CategoryTheory.CommMon.instIsIsoHomHomMon, CategoryTheory.Grp.rightUnitor_inv_hom_hom, CategoryTheory.Grp.forget₂Mon_map_hom, CategoryTheory.Grp.whiskerRight_hom_hom, CategoryTheory.Functor.mapMonNatIso_hom_app_hom, CategoryTheory.Grp.Hom.hom_hom_inv, CategoryTheory.Preadditive.commGrpEquivalenceAux_hom_app_hom_hom_hom, ext'_iff, CategoryTheory.Mon.fst_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided_map_hom_hom_app, CategoryTheory.Functor.mapMonNatIso_inv_app_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.unitIso_hom_app_hom_hom_app, CategoryTheory.Grp.snd_hom, CategoryTheory.Monad.monadToMon_map_hom, CategoryTheory.Mon.mkIso_inv_hom, CategoryTheory.Bimon.Bimon_ClassAux_counit, CategoryTheory.Grp.whiskerLeft_hom, CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom, CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom, CategoryTheory.Functor.mapCommMonCompIso_inv_app_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_hom_app_hom_hom, CategoryTheory.Grp.leftUnitor_inv_hom_hom, CategoryTheory.yonedaMon_map_app, CategoryTheory.Mon.associator_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.functor_map_hom_apply, CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom, MonObj.mopEquiv_inverse_map_hom, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Grp.rightUnitor_inv_hom, CategoryTheory.Functor.mapMonFunctor_map_app_hom, CategoryTheory.Functor.mapMonIdIso_hom_app_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_map_hom_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor_map_app_hom, CategoryTheory.CommGrp.hom_ext_iff, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse_map_hom_app, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.counitIso_hom_app_app_hom_hom, CategoryTheory.Mon.whiskerLeft_hom, CategoryTheory.Grp.associator_hom_hom_hom, CategoryTheory.CommMon.mkIso_inv_hom_hom, CategoryTheory.Mon.limitCone_π_app_hom, CategoryTheory.Grp.braiding_inv_hom, CategoryTheory.Grp.mkIso'_hom_hom_hom, CategoryTheory.Grp.id_hom, CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom, CategoryTheory.Grp.fst_hom, MonObj.mopEquiv_counitIso_hom_app_hom_unmop, CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom, CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_inv_app_hom, hom_mul, CategoryTheory.Mon.associator_inv_hom, CategoryTheory.Monad.monToMonad_map_toNatTrans, CategoryTheory.Mon.mkIso'_inv_hom, CategoryTheory.Mon.uniqueHomFromTrivial_default_hom, MonObj.mopEquiv_functor_map_hom_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObj_map_hom, ext_iff, CategoryTheory.Functor.mapCommMon_map_hom_hom, CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_map_hom_hom_app, CategoryTheory.Preadditive.commGrpEquivalenceAux_inv_app_hom_hom_hom, CategoryTheory.Functor.mapGrp_map_hom_hom, CategoryTheory.Grp.comp_hom_hom, CategoryTheory.Functor.mapMonIdIso_inv_app_hom, CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom, MonObj.mopEquiv_unitIso_hom_app_hom, CategoryTheory.Grp.braiding_inv_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom, CategoryTheory.CommGrp.mkIso_hom_hom, hom_pow, CategoryTheory.Grp.rightUnitor_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_inv_app_hom_hom_hom, CategoryTheory.Grp.hom_ext_iff, CategoryTheory.Grp.homMk''_hom_hom, CategoryTheory.CommMon.id_hom, CategoryTheory.Functor.mapMon_map_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_X_map, CategoryTheory.Mon.leftUnitor_hom_hom, CategoryTheory.Functor.mapGrpIdIso_inv_app_hom_hom, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom, CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom, CategoryTheory.Grp.leftUnitor_inv_hom, CategoryTheory.CommMon.mkIso_hom_hom_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom, CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.Functor.mapMonCompIso_inv_app_hom, CategoryTheory.CommMon.hom_ext_iff, CategoryTheory.Grp.mkIso_inv_hom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom, CategoryTheory.Grp.snd_hom_hom, CategoryTheory.Functor.mapGrpNatTrans_app_hom_hom, CategoryTheory.Grp.hom_one, CategoryTheory.Preadditive.commGrpEquivalence_counitIso_hom_app_hom_hom_hom, CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom, CategoryTheory.Mon.comp_hom', CategoryTheory.Grp.associator_inv_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_inv_app_app_hom, CategoryTheory.Mon.braiding_inv_hom, CategoryTheory.Grp.homMk_hom_hom, CategoryTheory.Monad.monadMonEquiv_counitIso_inv_app_hom, MonObj.mopEquiv_counitIso_inv_app_hom_unmop, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_inv_app_hom_app, CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom, CategoryTheory.Mon.hom_mul, CategoryTheory.Mon.comp_hom, CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom, CategoryTheory.Grp.Hom.hom_inv, CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom, commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom, CategoryTheory.Mon.rightUnitor_hom_hom, CategoryTheory.Grp.braiding_hom_hom, CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom, CategoryTheory.Bimon.toMonComon_map_hom, CategoryTheory.Grp.associator_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_inverse_map, CategoryTheory.Mon.forget_map, CategoryTheory.Mon.instIsIsoHom, CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom, CategoryTheory.Functor.mapCommMonIdIso_inv_app_hom_hom, isMonHom_hom, MonObj.mopEquiv_unitIso_inv_app_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_inv_app_hom_hom, ModuleCat.MonModuleEquivalenceAlgebra.inverse_map_hom, CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom, CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom, CategoryTheory.Grp.whiskerRight_hom, CategoryTheory.Mon.instIsIsoHomOfMapForget, CategoryTheory.Mon.braiding_hom_hom, CategoryTheory.CommMon.mkIso'_hom_hom_hom, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, CategoryTheory.Grp.fst_hom_hom, CategoryTheory.Grp.mkIso'_inv_hom_hom, commBialgCatEquivComonCommAlgCat_functor_map_unop_hom, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_hom_app_hom_hom, CategoryTheory.Preadditive.commGrpEquivalence_functor_map_hom_hom_hom, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app, CategoryTheory.Grp.braiding_hom_hom_hom, CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom, CategoryTheory.CommMon.forget₂Mon_map_hom, CategoryTheory.Mon.hom_one, commBialgCatEquivComonCommAlgCat_counitIso_inv_app, CategoryTheory.Mon.mkIso'_hom_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_map_app_hom_hom, CategoryTheory.Grp.comp_hom, CategoryTheory.Mon.id_hom', CategoryTheory.Grp.id_hom_hom, CategoryTheory.Bimon.toComon_obj_comon_comul, CategoryTheory.Mon.snd_hom, hom_one, CategoryTheory.CommGrp.forget_map, CategoryTheory.Functor.mapCommMonCompIso_hom_app_hom_hom
mk' 📖	CompOp	5 math math: commBialgCatEquivComonCommAlgCat_unitIso_inv_app, commBialgCatEquivComonCommAlgCat_unitIso_hom_app, CategoryTheory.Functor.mapCommMonFunctor_map_app, commBialgCatEquivComonCommAlgCat_counitIso_hom_app, commBialgCatEquivComonCommAlgCat_counitIso_inv_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom	—	—	—
ext' 📖	—	hom	—	—	ext
ext'_iff 📖	mathematical	—	hom	—	ext'
ext_iff 📖	mathematical	—	hom	—	ext
isMonHom_hom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.Mon.X CategoryTheory.Mon.mon hom	—	—

CategoryTheory.MonObj

Definitions

Name	Category	Theorems
instTensorUnit 📖	CompOp	11 math math: CategoryTheory.IsCommMonObj.instTensorUnit, instIsMonHomOne, instIsMonHomToUnit, mul_def, one_def, instIsMonHomHomLeftUnitor, CategoryTheory.Grp.tensorUnit_mul, CategoryTheory.Grp.tensorUnit_one, instIsMonHomHomRightUnitor, CategoryTheory.Functor.instIsMonHomε, CategoryTheory.ModObj.smul_def
mul 📖	CompOp	178 math math: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.Bimon.toMonComonObj_mon_mul_hom, CategoryTheory.Functor.mapCommMon_obj_mon_mul, CategoryTheory.ModObj.mul_smul_assoc, CategoryTheory.Bimon.ofMonComonObjX_mul, CategoryTheory.Monad.mul_def, CategoryTheory.GrpObj.lift_inv_right_eq, mul_assoc, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, ofIso_mul, CategoryTheory.Functor.mapMon_obj_mon_mul, CategoryTheory.Over.monObjMkPullbackSnd_mul, CategoryTheory.Functor.comp_mapGrp_mul, Bimod.TensorBimod.right_assoc', CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul, CategoryTheory.GrpObj.left_inv_assoc, CategoryTheory.Functor.mapGrp_id_mul, CategoryTheory.Over.grpObjMkPullbackSnd_mul, CategoryTheory.Functor.FullyFaithful.monObj_mul, lift_comp_one_right, Bimod.left_assoc_assoc, Bimod.right_assoc, CategoryTheory.GrpObj.lift_inv_comp_right, CategoryTheory.HopfObj.mul_antipode, CategoryTheory.Grp.hom_mul, lift_lift_assoc, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_mul, mul_leftUnitor, lift_comp_one_right_assoc, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_mul_app, CategoryTheory.Bimon.compatibility_assoc, CategoryTheory.ModObj.mul_smul'_assoc, CategoryTheory.BimonObj.mul_counit_assoc, CategoryTheory.Mon.trivial_mon_mul, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_mul, CategoryTheory.CommGrp.forget₂Grp_obj_mul, mul_def, mul_mul_mul_comm'_assoc, one_mul_assoc, CategoryTheory.HopfObj.antipode_left, CategoryTheory.GrpObj.tensorHom_inv_inv_mul_assoc, CategoryTheory.Mon.limit_mon_mul, CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom, ext_iff, CommAlgCat.mul_op_of_unop_hom, mul_mul_mul_comm, CategoryTheory.Hom.mul_def, Bimod.right_assoc_assoc, tensorObj.mul_def, lift_comp_one_left, CategoryTheory.Grp.tensorUnit_mul, CategoryTheory.Bimon.ofMon_Comon_ObjX_mul, CategoryTheory.Mon_Class.mul_eq_mul, CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv, CategoryTheory.Functor.comp_mapMon_mul, CategoryTheory.HopfObj.antipode_comul₂, CategoryTheory.IsMonHom.mul_hom, CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc, CategoryTheory.BimonObj.mul_comul_assoc, CategoryTheory.Functor.comp_mapCommMon_mul, CategoryTheory.Comon.MonOpOpToComonObj_comon_comul, CategoryTheory.HopfObj.antipode_left_assoc, CategoryTheory.ModObj.smul_eq_mul, mul_one, CategoryTheory.Grp.forget₂Mon_obj_mul, CategoryTheory.Mon.tensorObj_mul, CategoryTheory.GrpObj.lift_inv_left_eq, CategoryTheory.Functor.comp_mapCommGrp_mul, Mon_tensor_mul_one, CategoryTheory.BimonObj.mul_counit, Mon_tensor_one_mul, CategoryTheory.Functor.mapCommMon_id_mul, CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_μ, CategoryTheory.CommMon.forget₂Mon_obj_mul, CategoryTheory.Conv.mul_eq, CategoryTheory.GrpObj.isPullback, CategoryTheory.Functor.obj.μ_def, AlgebraicGeometry.Scheme.monObjAsOverPullback_mul, Mon_tensor_mul_assoc, CategoryTheory.IsCommMonObj.mul_comm'_assoc, mul_mul_mul_comm', CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.CommGrp.forget₂CommMon_obj_mul, Bimod.TensorBimod.left_assoc', CategoryTheory.GrpObj.eq_lift_inv_right, mul_mul_mul_comm_assoc, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_mul, ofRepresentableBy_mul, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ, CategoryTheory.GrpObj.left_inv, CategoryTheory.Bimon.mul_counit, CategoryTheory.ModObj.assoc_flip, CategoryTheory.HopfObj.antipode_right_assoc, CategoryTheory.GrpObj.mul_inv_rev_assoc, CategoryTheory.Grp.tensorObj_mul, Bimod.left_assoc, Bimod.regular_actRight, CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul, CategoryTheory.GrpObj.tensorHom_inv_inv_mul, mul_associator, CategoryTheory.GrpObj.mul_inv, CategoryTheory.IsCommMonObj.mul_comm, CategoryTheory.Functor.obj.μ_def_assoc, CategoryTheory.Mon.mul_def, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_mul, MonObj.unmopMonObj_mul, CategoryTheory.Functor.id_mapMon_mul, mul_braiding, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul, CategoryTheory.Functor.mapGrp_obj_grp_mul, CategoryTheory.Functor.mapCommpGrp_id_mul, MonObj.mopEquiv_functor_obj_mon_mul_unmop, CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv_assoc, CategoryTheory.Monad.ofMon_μ, CategoryTheory.GrpObj.mul_inv_rev, CategoryTheory.GrpObj.mulRight_hom, CategoryTheory.CommMon.trivial_mon_mul, CategoryTheory.Preadditive.mul_def, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, CategoryTheory.Mod_.regular_mod_smul, CategoryTheory.HopfObj.antipode_comul₁, CategoryTheory.Functor.FullyFaithful.grpObj_mul, CategoryTheory.GrpObj.mulRight_inv, CategoryTheory.Comon.ComonToMonOpOpObj_mon_mul, CategoryTheory.GrpObj.mul_inv_assoc, CategoryTheory.IsCommMonObj.mul_comm_assoc, CategoryTheory.Mon.hom_mul, CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.GrpObj.eq_lift_inv_left, lift_comp_one_left_assoc, CategoryTheory.HopfObj.mul_antipode₂, mul_assoc_assoc, CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom_assoc, CategoryTheory.IsCommMonObj.mul_comm', CommGrpTypeEquivalenceCommGrp.inverse_obj_mul, mul_one_assoc, mul_assoc_flip_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_mul_app, CategoryTheory.CommGrp.trivial_grp_mul, CategoryTheory.Mod_.assoc_flip, CategoryTheory.BimonObj.mul_comul, CategoryTheory.IsMonHom.mul_hom_assoc, Bimod.regular_actLeft, CategoryTheory.GrpObj.ofIso_mul, CategoryTheory.GrpObj.lift_comp_inv_right, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul, CategoryTheory.Bimon.mul_counit_assoc, CategoryTheory.ModObj.mul_smul, CategoryTheory.Functor.mapCommGrp_obj_grp_mul, MonObj.mopMonObj_mul_unmop, CategoryTheory.ModObj.mul_smul', CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_mul, one_mul, mul_rightUnitor, CategoryTheory.Bimon.trivial_X_mon_mul, CategoryTheory.HopfObj.antipode_right, mul_one_hom, CategoryTheory.Grp.trivial_grp_mul, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_mul, CategoryTheory.Bimon.compatibility, CategoryTheory.GrpObj.right_inv_assoc, CategoryTheory.Mon.tensorUnit_mul, CategoryTheory.Bimon.Mon_Class.tensorObj.mul_def, instIsMonHomMulOfIsCommMonObj, one_mul_hom, mul_eq_mul, CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, CategoryTheory.Mon_Class.mul_mul_mul_comm', CategoryTheory.Mon_Class.mul_mul_mul_comm, CategoryTheory.Comon.monoidal_tensorObj_comon_comul, CategoryTheory.Mon.tensor_mul, mul_assoc_flip, MonObj.mopEquiv_inverse_obj_mon_mul
ofIso 📖	CompOp	3 math math: ofIso_mul, ofIso_one, CategoryTheory.isMonHom_ofIso
one 📖	CompOp	147 math math: CategoryTheory.GrpObj.lift_inv_comp_left, CategoryTheory.ModObj.one_smul_assoc, CategoryTheory.Preadditive.commGrpEquivalence_functor_obj_grp_one, CategoryTheory.Monad.ofMon_η, CategoryTheory.Functor.mapCommGrp_obj_grp_one, CategoryTheory.BimonObj.one_comul, CategoryTheory.GrpObj.lift_inv_comp_left_assoc, CommGrpTypeEquivalenceCommGrp.inverse_obj_one, CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul, CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one, CategoryTheory.GrpObj.left_inv_assoc, instIsMonHomOne, CategoryTheory.Over.grpObjMkPullbackSnd_one, ofIso_one, lift_comp_one_right, Bimod.actRight_one, ofRepresentableBy_one, CategoryTheory.GrpObj.lift_inv_comp_right, Bimod.TensorBimod.actRight_one', lift_comp_one_right_assoc, CategoryTheory.GrpObj.one_inv_assoc, CategoryTheory.Functor.mapGrp_obj_grp_one, CategoryTheory.Functor.mapGrp_id_one, CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc, CategoryTheory.GrpObj.lift_comp_inv_right_assoc, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one, AlgebraicGeometry.instIsClosedImmersionLeftSchemeDiscretePUnitOneOverSpecOf, MonObj.mopEquiv_functor_obj_mon_one_unmop, MonObj.unmopMonObj_one, CategoryTheory.HopfObj.one_antipode, CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η, CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_inv_one_tensor_mul_assoc, CategoryTheory.Mon.tensorObj_one, one_def, one_mul_assoc, CategoryTheory.Bimon.ofMon_Comon_ObjX_one, CategoryTheory.HopfObj.antipode_left, CategoryTheory.IsMonHom.one_hom_assoc, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.inverse_obj_mon_one_app, CategoryTheory.ModObj.one_smul'_assoc, CategoryTheory.Functor.obj.η_def_assoc, lift_comp_one_left, CategoryTheory.Functor.obj.η_def, CategoryTheory.CommGrp.trivial_grp_one, CategoryTheory.Bimon.one_comul, CategoryTheory.GrpObj.one_inv, CategoryTheory.GrpObj.mulRight_one, CategoryTheory.HopfObj.antipode_comul₂, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_one, CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul_assoc, tensorObj.one_def, CategoryTheory.HopfObj.antipode_left_assoc, CategoryTheory.Functor.mapMon_obj_mon_one, Bimod.one_actLeft_assoc, mul_one, CategoryTheory.Mon_Class.one_eq_one, CategoryTheory.GrpObj.whiskerLeft_η_commutator, CategoryTheory.BimonObj.one_counit_assoc, Mon_tensor_mul_one, CategoryTheory.BimonObj.one_comul_assoc, Mon_tensor_one_mul, CategoryTheory.IsMonHom.one_hom, CategoryTheory.Conv.one_eq, CategoryTheory.Grp.tensorUnit_one, CategoryTheory.Functor.FullyFaithful.monObj_one, CategoryTheory.Mathlib.Tactic.MonTauto.eq_mul_one, CategoryTheory.Over.monObjMkPullbackSnd_one, CategoryTheory.CommGrp.forget₂Grp_obj_one, CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc, CategoryTheory.ModObj.one_smul', one_leftUnitor, CategoryTheory.Mon.uniqueHomFromTrivial_default_hom, one_braiding, CategoryTheory.Functor.mapCommGrp_id_one, ModuleCat.MonModuleEquivalenceAlgebra.algebraMap, Bimod.one_actLeft, CategoryTheory.HopfObj.mul_antipode₁, CategoryTheory.Mon.trivial_mon_one, CategoryTheory.Functor.mapCommMon_obj_mon_one, CategoryTheory.GrpObj.left_inv, CategoryTheory.Mon.tensorUnit_one, CategoryTheory.HopfObj.antipode_right_assoc, CategoryTheory.CommMon.trivial_mon_one, CommAlgCat.one_op_of_unop_hom, CategoryTheory.BimonObj.one_counit, CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_inv_tensor_one_mul, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one, CategoryTheory.Bimon.ofMonComonObjX_one, CategoryTheory.Grp.tensorObj_one, one_associator, CategoryTheory.Bimon.toMonComonObj_mon_one_hom, CategoryTheory.ModObj.one_smul, CategoryTheory.CommGrp.forget₂CommMon_obj_one, CategoryTheory.Grp.trivial_grp_one, CategoryTheory.Bimon.one_comul_assoc, CategoryTheory.GrpObj.lift_comp_inv_left_assoc, CategoryTheory.Functor.comp_mapCommGrp_one, CategoryTheory.Grp.hom_one, CategoryTheory.Grp.forget₂Mon_obj_one, Bimod.actRight_one_assoc, CategoryTheory.Hom.one_def, CategoryTheory.HopfObj.antipode_comul₁, CategoryTheory.GrpObj.η_whiskerRight_commutator, MonObj.mopMonObj_one_unmop, Bimod.TensorBimod.one_act_left', CategoryTheory.GrpObj.right_inv, CategoryTheory.GrpObj.lift_comp_inv_left, CategoryTheory.Mon.limit_mon_one, lift_comp_one_left_assoc, CategoryTheory.HopfObj.mul_antipode₂, MonObj.mopEquiv_inverse_obj_mon_one, mul_one_assoc, CategoryTheory.Functor.FullyFaithful.grpObj_one, one_rightUnitor, CategoryTheory.Mon.one_def, CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverseObj_mon_one_app, CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_ε, CategoryTheory.Preadditive.one_def, AlgebraicGeometry.Scheme.monObjAsOverPullback_one, CategoryTheory.GrpObj.lift_comp_inv_right, one_eq_one, CategoryTheory.Functor.mapCommMon_id_one, CategoryTheory.Monad.one_def, CategoryTheory.GrpObj.ofIso_one, one_mul, CategoryTheory.Functor.id_mapMon_one, CategoryTheory.HopfObj.antipode_right, mul_one_hom, CategoryTheory.Comon.MonOpOpToComonObj_comon_counit, CategoryTheory.GrpObj.right_inv_assoc, CategoryTheory.Bimon.toMon_Comon_ofMon_Comon_obj_one, CategoryTheory.Comon.monoidal_tensorObj_comon_counit, CategoryTheory.Mon.tensor_one, CategoryTheory.Mon.hom_one, ModuleCat.MonModuleEquivalenceAlgebra.inverseObj_one, CategoryTheory.HopfObj.one_antipode_assoc, CategoryTheory.Functor.comp_mapMon_one, one_mul_hom, CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor_obj_obj_mon_one, CategoryTheory.CommMon.forget₂Mon_obj_one, CategoryTheory.Mathlib.Tactic.MonTauto.eq_one_mul, CategoryTheory.GrpObj.lift_inv_comp_right_assoc, CategoryTheory.Functor.comp_mapCommMon_one, CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj_ε, CategoryTheory.Functor.comp_mapGrp_one, CategoryTheory.Bimon.trivial_X_mon_one, CategoryTheory.Comon.ComonToMonOpOpObj_mon_one
termη 📖	CompOp	—
termμ 📖	CompOp	—
«termη[_]» 📖	CompOp	—
«termμ[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Mon_tensor_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorμ_natural_left CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom mul_assoc CategoryTheory.MonoidalCategory.tensor_associativity CategoryTheory.MonoidalCategory.tensorμ_natural_right CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc
Mon_tensor_mul_one 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom one CategoryTheory.MonoidalCategory.tensorμ mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorμ_natural_right CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom mul_one CategoryTheory.MonoidalCategory.tensor_right_unitality
Mon_tensor_one_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom one CategoryTheory.MonoidalCategory.tensorμ mul CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorμ_natural_left CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom one_mul CategoryTheory.MonoidalCategory.tensor_left_unitality
ext 📖	—	mul	—	—	CategoryTheory.MonoidalCategory.tensorHom_def CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Category.assoc mul_one CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.tensorHom_def' CategoryTheory.MonoidalCategory.id_whiskerLeft one_mul
ext_iff 📖	mathematical	—	mul	—	ext
instIsMonHomHomAssociator 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj.instTensorObj CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	one_associator mul_associator
instIsMonHomHomBraiding 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.instMonObjTensorObj CategoryTheory.SymmetricCategory.toBraidedCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	one_braiding mul_braiding
instIsMonHomHomLeftUnitor 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit tensorObj.instTensorObj instTensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	one_leftUnitor mul_leftUnitor
instIsMonHomHomRightUnitor 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit tensorObj.instTensorObj instTensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	one_rightUnitor mul_rightUnitor
instIsMonHomId 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Category.id_comp
instIsMonHomTensorHom 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj.instTensorObj CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.IsMonHom.one_hom CategoryTheory.MonoidalCategory.tensorμ_natural CategoryTheory.IsMonHom.mul_hom
instIsMonHomWhiskerLeft 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj.instTensorObj CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.IsMonHom.one_hom instIsMonHomTensorHom instIsMonHomId CategoryTheory.IsMonHom.mul_hom
instIsMonHomWhiskerRight 📖	mathematical	—	CategoryTheory.IsMonHom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct tensorObj.instTensorObj CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.IsMonHom.one_hom instIsMonHomTensorHom instIsMonHomId CategoryTheory.IsMonHom.mul_hom
mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
mul_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_assoc
mul_assoc_flip 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft mul CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	mul_assoc CategoryTheory.Iso.inv_hom_id_assoc
mul_assoc_flip_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft mul CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_assoc_flip
mul_associator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.MonoidalCategory.associator_naturality CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.associator_monoidal
mul_braiding 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct mul CategoryTheory.Mon.instMonObjTensorObj CategoryTheory.SymmetricCategory.toBraidedCategory CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding CategoryTheory.MonoidalCategoryStruct.tensorHom	—	CategoryTheory.Category.assoc CategoryTheory.BraidedCategory.braiding_naturality CategoryTheory.BraidedCategory.braiding_tensor_right_hom CategoryTheory.BraidedCategory.braiding_tensor_left_hom CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.pentagon_assoc CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.whiskerLeft_hom_inv_assoc CategoryTheory.SymmetricCategory.symmetry CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.pentagon_inv_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.Iso.inv_hom_id CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.tensorHom_def
mul_def 📖	mathematical	—	mul CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
mul_leftUnitor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor mul	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.leftUnitor_naturality CategoryTheory.MonoidalCategory.leftUnitor_monoidal
mul_mul_mul_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom mul	—	CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom CategoryTheory.MonoidalCategory.id_tensorHom_id CategoryTheory.Category.id_comp CategoryTheory.IsCommMonObj.mul_comm CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc
mul_mul_mul_comm' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.MonoidalCategoryStruct.tensorHom mul	—	CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_inv CategoryTheory.Mathlib.Tactic.MonTauto.mul_assoc_hom CategoryTheory.MonoidalCategory.id_tensorHom_id CategoryTheory.Category.id_comp CategoryTheory.IsCommMonObj.mul_comm' CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp_assoc
mul_mul_mul_comm'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorδ CategoryTheory.MonoidalCategoryStruct.tensorHom mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_mul_mul_comm'
mul_mul_mul_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom mul	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_mul_mul_comm
mul_one 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
mul_one_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerLeft one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' mul_one
mul_one_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.MonoidalCategory.tensorHom_def_assoc mul_one CategoryTheory.MonoidalCategory.rightUnitor_naturality
mul_rightUnitor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.tensorμ CategoryTheory.MonoidalCategoryStruct.tensorHom mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.rightUnitor_naturality CategoryTheory.MonoidalCategory.rightUnitor_monoidal
ofIso_mul 📖	mathematical	—	mul ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	—
ofIso_one 📖	mathematical	—	one ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Iso.hom	—	—
one_associator 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom one CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom CategoryTheory.MonoidalCategory.associator_naturality CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.id_tensorHom
one_braiding 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj one tensorObj.instTensorObj CategoryTheory.Iso.hom CategoryTheory.BraidedCategory.braiding	—	CategoryTheory.Category.assoc CategoryTheory.BraidedCategory.braiding_naturality CategoryTheory.braiding_tensorUnit_right Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_tensorHom Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_cons Mathlib.Tactic.Monoidal.evalHorizontalCompAux_of Mathlib.Tactic.Monoidal.evalHorizontalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_tensorHom Mathlib.Tactic.Monoidal.naturality_id
one_def 📖	mathematical	—	one CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct instTensorUnit CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
one_leftUnitor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.CategoryStruct.id one CategoryTheory.Iso.hom	—	CategoryTheory.MonoidalCategory.id_tensorHom CategoryTheory.MonoidalCategory.id_whiskerLeft CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
one_mul 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
one_mul_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.whiskerRight one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_mul
one_mul_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategoryStruct.tensorHom one mul CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.MonoidalCategory.tensorHom_def'_assoc one_mul CategoryTheory.MonoidalCategory.leftUnitor_naturality
one_rightUnitor 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.leftUnitor CategoryTheory.MonoidalCategoryStruct.tensorHom one CategoryTheory.CategoryStruct.id CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.MonoidalCategory.tensorHom_id CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id

CategoryTheory.MonObj.tensorObj

Definitions

Name	Category	Theorems
instTensorObj 📖	CompOp	11 math math: CategoryTheory.MonObj.instIsMonHomHomAssociator, CategoryTheory.MonObj.instIsMonHomTensorHom, mul_def, CategoryTheory.MonObj.instIsMonHomHomLeftUnitor, one_def, CategoryTheory.MonObj.instIsMonHomHomRightUnitor, CategoryTheory.MonObj.one_braiding, CategoryTheory.MonObj.instIsMonHomWhiskerLeft, CategoryTheory.MonObj.instIsMonHomWhiskerRight, CategoryTheory.Mon.monMonoidalStruct_tensorHom_hom, CategoryTheory.Bimon.Mon_Class.tensorObj.mul_def

Theorems

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

CategoryTheory.Mon_Class

Theorems

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

---

← Back to Index