MonCat

📁 Source: MathlibTest/MonCat.lean

Statistics

Metric	Count
Definitions MonCat	1
Theorems	0
Total	1

(root)

Definitions

Name	Category	Theorems
MonCat 📖	CompData	92 math math: CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier, CommMonCat.forget₂_full, MonCat.FilteredColimits.colimit_mul_mk_eq', CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon, MonCat.forget_map, MonCat.forget_reflects_isos, AddMonCat.equivalence_functor_obj_coe, CommMonCat.coe_forget₂_obj, MonCat.ext_iff, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply, MonCat.forget_preservesLimitsOfSize, CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply, MonCat.forget_preservesLimitsOfShape, CategoryTheory.MonObj.ofRepresentableBy_one, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk, MonCat.oneHom_apply, MonCat.toCat_faithful, AddMonCat.equivalence_inverse_map, MonCat.instIsRightAdjointForgetMonoidHomCarrier, AddMonCat.equivalence_counitIso, GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, MonCat.FilteredColimits.M.map_mk, CategoryTheory.IsCommMonObj.ofRepresentableBy, SemiRingCat.forget₂Mon_preservesLimitsOfSize, MonCat.ofHom_comp, CategoryTheory.IsCommMon.ofRepresentableBy, CategoryTheory.essImage_yonedaMon, CategoryTheory.yonedaMon_naturality_assoc, CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, MonCat.hom_one, CategoryTheory.yonedaMonObj_map, CategoryTheory.instFaithfulMonFunctorOppositeMonCatYonedaMon, CategoryTheory.yonedaMon_naturality, CommMonCat.forget₂_map_ofHom, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, CategoryTheory.yonedaMonObj_obj_coe, SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, GrpCat.forget₂Mon_preservesLimits, CommMonCat.hom_forget₂_map, AddMonCat.equivalence_inverse_obj_coe, CommMonCat.forget₂Mon_preservesLimitsOfSize, MulEquiv.toMonCatIso_inv, CategoryTheory.yonedaMon_map_app, MonCat.adjoinOne_obj_coe, MonCat.comp_apply, MonCat.uliftFunctor_obj_coe, MonCat.coe_comp, MonCat.forget_isCorepresentable, MonCat.HasLimits.hasLimit, MonCat.adjoinOne_map, MonCat.FilteredColimits.cocone_naturality, MulEquiv.toMonCatIso_hom, CategoryTheory.yonedaGrpObj_map, GrpCat.forget₂_map, MonCat.FilteredColimits.forget_preservesFilteredColimits, MonCat.HasLimits.hasLimitsOfShape, CategoryTheory.MonObj.ofRepresentableBy_mul, GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections, MonCat.uliftFunctor_map, MonCat.toCat_full, MonCat.val_units_map_hom_apply, MonCat.hasLimitsOfSize, GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier, MonCat.Colimits.cocone_naturality_components, CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits, MonCat.FilteredColimits.colimit_one_eq, MonCat.ofHom_id, MonCat.coe_id, MonCat.FilteredColimits.colimit_mul_mk_eq, MonCat.val_inv_units_map_hom_apply, CommMonCat.forget₂Mon_preservesLimits, AddMonCat.equivalence_unitIso, MonCat.units_obj_coe, MonCat.Colimits.hasColimits_monCat, GrpCat.forget₂_map_ofHom, AddMonCat.equivalence_functor_map, MonCat.hom_comp, MonCat.forget_preservesLimits, CategoryTheory.yonedaGrp_map_app, SemiRingCat.forget₂_monCat_map, MonCat.Colimits.cocone_naturality, instIsRightAdjointGrpCatMonCatUnits, MonCat.id_apply, MonCat.ofHom_apply, GrpCat.forget₂Mon_preservesLimitsOfSize, SemiRingCat.forget₂Mon_preservesLimits, MonCat.hom_id, CategoryTheory.yonedaMon_obj, MonCat.inv_hom_apply, MonCat.hom_inv_apply, MonCat.FilteredColimits.M.mk_surjective, MonCat.hasLimits

---

← Back to Index