Basic

📁 Source: Mathlib/Algebra/Category/MonCat/Basic.lean

Statistics

Metric	Count
Definitions `AddCommMonCat`, `hom`, `hom`, `hom'`, `carrier`, `equivalence`, `fullyFaithfulForgetToAddMonCat`, `hasForgetToAddMonCat`, `instCategory`, `instCoeMonCat`, `instCoeSortType`, `instConcreteCategoryAddMonoidHomCarrier`, `instInhabited`, `of`, `ofHom`, `str`, `uliftFunctor`, `toAddCommMonCatIso`, `toAddMonCatIso`, `AddMonCat`, `hom`, `hom'`, `carrier`, `equivalence`, `instCategory`, `instCoeSortType`, `instConcreteCategoryAddMonoidHomCarrier`, `instInhabited`, `instZeroHom`, `of`, `ofHom`, `str`, `uliftFunctor`, `addMonCatIsoToAddEquiv`, `commMonCatIsoToAddEquiv`, `commMonCatIsoToMulEquiv`, `monCatIsoToMulEquiv`, `CommMonCat`, `hom`, `hom`, `hom'`, `carrier`, `fullyFaithfulForgetToMonCat`, `hasForgetToMonCat`, `instCategory`, `instCoeMonCat`, `instCoeSortType`, `instConcreteCategoryMonoidHomCarrier`, `instInhabited`, `of`, `ofHom`, `str`, `uliftFunctor`, `hom`, `hom`, `hom'`, `carrier`, `instCategory`, `instCoeSortType`, `instConcreteCategoryMonoidHomCarrier`, `instInhabited`, `instOneHom`, `of`, `ofHom`, `str`, `uliftFunctor`, `toCommMonCatIso`, `toMonCatIso`, `addEquivIsoAddCommMonCatIso`, `addEquivIsoAddMonCatIso`, `mulEquivIsoCommMonCatIso`, `mulEquivIsoMonCatIso`	72
Theorems `ext`, `ext_iff`, `coe_comp`, `coe_forget₂_obj`, `coe_id`, `coe_of`, `comp_apply`, `equivalence_counitIso`, `equivalence_functor_map`, `equivalence_functor_obj_coe`, `equivalence_inverse_map`, `equivalence_inverse_obj_coe`, `equivalence_unitIso`, `ext`, `ext_iff`, `forget_map`, `forget_reflects_isos`, `forget₂_full`, `forget₂_map_ofHom`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_forget₂_map`, `hom_id`, `hom_neg_apply`, `hom_ofHom`, `id_apply`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `neg_hom_apply`, `ofHom_apply`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `uliftFunctor_map`, `uliftFunctor_obj_coe`, `toAddCommMonCatIso_hom`, `toAddCommMonCatIso_inv`, `toAddMonCatIso_hom`, `toAddMonCatIso_inv`, `ext`, `ext_iff`, `add_of`, `coe_comp`, `coe_id`, `coe_of`, `comp_apply`, `equivalence_counitIso`, `equivalence_functor_map`, `equivalence_functor_obj_coe`, `equivalence_inverse_map`, `equivalence_inverse_obj_coe`, `equivalence_unitIso`, `ext`, `ext_iff`, `forget_map`, `forget_reflects_isos`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_id`, `hom_neg_apply`, `hom_ofHom`, `hom_zero`, `id_apply`, `neg_hom_apply`, `ofHom_apply`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `uliftFunctor_map`, `uliftFunctor_obj_coe`, `zeroHom_apply`, `zero_of`, `ext`, `ext_iff`, `coe_comp`, `coe_forget₂_obj`, `coe_id`, `coe_of`, `comp_apply`, `ext`, `ext_iff`, `forget_map`, `forget_reflects_isos`, `forget₂_full`, `forget₂_map_ofHom`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_forget₂_map`, `hom_id`, `hom_inv_apply`, `hom_ofHom`, `id_apply`, `instFullMonCatForget₂MonoidHomCarrierCarrier`, `inv_hom_apply`, `ofHom_apply`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `uliftFunctor_map`, `uliftFunctor_obj_coe`, `ext`, `ext_iff`, `coe_comp`, `coe_id`, `coe_of`, `comp_apply`, `ext`, `ext_iff`, `forget_map`, `forget_reflects_isos`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_id`, `hom_inv_apply`, `hom_ofHom`, `hom_one`, `id_apply`, `inv_hom_apply`, `mul_of`, `ofHom_apply`, `ofHom_comp`, `ofHom_hom`, `ofHom_id`, `oneHom_apply`, `one_of`, `uliftFunctor_map`, `uliftFunctor_obj_coe`, `toCommMonCatIso_hom`, `toCommMonCatIso_inv`, `toMonCatIso_hom`, `toMonCatIso_inv`	134
Total	206

AddCommMonCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	54 math math: `coyoneda_obj_obj_coe`, `free_obj_coe`, `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `coe_id`, `ofHom_apply`, `FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `coe_of`, `hom_forget₂_map`, `forget₂AddMonPreservesLimitsOfSize`, `coyonedaType_obj_map`, `coyonedaType_map_app`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `equivalence_functor_map`, `forget_preservesLimitsOfShape`, `comp_apply`, `forget₂_full`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `forget_preservesLimits`, `FilteredColimits.forget_preservesFilteredColimits`, `neg_hom_apply`, `forget₂Mon_preservesLimits`, `ext_iff`, `coe_comp`, `coyoneda_map_app`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape`, `instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `equivalence_inverse_obj_coe`, `ofHom_hom`, `hom_neg_apply`, `coe_forget₂_obj`, `coyonedaForget_inv_app_app`, `coyonedaType_obj_obj_coe`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `SemiRingCat.forget₂AddCommMon_preservesLimits`, `forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize`, `forget_isCorepresentable`, `equivalence_functor_obj_coe`, `equivalence_counitIso`, `forget_preservesLimitsOfSize`, `uliftFunctor_obj_coe`, `id_apply`, `coyoneda_obj_map`, `SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize`, `coyonedaForget_hom_app_app_hom`, `hom_comp`, `hom_id`, `forget_map`, `forget_reflects_isos`, `SemimoduleCat.forget₂_obj`, `uliftFunctor_map`, `SemimoduleCat.forget₂_map`, `SemiRingCat.forget₂_addCommMonCat_map`
`equivalence` 📖	CompOp	6 math math: `equivalence_unitIso`, `equivalence_functor_map`, `equivalence_inverse_obj_coe`, `equivalence_functor_obj_coe`, `equivalence_counitIso`, `equivalence_inverse_map`
`fullyFaithfulForgetToAddMonCat` 📖	CompOp	—
`hasForgetToAddMonCat` 📖	CompOp	9 math math: `FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `hom_forget₂_map`, `forget₂AddMonPreservesLimitsOfSize`, `forget₂_full`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `forget₂Mon_preservesLimits`, `instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `coe_forget₂_obj`, `forget₂_map_ofHom`
`instCategory` 📖	CompOp	64 math math: `coyoneda_obj_obj_coe`, `equivalence_unitIso`, `free_obj_coe`, `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `coe_id`, `ofHom_apply`, `FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `hom_forget₂_map`, `hasLimitsOfSize`, `free_map`, `forget₂AddMonPreservesLimitsOfSize`, `coyonedaType_obj_map`, `coyonedaType_map_app`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `equivalence_functor_map`, `forget_preservesLimitsOfShape`, `comp_apply`, `forget₂_full`, `AddEquiv.toAddCommMonCatIso_inv`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `forget_preservesLimits`, `FilteredColimits.forget_preservesFilteredColimits`, `neg_hom_apply`, `forget₂Mon_preservesLimits`, `ext_iff`, `instIsLeftAdjointFree`, `coe_comp`, `coyoneda_map_app`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape`, `instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `equivalence_inverse_obj_coe`, `hom_neg_apply`, `coe_forget₂_obj`, `ofHom_comp`, `coyonedaForget_inv_app_app`, `coyonedaType_obj_obj_coe`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `SemiRingCat.forget₂AddCommMon_preservesLimits`, `forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize`, `forget_isCorepresentable`, `equivalence_functor_obj_coe`, `equivalence_counitIso`, `forget_preservesLimitsOfSize`, `uliftFunctor_obj_coe`, `id_apply`, `coyoneda_obj_map`, `ofHom_id`, `SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize`, `coyonedaForget_hom_app_app_hom`, `equivalence_inverse_map`, `hasLimitsOfShape`, `hasLimits`, `hom_comp`, `hom_id`, `forget_map`, `forget_reflects_isos`, `SemimoduleCat.forget₂_obj`, `uliftFunctor_map`, `SemimoduleCat.forget₂_map`, `AddEquiv.toAddCommMonCatIso_hom`, `SemiRingCat.forget₂_addCommMonCat_map`, `hasLimit`
`instCoeMonCat` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryAddMonoidHomCarrier` 📖	CompOp	37 math math: `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `coe_id`, `ofHom_apply`, `FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `hom_forget₂_map`, `forget₂AddMonPreservesLimitsOfSize`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `forget_preservesLimitsOfShape`, `comp_apply`, `forget₂_full`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `forget_preservesLimits`, `FilteredColimits.forget_preservesFilteredColimits`, `neg_hom_apply`, `forget₂Mon_preservesLimits`, `ext_iff`, `coe_comp`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape`, `instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `hom_neg_apply`, `coe_forget₂_obj`, `coyonedaForget_inv_app_app`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `SemiRingCat.forget₂AddCommMon_preservesLimits`, `forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize`, `forget_isCorepresentable`, `forget_preservesLimitsOfSize`, `id_apply`, `SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize`, `coyonedaForget_hom_app_app_hom`, `forget_map`, `forget_reflects_isos`, `SemimoduleCat.forget₂_obj`, `SemimoduleCat.forget₂_map`, `SemiRingCat.forget₂_addCommMonCat_map`
`instInhabited` 📖	CompOp	—
`of` 📖	CompOp	13 math math: `ofHom_apply`, `coe_of`, `hom_ofHom`, `coyonedaType_map_app`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `AddEquiv.toAddCommMonCatIso_inv`, `coyoneda_map_app`, `ofHom_comp`, `forget₂_map_ofHom`, `equivalence_counitIso`, `ofHom_id`, `SemimoduleCat.forget₂_obj`, `AddEquiv.toAddCommMonCatIso_hom`
`ofHom` 📖	CompOp	18 math math: `ofHom_apply`, `free_map`, `coyonedaType_obj_map`, `hom_ofHom`, `coyonedaType_map_app`, `AddEquiv.toAddCommMonCatIso_inv`, `coyoneda_map_app`, `ofHom_hom`, `ofHom_comp`, `forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `equivalence_counitIso`, `coyoneda_obj_map`, `ofHom_id`, `equivalence_inverse_map`, `uliftFunctor_map`, `SemimoduleCat.forget₂_map`, `AddEquiv.toAddCommMonCatIso_hom`
`str` 📖	CompOp	48 math math: `coyoneda_obj_obj_coe`, `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `coe_id`, `ofHom_apply`, `FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `hom_forget₂_map`, `forget₂AddMonPreservesLimitsOfSize`, `coyonedaType_obj_map`, `coyonedaType_map_app`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `equivalence_functor_map`, `forget_preservesLimitsOfShape`, `comp_apply`, `forget₂_full`, `instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `forget_preservesLimits`, `FilteredColimits.forget_preservesFilteredColimits`, `neg_hom_apply`, `forget₂Mon_preservesLimits`, `ext_iff`, `coe_comp`, `coyoneda_map_app`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape`, `instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_hom`, `hom_neg_apply`, `coe_forget₂_obj`, `coyonedaForget_inv_app_app`, `instIsRightAdjointForgetAddMonoidHomCarrier`, `SemiRingCat.forget₂AddCommMon_preservesLimits`, `forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize`, `forget_isCorepresentable`, `equivalence_counitIso`, `forget_preservesLimitsOfSize`, `id_apply`, `coyoneda_obj_map`, `SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize`, `coyonedaForget_hom_app_app_hom`, `hom_comp`, `hom_id`, `forget_map`, `forget_reflects_isos`, `SemimoduleCat.forget₂_obj`, `uliftFunctor_map`, `SemimoduleCat.forget₂_map`, `SemiRingCat.forget₂_addCommMonCat_map`
`uliftFunctor` 📖	CompOp	2 math math: `uliftFunctor_obj_coe`, `uliftFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_forget₂_obj` 📖	mathematical	—	`AddMonCat.carrier` `CategoryTheory.Functor.obj` `AddCommMonCat` `instCategory` `AddMonCat` `AddMonCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `AddMonCat.str` `AddMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddMonCat`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`equivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `AddCommMonCat` `CommMonCat` `instCategory` `CommMonCat.instCategory` `equivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `of` `Additive` `CommMonCat.carrier` `Additive.addCommMonoid` `CommMonCat.str` `ofHom` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Additive.addZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom.toAdditive` `CommMonCat.Hom.hom` `CommMonCat.of` `Multiplicative` `carrier` `Multiplicative.commMonoid` `str` `CommMonCat.ofHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Multiplicative.mulOneClass` `AddMonoidHom.toMultiplicative` `Hom.hom`	—	—
`equivalence_functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddCommMonCat` `instCategory` `CommMonCat` `CommMonCat.instCategory` `CategoryTheory.Equivalence.functor` `equivalence` `CommMonCat.ofHom` `Multiplicative` `carrier` `Multiplicative.commMonoid` `str` `DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `MonoidHom` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddMonoidHom.toMultiplicative` `Hom.hom`	—	—
`equivalence_functor_obj_coe` 📖	mathematical	—	`CommMonCat.carrier` `CategoryTheory.Functor.obj` `AddCommMonCat` `instCategory` `CommMonCat` `CommMonCat.instCategory` `CategoryTheory.Equivalence.functor` `equivalence` `Multiplicative` `carrier`	—	—
`equivalence_inverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommMonCat` `CommMonCat.instCategory` `AddCommMonCat` `instCategory` `CategoryTheory.Equivalence.inverse` `equivalence` `ofHom` `Additive` `CommMonCat.carrier` `Additive.addCommMonoid` `CommMonCat.str` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `AddMonoidHom` `AddZeroClass.toAddZero` `Additive.addZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom.toAdditive` `CommMonCat.Hom.hom`	—	—
`equivalence_inverse_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CommMonCat` `CommMonCat.instCategory` `AddCommMonCat` `instCategory` `CategoryTheory.Equivalence.inverse` `equivalence` `Additive` `CommMonCat.carrier`	—	—
`equivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `AddCommMonCat` `CommMonCat` `instCategory` `CommMonCat.instCategory` `equivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—
`ext` 📖	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddCommMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	—
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `AddCommMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`Equiv.left_inv` `Equiv.right_inv` `AddMonoidHom.map_add'` `CategoryTheory.Iso.isIso_hom`
`forget₂_full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `AddCommMonCat` `instCategory` `AddMonCat` `AddMonCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `AddMonCat.carrier` `AddMonCat.str` `AddMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddMonCat`	—	—
`forget₂_map_ofHom` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddCommMonCat` `instCategory` `AddMonCat` `AddMonCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `AddMonCat.carrier` `AddMonCat.str` `AddMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddMonCat` `of` `ofHom` `AddMonCat.ofHom`	—	—
`hom_comp` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `AddCommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `AddMonoidHom.comp` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_forget₂_map` 📖	mathematical	—	`AddMonCat.Hom.hom` `CategoryTheory.Functor.obj` `AddCommMonCat` `instCategory` `AddMonCat` `AddMonCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `AddMonCat.carrier` `AddMonCat.str` `AddMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddMonCat` `CategoryTheory.Functor.map` `Hom.hom`	—	—
`hom_id` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `AddCommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `AddMonoidHom.id` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str`	—	—
`hom_neg_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.inv_hom_id_apply`
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`instFullMonCatForget₂AddMonoidHomCarrierCarrier` 📖	mathematical	—	`CategoryTheory.Functor.Full` `AddCommMonCat` `instCategory` `AddMonCat` `AddMonCat.instCategory` `CategoryTheory.forget₂` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `AddMonCat.carrier` `AddMonCat.str` `AddMonCat.instConcreteCategoryAddMonoidHomCarrier` `hasForgetToAddMonCat`	—	`CategoryTheory.Functor.FullyFaithful.full`
`neg_hom_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id_apply`
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddCommMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `ofHom`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `CategoryTheory.CategoryStruct.comp` `AddCommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `str` `Hom.hom`	—	—
`ofHom_id` 📖	mathematical	—	`ofHom` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `CategoryTheory.CategoryStruct.id` `AddCommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`uliftFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddCommMonCat` `instCategory` `uliftFunctor` `ofHom` `carrier` `ULift.addCommMonoid` `str` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `ULift.addZeroClass` `AddEquiv.toAddMonoidHom` `AddEquiv.symm` `ULift.add` `AddZero.toAdd` `AddEquiv.ulift` `Hom.hom`	—	—
`uliftFunctor_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `AddCommMonCat` `instCategory` `uliftFunctor`	—	—

AddCommMonCat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	15 math math: `AddCommMonCat.hom_forget₂_map`, `AddCommMonCat.coyonedaType_obj_map`, `AddCommMonCat.hom_ofHom`, `AddCommMonCat.coyonedaType_map_app`, `AddCommMonCat.equivalence_functor_map`, `AddCommMonCat.hom_ext_iff`, `AddCommMonCat.coyoneda_map_app`, `AddCommMonCat.ofHom_hom`, `AddCommMonCat.coyonedaForget_inv_app_app`, `AddCommMonCat.equivalence_counitIso`, `AddCommMonCat.coyoneda_obj_map`, `AddCommMonCat.coyonedaForget_hom_app_app_hom`, `AddCommMonCat.hom_comp`, `AddCommMonCat.hom_id`, `AddCommMonCat.uliftFunctor_map`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`

AddCommMonCat.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

AddEquiv

Definitions

Name	Category	Theorems
`toAddCommMonCatIso` 📖	CompOp	2 math math: `toAddCommMonCatIso_inv`, `toAddCommMonCatIso_hom`
`toAddMonCatIso` 📖	CompOp	2 math math: `toAddMonCatIso_hom`, `toAddMonCatIso_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toAddCommMonCatIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `AddCommMonCat` `AddCommMonCat.instCategory` `AddCommMonCat.of` `toAddCommMonCatIso` `AddCommMonCat.ofHom` `toAddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	—
`toAddCommMonCatIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `AddCommMonCat` `AddCommMonCat.instCategory` `AddCommMonCat.of` `toAddCommMonCatIso` `AddCommMonCat.ofHom` `toAddMonoidHom` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `symm` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`toAddMonCatIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `AddMonCat` `AddMonCat.instCategory` `AddMonCat.of` `toAddMonCatIso` `AddMonCat.ofHom` `toAddMonoidHom` `AddMonoid.toAddZeroClass`	—	—
`toAddMonCatIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `AddMonCat` `AddMonCat.instCategory` `AddMonCat.of` `toAddMonCatIso` `AddMonCat.ofHom` `toAddMonoidHom` `AddMonoid.toAddZeroClass` `symm` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—

AddMonCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	55 math math: `AddGrpCat.forget₂_map`, `comp_apply`, `FilteredColimits.M.mk_surjective`, `uliftFunctor_map`, `zeroHom_apply`, `equivalence_functor_obj_coe`, `forget_reflects_isos`, `forget_preservesLimitsOfSize`, `hom_zero`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `ext_iff`, `AddCommMonCat.hom_forget₂_map`, `hom_comp`, `FilteredColimits.colimit_add_mk_eq`, `forget_preservesLimitsOfShape`, `AddGrpCat.FilteredColimits.colimit_add_mk_eq`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `equivalence_counitIso`, `forget_map`, `AddGrpCat.FilteredColimits.colimit_neg_mk_eq`, `coe_comp`, `AddGrpCat.forget₂AddMonPreservesLimitsOfSize`, `ofHom_hom`, `AddCommMonCat.forget₂_full`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `FilteredColimits.colimit_zero_eq`, `coe_id`, `FilteredColimits.M.map_mk`, `AddCommMonCat.forget₂Mon_preservesLimits`, `equivalence_inverse_obj_coe`, `neg_hom_apply`, `coe_of`, `forget_isCorepresentable`, `hom_id`, `AddGrpCat.forget₂_map_ofHom`, `id_apply`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_apply`, `AddGrpCat.FilteredColimits.colimit_add_mk_eq'`, `FilteredColimits.colimit_add_mk_eq'`, `AddCommMonCat.coe_forget₂_obj`, `zero_of`, `forget_preservesLimits`, `adjoinZero_obj_coe`, `AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `hom_neg_apply`, `AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits`, `AddCommMonCat.forget₂_map_ofHom`, `add_of`, `uliftFunctor_obj_coe`, `equivalence_functor_map`, `AddGrpCat.FilteredColimits.colimit_zero_eq`, `AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddGrpCat.forget₂Mon_preservesLimits`
`equivalence` 📖	CompOp	6 math math: `equivalence_functor_obj_coe`, `equivalence_inverse_map`, `equivalence_counitIso`, `equivalence_inverse_obj_coe`, `equivalence_unitIso`, `equivalence_functor_map`
`instCategory` 📖	CompOp	59 math math: `hasLimitsOfSize`, `AddGrpCat.forget₂_map`, `comp_apply`, `FilteredColimits.M.mk_surjective`, `uliftFunctor_map`, `AddEquiv.toAddMonCatIso_hom`, `zeroHom_apply`, `equivalence_functor_obj_coe`, `forget_reflects_isos`, `forget_preservesLimitsOfSize`, `hom_zero`, `ofHom_id`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `ext_iff`, `AddCommMonCat.hom_forget₂_map`, `hom_comp`, `FilteredColimits.colimit_add_mk_eq`, `forget_preservesLimitsOfShape`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `equivalence_inverse_map`, `equivalence_counitIso`, `forget_map`, `coe_comp`, `AddEquiv.toAddMonCatIso_inv`, `AddGrpCat.forget₂AddMonPreservesLimitsOfSize`, `AddCommMonCat.forget₂_full`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `FilteredColimits.colimit_zero_eq`, `coe_id`, `FilteredColimits.M.map_mk`, `AddCommMonCat.forget₂Mon_preservesLimits`, `equivalence_inverse_obj_coe`, `neg_hom_apply`, `forget_isCorepresentable`, `hom_id`, `FilteredColimits.cocone_naturality`, `AddGrpCat.forget₂_map_ofHom`, `id_apply`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_apply`, `HasLimits.hasLimitsOfShape`, `FilteredColimits.colimit_add_mk_eq'`, `hasLimits`, `AddCommMonCat.coe_forget₂_obj`, `forget_preservesLimits`, `adjoinZero_obj_coe`, `AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_comp`, `hom_neg_apply`, `AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits`, `AddCommMonCat.forget₂_map_ofHom`, `equivalence_unitIso`, `HasLimits.hasLimit`, `uliftFunctor_obj_coe`, `equivalence_functor_map`, `AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `adjoinZero_map`, `AddGrpCat.forget₂Mon_preservesLimits`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryAddMonoidHomCarrier` 📖	CompOp	33 math math: `AddGrpCat.forget₂_map`, `comp_apply`, `forget_reflects_isos`, `forget_preservesLimitsOfSize`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `ext_iff`, `AddCommMonCat.hom_forget₂_map`, `FilteredColimits.colimit_add_mk_eq`, `forget_preservesLimitsOfShape`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `forget_map`, `coe_comp`, `AddGrpCat.forget₂AddMonPreservesLimitsOfSize`, `AddCommMonCat.forget₂_full`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `coe_id`, `FilteredColimits.M.map_mk`, `AddCommMonCat.forget₂Mon_preservesLimits`, `neg_hom_apply`, `forget_isCorepresentable`, `AddGrpCat.forget₂_map_ofHom`, `id_apply`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_apply`, `AddCommMonCat.coe_forget₂_obj`, `forget_preservesLimits`, `AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `hom_neg_apply`, `AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits`, `AddCommMonCat.forget₂_map_ofHom`, `AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddGrpCat.forget₂Mon_preservesLimits`
`instInhabited` 📖	CompOp	—
`instZeroHom` 📖	CompOp	2 math math: `zeroHom_apply`, `hom_zero`
`of` 📖	CompOp	10 math math: `AddEquiv.toAddMonCatIso_hom`, `ofHom_id`, `equivalence_counitIso`, `AddEquiv.toAddMonCatIso_inv`, `coe_of`, `ofHom_apply`, `zero_of`, `ofHom_comp`, `add_of`, `hom_ofHom`
`ofHom` 📖	CompOp	13 math math: `uliftFunctor_map`, `AddEquiv.toAddMonCatIso_hom`, `ofHom_id`, `equivalence_inverse_map`, `equivalence_counitIso`, `AddEquiv.toAddMonCatIso_inv`, `ofHom_hom`, `AddGrpCat.forget₂_map_ofHom`, `ofHom_apply`, `ofHom_comp`, `AddCommMonCat.forget₂_map_ofHom`, `hom_ofHom`, `adjoinZero_map`
`str` 📖	CompOp	46 math math: `AddGrpCat.forget₂_map`, `comp_apply`, `uliftFunctor_map`, `zeroHom_apply`, `forget_reflects_isos`, `forget_preservesLimitsOfSize`, `hom_zero`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `ext_iff`, `AddCommMonCat.hom_forget₂_map`, `hom_comp`, `FilteredColimits.colimit_add_mk_eq`, `forget_preservesLimitsOfShape`, `AddGrpCat.FilteredColimits.colimit_add_mk_eq`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `equivalence_counitIso`, `forget_map`, `coe_comp`, `AddGrpCat.forget₂AddMonPreservesLimitsOfSize`, `ofHom_hom`, `AddCommMonCat.forget₂_full`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `FilteredColimits.colimit_zero_eq`, `coe_id`, `FilteredColimits.M.map_mk`, `AddCommMonCat.forget₂Mon_preservesLimits`, `neg_hom_apply`, `forget_isCorepresentable`, `hom_id`, `AddGrpCat.forget₂_map_ofHom`, `id_apply`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `ofHom_apply`, `AddGrpCat.FilteredColimits.colimit_add_mk_eq'`, `FilteredColimits.colimit_add_mk_eq'`, `AddCommMonCat.coe_forget₂_obj`, `forget_preservesLimits`, `AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `hom_neg_apply`, `AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits`, `AddCommMonCat.forget₂_map_ofHom`, `equivalence_functor_map`, `AddGrpCat.FilteredColimits.colimit_zero_eq`, `AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddGrpCat.forget₂Mon_preservesLimits`
`uliftFunctor` 📖	CompOp	2 math math: `uliftFunctor_map`, `uliftFunctor_obj_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_of` 📖	mathematical	—	`carrier` `of` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`equivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `AddMonCat` `MonCat` `instCategory` `MonCat.instCategory` `equivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.comp` `of` `Additive` `MonCat.carrier` `Additive.addMonoid` `MonCat.str` `ofHom` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidHom` `AddZeroClass.toAddZero` `Additive.addZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom.toAdditive` `MonCat.Hom.hom` `MonCat.of` `Multiplicative` `carrier` `Multiplicative.monoid` `str` `MonCat.ofHom` `AddMonoid.toAddZeroClass` `Multiplicative.mulOneClass` `AddMonoidHom.toMultiplicative` `Hom.hom`	—	—
`equivalence_functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.Equivalence.functor` `equivalence` `MonCat.ofHom` `Multiplicative` `carrier` `Multiplicative.monoid` `str` `DFunLike.coe` `Equiv` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `MonoidHom` `MulOneClass.toMulOne` `Multiplicative.mulOneClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddMonoidHom.toMultiplicative` `Hom.hom`	—	—
`equivalence_functor_obj_coe` 📖	mathematical	—	`MonCat.carrier` `CategoryTheory.Functor.obj` `AddMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.Equivalence.functor` `equivalence` `Multiplicative` `carrier`	—	—
`equivalence_inverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `MonCat` `MonCat.instCategory` `AddMonCat` `instCategory` `CategoryTheory.Equivalence.inverse` `equivalence` `ofHom` `Additive` `MonCat.carrier` `Additive.addMonoid` `MonCat.str` `DFunLike.coe` `Equiv` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `AddMonoidHom` `AddZeroClass.toAddZero` `Additive.addZeroClass` `EquivLike.toFunLike` `Equiv.instEquivLike` `MonoidHom.toAdditive` `MonCat.Hom.hom`	—	—
`equivalence_inverse_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `MonCat` `MonCat.instCategory` `AddMonCat` `instCategory` `CategoryTheory.Equivalence.inverse` `equivalence` `Additive` `MonCat.carrier`	—	—
`equivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `AddMonCat` `MonCat` `instCategory` `MonCat.instCategory` `equivalence` `CategoryTheory.Iso.refl` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.id`	—	—
`ext` 📖	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	—
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `AddMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier`	—	`Equiv.left_inv` `Equiv.right_inv` `AddMonoidHom.map_add'` `CategoryTheory.Iso.isIso_hom`
`hom_comp` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `AddMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `AddMonoidHom.comp` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_id` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `AddMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `AddMonoidHom.id` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str`	—	—
`hom_neg_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.inv_hom_id_apply`
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`hom_zero` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `AddMonCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instZeroHom` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `instZeroAddMonoidHom`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`neg_hom_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id_apply`
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `carrier` `CategoryTheory.ConcreteCategory.hom` `AddMonCat` `instCategory` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `instConcreteCategoryAddMonoidHomCarrier` `ofHom`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.CategoryStruct.comp` `AddMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `str` `Hom.hom`	—	—
`ofHom_id` 📖	mathematical	—	`ofHom` `AddMonoidHom.id` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.CategoryStruct.id` `AddMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`uliftFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `AddMonCat` `instCategory` `uliftFunctor` `ofHom` `carrier` `ULift.addMonoid` `str` `AddMonoidHom.comp` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ULift.addZeroClass` `AddEquiv.toAddMonoidHom` `AddEquiv.symm` `ULift.add` `AddZero.toAdd` `AddEquiv.ulift` `Hom.hom`	—	—
`uliftFunctor_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `AddMonCat` `instCategory` `uliftFunctor`	—	—
`zeroHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `carrier` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `str` `AddMonoidHom.instFunLike` `Hom.hom` `Quiver.Hom` `AddMonCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instZeroHom` `AddZero.toZero`	—	—
`zero_of` 📖	mathematical	—	`carrier` `of` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	—

AddMonCat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	11 math math: `AddMonCat.uliftFunctor_map`, `AddMonCat.zeroHom_apply`, `AddMonCat.hom_zero`, `AddCommMonCat.hom_forget₂_map`, `AddMonCat.hom_comp`, `AddMonCat.equivalence_counitIso`, `AddMonCat.ofHom_hom`, `AddMonCat.hom_id`, `AddMonCat.hom_ext_iff`, `AddMonCat.equivalence_functor_map`, `AddMonCat.hom_ofHom`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`

CategoryTheory.Iso

Definitions

Name	Category	Theorems
`addMonCatIsoToAddEquiv` 📖	CompOp	—
`commMonCatIsoToAddEquiv` 📖	CompOp	—
`commMonCatIsoToMulEquiv` 📖	CompOp	—
`monCatIsoToMulEquiv` 📖	CompOp	—

CommMonCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	56 math math: `instFullMonCatForget₂MonoidHomCarrierCarrier`, `forget₂_full`, `forget_preservesLimitsOfShape`, `CommGrpCat.forget₂CommMon_preservesLimitsOfShape`, `coe_of`, `coe_forget₂_obj`, `hom_comp`, `coyonedaType_obj_map`, `coe_comp`, `coyoneda_obj_map`, `forget_preservesLimitsOfSize`, `CommGrpCat.forget₂CommMon_preservesLimitsOfSize`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `val_units_map_hom_apply`, `coyonedaForget_inv_app_app`, `val_inv_units_map_hom_apply`, `forget₂_map_ofHom`, `forget_map`, `comp_apply`, `hom_forget₂_map`, `coyonedaType_obj_obj_coe`, `forget₂Mon_preservesLimitsOfSize`, `inv_hom_apply`, `CommRingCat.commMon_forget₂_obj_coe`, `coe_id`, `CommRingCat.monoidAlgebra_map`, `hom_id`, `AddCommMonCat.equivalence_inverse_obj_coe`, `uliftFunctor_obj_coe`, `instIsRightAdjointForgetMonoidHomCarrier`, `forget_reflects_isos`, `forget_preservesLimits`, `FilteredColimits.forget₂Mon_preservesFilteredColimits`, `coyoneda_map_app`, `ofHom_hom`, `coyoneda_obj_obj_coe`, `units_obj_coe`, `id_apply`, `forget₂Mon_preservesLimits`, `coyonedaForget_hom_app_app_hom`, `uliftFunctor_map`, `AddCommMonCat.equivalence_functor_obj_coe`, `AddCommMonCat.equivalence_counitIso`, `CommRingCat.monoidAlgebra_obj`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.equivalence_inverse_map`, `ofHom_apply`, `forget_isCorepresentable`, `ext_iff`, `coyonedaType_map_app`, `hom_inv_apply`
`fullyFaithfulForgetToMonCat` 📖	CompOp	—
`hasForgetToMonCat` 📖	CompOp	11 math math: `instFullMonCatForget₂MonoidHomCarrierCarrier`, `forget₂_full`, `coe_forget₂_obj`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `forget₂_map_ofHom`, `hom_forget₂_map`, `forget₂Mon_preservesLimitsOfSize`, `FilteredColimits.forget₂Mon_preservesFilteredColimits`, `forget₂Mon_preservesLimits`
`instCategory` 📖	CompOp	66 math math: `instFullMonCatForget₂MonoidHomCarrierCarrier`, `MulEquiv.toCommMonCatIso_hom`, `forget₂_full`, `AddCommMonCat.equivalence_unitIso`, `forget_preservesLimitsOfShape`, `CommGrpCat.forget₂CommMon_preservesLimitsOfShape`, `coe_forget₂_obj`, `hom_comp`, `coyonedaType_obj_map`, `coe_comp`, `coyoneda_obj_map`, `forget_preservesLimitsOfSize`, `CommGrpCat.forget₂CommMon_preservesLimitsOfSize`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `AddCommMonCat.equivalence_functor_map`, `CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `val_units_map_hom_apply`, `coyonedaForget_inv_app_app`, `ofHom_comp`, `val_inv_units_map_hom_apply`, `forget₂_map_ofHom`, `hasLimitsOfSize`, `forget_map`, `comp_apply`, `hom_forget₂_map`, `coyonedaType_obj_obj_coe`, `forget₂Mon_preservesLimitsOfSize`, `hasLimits`, `inv_hom_apply`, `CommRingCat.commMon_forget₂_obj_coe`, `coe_id`, `CommRingCat.monoidAlgebra_map`, `hom_id`, `AddCommMonCat.equivalence_inverse_obj_coe`, `uliftFunctor_obj_coe`, `instIsRightAdjointForgetMonoidHomCarrier`, `forget_reflects_isos`, `forget_preservesLimits`, `FilteredColimits.forget₂Mon_preservesFilteredColimits`, `coyoneda_map_app`, `coyoneda_obj_obj_coe`, `instIsRightAdjointCommGrpCatCommMonCatUnits`, `hasLimit`, `units_obj_coe`, `id_apply`, `MulEquiv.toCommMonCatIso_inv`, `forget₂Mon_preservesLimits`, `coyonedaForget_hom_app_app_hom`, `uliftFunctor_map`, `AddCommMonCat.equivalence_functor_obj_coe`, `AddCommMonCat.equivalence_counitIso`, `CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra`, `CommRingCat.monoidAlgebra_obj`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.equivalence_inverse_map`, `ofHom_id`, `ofHom_apply`, `hasLimitsOfShape`, `forget_isCorepresentable`, `ext_iff`, `coyonedaType_map_app`, `hom_inv_apply`
`instCoeMonCat` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryMonoidHomCarrier` 📖	CompOp	35 math math: `instFullMonCatForget₂MonoidHomCarrierCarrier`, `forget₂_full`, `forget_preservesLimitsOfShape`, `CommGrpCat.forget₂CommMon_preservesLimitsOfShape`, `coe_forget₂_obj`, `coe_comp`, `forget_preservesLimitsOfSize`, `CommGrpCat.forget₂CommMon_preservesLimitsOfSize`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `coyonedaForget_inv_app_app`, `forget₂_map_ofHom`, `forget_map`, `comp_apply`, `hom_forget₂_map`, `forget₂Mon_preservesLimitsOfSize`, `inv_hom_apply`, `CommRingCat.commMon_forget₂_obj_coe`, `coe_id`, `instIsRightAdjointForgetMonoidHomCarrier`, `forget_reflects_isos`, `forget_preservesLimits`, `FilteredColimits.forget₂Mon_preservesFilteredColimits`, `id_apply`, `forget₂Mon_preservesLimits`, `coyonedaForget_hom_app_app_hom`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `FilteredColimits.forget_preservesFilteredColimits`, `ofHom_apply`, `forget_isCorepresentable`, `ext_iff`, `hom_inv_apply`
`instInhabited` 📖	CompOp	—
`of` 📖	CompOp	11 math math: `MulEquiv.toCommMonCatIso_hom`, `coe_of`, `ofHom_comp`, `forget₂_map_ofHom`, `hom_ofHom`, `coyoneda_map_app`, `MulEquiv.toCommMonCatIso_inv`, `AddCommMonCat.equivalence_counitIso`, `ofHom_id`, `ofHom_apply`, `coyonedaType_map_app`
`ofHom` 📖	CompOp	17 math math: `MulEquiv.toCommMonCatIso_hom`, `coyonedaType_obj_map`, `coyoneda_obj_map`, `AddCommMonCat.equivalence_functor_map`, `ofHom_comp`, `forget₂_map_ofHom`, `hom_ofHom`, `coyoneda_map_app`, `ofHom_hom`, `MulEquiv.toCommMonCatIso_inv`, `uliftFunctor_map`, `AddCommMonCat.equivalence_counitIso`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `ofHom_id`, `ofHom_apply`, `coyonedaType_map_app`
`str` 📖	CompOp	51 math math: `instFullMonCatForget₂MonoidHomCarrierCarrier`, `forget₂_full`, `forget_preservesLimitsOfShape`, `CommGrpCat.forget₂CommMon_preservesLimitsOfShape`, `coe_forget₂_obj`, `hom_comp`, `coyonedaType_obj_map`, `coe_comp`, `coyoneda_obj_map`, `forget_preservesLimitsOfSize`, `CommGrpCat.forget₂CommMon_preservesLimitsOfSize`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `val_units_map_hom_apply`, `coyonedaForget_inv_app_app`, `val_inv_units_map_hom_apply`, `forget₂_map_ofHom`, `forget_map`, `comp_apply`, `hom_forget₂_map`, `forget₂Mon_preservesLimitsOfSize`, `inv_hom_apply`, `CommRingCat.commMon_forget₂_obj_coe`, `coe_id`, `CommRingCat.monoidAlgebra_map`, `hom_id`, `instIsRightAdjointForgetMonoidHomCarrier`, `forget_reflects_isos`, `forget_preservesLimits`, `FilteredColimits.forget₂Mon_preservesFilteredColimits`, `coyoneda_map_app`, `ofHom_hom`, `coyoneda_obj_obj_coe`, `units_obj_coe`, `id_apply`, `forget₂Mon_preservesLimits`, `coyonedaForget_hom_app_app_hom`, `uliftFunctor_map`, `AddCommMonCat.equivalence_counitIso`, `CommRingCat.monoidAlgebra_obj`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.equivalence_inverse_map`, `ofHom_apply`, `forget_isCorepresentable`, `ext_iff`, `coyonedaType_map_app`, `hom_inv_apply`
`uliftFunctor` 📖	CompOp	2 math math: `uliftFunctor_obj_coe`, `uliftFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_forget₂_obj` 📖	mathematical	—	`MonCat.carrier` `CategoryTheory.Functor.obj` `CommMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `MonCat.str` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`ext` 📖	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	—
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `CommMonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`Equiv.left_inv` `Equiv.right_inv` `MonoidHom.map_mul'` `CategoryTheory.Iso.isIso_hom`
`forget₂_full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CommMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `MonCat.carrier` `MonCat.str` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat`	—	—
`forget₂_map_ofHom` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `MonCat.carrier` `MonCat.str` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat` `of` `ofHom` `MonCat.ofHom`	—	—
`hom_comp` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `CommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `MonoidHom.comp` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_forget₂_map` 📖	mathematical	—	`MonCat.Hom.hom` `CategoryTheory.Functor.obj` `CommMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `MonCat.carrier` `MonCat.str` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat` `CategoryTheory.Functor.map` `Hom.hom`	—	—
`hom_id` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `CommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `MonoidHom.id` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str`	—	—
`hom_inv_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.inv_hom_id_apply`
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`instFullMonCatForget₂MonoidHomCarrierCarrier` 📖	mathematical	—	`CategoryTheory.Functor.Full` `CommMonCat` `instCategory` `MonCat` `MonCat.instCategory` `CategoryTheory.forget₂` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `MonCat.carrier` `MonCat.str` `MonCat.instConcreteCategoryMonoidHomCarrier` `hasForgetToMonCat`	—	`CategoryTheory.Functor.FullyFaithful.full`
`inv_hom_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id_apply`
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `carrier` `CategoryTheory.ConcreteCategory.hom` `CommMonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `ofHom`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CategoryTheory.CategoryStruct.comp` `CommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `str` `Hom.hom`	—	—
`ofHom_id` 📖	mathematical	—	`ofHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `CategoryTheory.CategoryStruct.id` `CommMonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`uliftFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CommMonCat` `instCategory` `uliftFunctor` `ofHom` `carrier` `ULift.commMonoid` `str` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `ULift.mulOneClass` `MulEquiv.toMonoidHom` `MulEquiv.symm` `ULift.mul` `MulOne.toMul` `MulEquiv.ulift` `Hom.hom`	—	—
`uliftFunctor_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `CommMonCat` `instCategory` `uliftFunctor`	—	—

CommMonCat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	18 math math: `CommMonCat.hom_ext_iff`, `CommMonCat.hom_comp`, `CommMonCat.coyonedaType_obj_map`, `CommMonCat.coyoneda_obj_map`, `CommMonCat.val_units_map_hom_apply`, `CommMonCat.coyonedaForget_inv_app_app`, `CommMonCat.val_inv_units_map_hom_apply`, `CommMonCat.hom_ofHom`, `CommMonCat.hom_forget₂_map`, `CommRingCat.monoidAlgebra_map`, `CommMonCat.hom_id`, `CommMonCat.coyoneda_map_app`, `CommMonCat.ofHom_hom`, `CommMonCat.coyonedaForget_hom_app_app_hom`, `CommMonCat.uliftFunctor_map`, `AddCommMonCat.equivalence_counitIso`, `AddCommMonCat.equivalence_inverse_map`, `CommMonCat.coyonedaType_map_app`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`

CommMonCat.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

MonCat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	77 math math: `GrpCat.FilteredColimits.colimit_inv_mk_eq`, `CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `coe_of`, `CommMonCat.forget₂_full`, `FilteredColimits.colimit_mul_mk_eq'`, `forget_map`, `forget_reflects_isos`, `AddMonCat.equivalence_functor_obj_coe`, `CommMonCat.coe_forget₂_obj`, `ext_iff`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply`, `forget_preservesLimitsOfSize`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply`, `forget_preservesLimitsOfShape`, `CategoryTheory.MonObj.ofRepresentableBy_one`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk`, `oneHom_apply`, `AddMonCat.equivalence_inverse_map`, `instIsRightAdjointForgetMonoidHomCarrier`, `AddMonCat.equivalence_counitIso`, `GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.M.map_mk`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `SemiRingCat.forget₂Mon_preservesLimitsOfSize`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `CategoryTheory.essImage_yonedaMon`, `CategoryTheory.yonedaMon_naturality_assoc`, `CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `hom_one`, `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`, `adjoinOne_obj_coe`, `comp_apply`, `uliftFunctor_obj_coe`, `coe_comp`, `forget_isCorepresentable`, `GrpCat.forget₂_map`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq`, `FilteredColimits.forget_preservesFilteredColimits`, `CategoryTheory.MonObj.ofRepresentableBy_mul`, `GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `uliftFunctor_map`, `GrpCat.FilteredColimits.colimit_mul_mk_eq`, `val_units_map_hom_apply`, `GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `Colimits.cocone_naturality_components`, `CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.colimit_one_eq`, `coe_id`, `FilteredColimits.colimit_mul_mk_eq`, `one_of`, `val_inv_units_map_hom_apply`, `CommMonCat.forget₂Mon_preservesLimits`, `units_obj_coe`, `GrpCat.forget₂_map_ofHom`, `hom_comp`, `GrpCat.FilteredColimits.colimit_mul_mk_eq'`, `forget_preservesLimits`, `mul_of`, `SemiRingCat.forget₂_monCat_map`, `ofHom_hom`, `GrpCat.FilteredColimits.colimit_one_eq`, `id_apply`, `ofHom_apply`, `GrpCat.forget₂Mon_preservesLimitsOfSize`, `SemiRingCat.forget₂Mon_preservesLimits`, `hom_id`, `inv_hom_apply`, `hom_inv_apply`, `FilteredColimits.M.mk_surjective`
`instCategory` 📖	CompOp	92 math math: `CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `CommMonCat.forget₂_full`, `FilteredColimits.colimit_mul_mk_eq'`, `CategoryTheory.instFullMonFunctorOppositeMonCatYonedaMon`, `forget_map`, `forget_reflects_isos`, `AddMonCat.equivalence_functor_obj_coe`, `CommMonCat.coe_forget₂_obj`, `ext_iff`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply`, `forget_preservesLimitsOfSize`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply`, `forget_preservesLimitsOfShape`, `CategoryTheory.MonObj.ofRepresentableBy_one`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk`, `oneHom_apply`, `toCat_faithful`, `AddMonCat.equivalence_inverse_map`, `instIsRightAdjointForgetMonoidHomCarrier`, `AddMonCat.equivalence_counitIso`, `GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.M.map_mk`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `SemiRingCat.forget₂Mon_preservesLimitsOfSize`, `ofHom_comp`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `CategoryTheory.essImage_yonedaMon`, `CategoryTheory.yonedaMon_naturality_assoc`, `CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `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`, `adjoinOne_obj_coe`, `comp_apply`, `uliftFunctor_obj_coe`, `coe_comp`, `forget_isCorepresentable`, `HasLimits.hasLimit`, `adjoinOne_map`, `FilteredColimits.cocone_naturality`, `MulEquiv.toMonCatIso_hom`, `CategoryTheory.yonedaGrpObj_map`, `GrpCat.forget₂_map`, `FilteredColimits.forget_preservesFilteredColimits`, `HasLimits.hasLimitsOfShape`, `CategoryTheory.MonObj.ofRepresentableBy_mul`, `GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `uliftFunctor_map`, `toCat_full`, `val_units_map_hom_apply`, `hasLimitsOfSize`, `GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `Colimits.cocone_naturality_components`, `CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.colimit_one_eq`, `ofHom_id`, `coe_id`, `FilteredColimits.colimit_mul_mk_eq`, `val_inv_units_map_hom_apply`, `CommMonCat.forget₂Mon_preservesLimits`, `AddMonCat.equivalence_unitIso`, `units_obj_coe`, `Colimits.hasColimits_monCat`, `GrpCat.forget₂_map_ofHom`, `AddMonCat.equivalence_functor_map`, `hom_comp`, `forget_preservesLimits`, `CategoryTheory.yonedaGrp_map_app`, `SemiRingCat.forget₂_monCat_map`, `Colimits.cocone_naturality`, `instIsRightAdjointGrpCatMonCatUnits`, `id_apply`, `ofHom_apply`, `GrpCat.forget₂Mon_preservesLimitsOfSize`, `SemiRingCat.forget₂Mon_preservesLimits`, `hom_id`, `CategoryTheory.yonedaMon_obj`, `inv_hom_apply`, `hom_inv_apply`, `FilteredColimits.M.mk_surjective`, `hasLimits`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryMonoidHomCarrier` 📖	CompOp	50 math math: `CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `CommMonCat.forget₂_full`, `forget_map`, `forget_reflects_isos`, `CommMonCat.coe_forget₂_obj`, `ext_iff`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply`, `forget_preservesLimitsOfSize`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply`, `forget_preservesLimitsOfShape`, `CategoryTheory.MonObj.ofRepresentableBy_one`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk`, `instIsRightAdjointForgetMonoidHomCarrier`, `GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.M.map_mk`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `SemiRingCat.forget₂Mon_preservesLimitsOfSize`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `CategoryTheory.essImage_yonedaMon`, `CategoryTheory.yonedaMon_naturality_assoc`, `CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `CategoryTheory.yonedaMon_naturality`, `CommMonCat.forget₂_map_ofHom`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk`, `SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `GrpCat.forget₂Mon_preservesLimits`, `CommMonCat.hom_forget₂_map`, `CommMonCat.forget₂Mon_preservesLimitsOfSize`, `comp_apply`, `coe_comp`, `forget_isCorepresentable`, `GrpCat.forget₂_map`, `FilteredColimits.forget_preservesFilteredColimits`, `CategoryTheory.MonObj.ofRepresentableBy_mul`, `GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `Colimits.cocone_naturality_components`, `CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `coe_id`, `FilteredColimits.colimit_mul_mk_eq`, `CommMonCat.forget₂Mon_preservesLimits`, `GrpCat.forget₂_map_ofHom`, `forget_preservesLimits`, `SemiRingCat.forget₂_monCat_map`, `id_apply`, `ofHom_apply`, `GrpCat.forget₂Mon_preservesLimitsOfSize`, `SemiRingCat.forget₂Mon_preservesLimits`, `inv_hom_apply`, `hom_inv_apply`
`instInhabited` 📖	CompOp	—
`instOneHom` 📖	CompOp	2 math math: `oneHom_apply`, `hom_one`
`of` 📖	CompOp	10 math math: `coe_of`, `AddMonCat.equivalence_counitIso`, `ofHom_comp`, `MulEquiv.toMonCatIso_inv`, `hom_ofHom`, `MulEquiv.toMonCatIso_hom`, `ofHom_id`, `one_of`, `mul_of`, `ofHom_apply`
`ofHom` 📖	CompOp	15 math math: `AddMonCat.equivalence_counitIso`, `ofHom_comp`, `CategoryTheory.yonedaMonObj_map`, `CommMonCat.forget₂_map_ofHom`, `MulEquiv.toMonCatIso_inv`, `CategoryTheory.yonedaMon_map_app`, `hom_ofHom`, `adjoinOne_map`, `MulEquiv.toMonCatIso_hom`, `uliftFunctor_map`, `ofHom_id`, `GrpCat.forget₂_map_ofHom`, `AddMonCat.equivalence_functor_map`, `ofHom_hom`, `ofHom_apply`
`str` 📖	CompOp	66 math math: `CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `CommMonCat.forget₂_full`, `FilteredColimits.colimit_mul_mk_eq'`, `forget_map`, `forget_reflects_isos`, `CommMonCat.coe_forget₂_obj`, `ext_iff`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply`, `forget_preservesLimitsOfSize`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply`, `forget_preservesLimitsOfShape`, `CategoryTheory.MonObj.ofRepresentableBy_one`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_quotMk`, `oneHom_apply`, `AddMonCat.equivalence_inverse_map`, `instIsRightAdjointForgetMonoidHomCarrier`, `AddMonCat.equivalence_counitIso`, `GrpCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.M.map_mk`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `SemiRingCat.forget₂Mon_preservesLimitsOfSize`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `CategoryTheory.essImage_yonedaMon`, `CategoryTheory.yonedaMon_naturality_assoc`, `CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `hom_one`, `CategoryTheory.yonedaMon_naturality`, `CommMonCat.forget₂_map_ofHom`, `SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk`, `SemiRingCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `GrpCat.forget₂Mon_preservesLimits`, `CommMonCat.hom_forget₂_map`, `CommMonCat.forget₂Mon_preservesLimitsOfSize`, `comp_apply`, `coe_comp`, `forget_isCorepresentable`, `GrpCat.forget₂_map`, `FilteredColimits.forget_preservesFilteredColimits`, `CategoryTheory.MonObj.ofRepresentableBy_mul`, `GrpCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `uliftFunctor_map`, `GrpCat.FilteredColimits.colimit_mul_mk_eq`, `val_units_map_hom_apply`, `GrpCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `Colimits.cocone_naturality_components`, `CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `FilteredColimits.colimit_one_eq`, `coe_id`, `FilteredColimits.colimit_mul_mk_eq`, `val_inv_units_map_hom_apply`, `CommMonCat.forget₂Mon_preservesLimits`, `units_obj_coe`, `GrpCat.forget₂_map_ofHom`, `hom_comp`, `GrpCat.FilteredColimits.colimit_mul_mk_eq'`, `forget_preservesLimits`, `SemiRingCat.forget₂_monCat_map`, `ofHom_hom`, `GrpCat.FilteredColimits.colimit_one_eq`, `id_apply`, `ofHom_apply`, `GrpCat.forget₂Mon_preservesLimitsOfSize`, `SemiRingCat.forget₂Mon_preservesLimits`, `hom_id`, `inv_hom_apply`, `hom_inv_apply`
`uliftFunctor` 📖	CompOp	2 math math: `uliftFunctor_obj_coe`, `uliftFunctor_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`ext` 📖	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`ext`
`forget_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `MonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom`	—	—
`forget_reflects_isos` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `MonCat` `instCategory` `CategoryTheory.types` `CategoryTheory.forget` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier`	—	`Equiv.left_inv` `Equiv.right_inv` `MonoidHom.map_mul'` `CategoryTheory.Iso.isIso_hom`
`hom_comp` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.comp` `MonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `MonoidHom.comp` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_id` 📖	mathematical	—	`Hom.hom` `CategoryTheory.CategoryStruct.id` `MonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `MonoidHom.id` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str`	—	—
`hom_inv_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Iso.hom` `CategoryTheory.Iso.inv`	—	`CategoryTheory.Iso.inv_hom_id_apply`
`hom_ofHom` 📖	mathematical	—	`Hom.hom` `of` `ofHom`	—	—
`hom_one` 📖	mathematical	—	`Hom.hom` `Quiver.Hom` `MonCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instOneHom` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `instOneMonoidHom`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—
`inv_hom_apply` 📖	mathematical	—	`DFunLike.coe` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `CategoryTheory.Iso.inv` `CategoryTheory.Iso.hom`	—	`CategoryTheory.Iso.hom_inv_id_apply`
`mul_of` 📖	mathematical	—	`carrier` `of` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`ofHom_apply` 📖	mathematical	—	`DFunLike.coe` `of` `carrier` `CategoryTheory.ConcreteCategory.hom` `MonCat` `instCategory` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `instConcreteCategoryMonoidHomCarrier` `ofHom`	—	—
`ofHom_comp` 📖	mathematical	—	`ofHom` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.CategoryStruct.comp` `MonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`ofHom_hom` 📖	mathematical	—	`ofHom` `carrier` `str` `Hom.hom`	—	—
`ofHom_id` 📖	mathematical	—	`ofHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CategoryTheory.CategoryStruct.id` `MonCat` `CategoryTheory.Category.toCategoryStruct` `instCategory` `of`	—	—
`oneHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `carrier` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `str` `MonoidHom.instFunLike` `Hom.hom` `Quiver.Hom` `MonCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `instOneHom` `MulOne.toOne`	—	—
`one_of` 📖	mathematical	—	`carrier` `of` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—
`uliftFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `MonCat` `instCategory` `uliftFunctor` `ofHom` `carrier` `ULift.monoid` `str` `MonoidHom.comp` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `ULift.mulOneClass` `MulEquiv.toMonoidHom` `MulEquiv.symm` `ULift.mul` `MulOne.toMul` `MulEquiv.ulift` `Hom.hom`	—	—
`uliftFunctor_obj_coe` 📖	mathematical	—	`carrier` `CategoryTheory.Functor.obj` `MonCat` `instCategory` `uliftFunctor`	—	—

MonCat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	17 math math: `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply`, `CategoryTheory.yonedaMonObjIsoOfRepresentableBy_inv_app_hom_apply`, `MonCat.oneHom_apply`, `AddMonCat.equivalence_inverse_map`, `AddMonCat.equivalence_counitIso`, `MonCat.hom_one`, `CommMonCat.hom_forget₂_map`, `MonCat.hom_ofHom`, `CategoryTheory.yonedaGrpObj_map`, `MonCat.uliftFunctor_map`, `MonCat.val_units_map_hom_apply`, `MonCat.val_inv_units_map_hom_apply`, `MonCat.hom_comp`, `CategoryTheory.yonedaGrp_map_app`, `MonCat.ofHom_hom`, `MonCat.hom_ext_iff`, `MonCat.hom_id`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`

MonCat.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

MulEquiv

Definitions

Name	Category	Theorems
`toCommMonCatIso` 📖	CompOp	2 math math: `toCommMonCatIso_hom`, `toCommMonCatIso_inv`
`toMonCatIso` 📖	CompOp	2 math math: `toMonCatIso_inv`, `toMonCatIso_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toCommMonCatIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CommMonCat` `CommMonCat.instCategory` `CommMonCat.of` `toCommMonCatIso` `CommMonCat.ofHom` `toMonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	—
`toCommMonCatIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CommMonCat` `CommMonCat.instCategory` `CommMonCat.of` `toCommMonCatIso` `CommMonCat.ofHom` `toMonoidHom` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `symm` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`toMonCatIso_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `MonCat` `MonCat.instCategory` `MonCat.of` `toMonCatIso` `MonCat.ofHom` `toMonoidHom` `Monoid.toMulOneClass`	—	—
`toMonCatIso_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `MonCat` `MonCat.instCategory` `MonCat.of` `toMonCatIso` `MonCat.ofHom` `toMonoidHom` `Monoid.toMulOneClass` `symm` `MulOne.toMul` `MulOneClass.toMulOne`	—	—

(root)

Definitions

Name	Category	Theorems
`AddCommMonCat` 📖	CompData	64 math math: `AddCommMonCat.coyoneda_obj_obj_coe`, `AddCommMonCat.equivalence_unitIso`, `AddCommMonCat.free_obj_coe`, `SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier`, `AddCommMonCat.coe_id`, `AddCommMonCat.ofHom_apply`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `AddCommMonCat.hom_forget₂_map`, `AddCommMonCat.hasLimitsOfSize`, `AddCommMonCat.free_map`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `AddCommMonCat.coyonedaType_obj_map`, `AddCommMonCat.coyonedaType_map_app`, `SemimoduleCat.forget₂_obj_moduleCat_of`, `AddCommMonCat.equivalence_functor_map`, `AddCommMonCat.forget_preservesLimitsOfShape`, `AddCommMonCat.comp_apply`, `AddCommMonCat.forget₂_full`, `AddEquiv.toAddCommMonCatIso_inv`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddCommMonCat.forget_preservesLimits`, `AddCommMonCat.FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.neg_hom_apply`, `AddCommMonCat.forget₂Mon_preservesLimits`, `AddCommMonCat.ext_iff`, `AddCommMonCat.instIsLeftAdjointFree`, `AddCommMonCat.coe_comp`, `AddCommMonCat.coyoneda_map_app`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `AddCommMonCat.equivalence_inverse_obj_coe`, `AddCommMonCat.hom_neg_apply`, `AddCommMonCat.coe_forget₂_obj`, `AddCommMonCat.ofHom_comp`, `AddCommMonCat.coyonedaForget_inv_app_app`, `AddCommMonCat.coyonedaType_obj_obj_coe`, `AddCommMonCat.instIsRightAdjointForgetAddMonoidHomCarrier`, `SemiRingCat.forget₂AddCommMon_preservesLimits`, `AddCommMonCat.forget₂_map_ofHom`, `AddCommGrpCat.forget₂_commMonCat_map_ofHom`, `AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize`, `AddCommMonCat.forget_isCorepresentable`, `AddCommMonCat.equivalence_functor_obj_coe`, `AddCommMonCat.equivalence_counitIso`, `AddCommMonCat.forget_preservesLimitsOfSize`, `AddCommMonCat.uliftFunctor_obj_coe`, `AddCommMonCat.id_apply`, `AddCommMonCat.coyoneda_obj_map`, `AddCommMonCat.ofHom_id`, `SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize`, `AddCommMonCat.coyonedaForget_hom_app_app_hom`, `AddCommMonCat.equivalence_inverse_map`, `AddCommMonCat.hasLimitsOfShape`, `AddCommMonCat.hasLimits`, `AddCommMonCat.hom_comp`, `AddCommMonCat.hom_id`, `AddCommMonCat.forget_map`, `AddCommMonCat.forget_reflects_isos`, `SemimoduleCat.forget₂_obj`, `AddCommMonCat.uliftFunctor_map`, `SemimoduleCat.forget₂_map`, `AddEquiv.toAddCommMonCatIso_hom`, `SemiRingCat.forget₂_addCommMonCat_map`, `AddCommMonCat.hasLimit`
`AddMonCat` 📖	CompData	59 math math: `AddMonCat.hasLimitsOfSize`, `AddGrpCat.forget₂_map`, `AddMonCat.comp_apply`, `AddMonCat.FilteredColimits.M.mk_surjective`, `AddMonCat.uliftFunctor_map`, `AddEquiv.toAddMonCatIso_hom`, `AddMonCat.zeroHom_apply`, `AddMonCat.equivalence_functor_obj_coe`, `AddMonCat.forget_reflects_isos`, `AddMonCat.forget_preservesLimitsOfSize`, `AddMonCat.hom_zero`, `AddMonCat.ofHom_id`, `AddCommMonCat.FilteredColimits.forget₂AddMonPreservesFilteredColimits`, `AddMonCat.ext_iff`, `AddCommMonCat.hom_forget₂_map`, `AddMonCat.hom_comp`, `AddMonCat.FilteredColimits.colimit_add_mk_eq`, `AddMonCat.forget_preservesLimitsOfShape`, `AddCommMonCat.forget₂AddMonPreservesLimitsOfSize`, `AddMonCat.equivalence_inverse_map`, `AddMonCat.equivalence_counitIso`, `AddMonCat.forget_map`, `AddMonCat.coe_comp`, `AddEquiv.toAddMonCatIso_inv`, `AddGrpCat.forget₂AddMonPreservesLimitsOfSize`, `AddCommMonCat.forget₂_full`, `AddMonCat.FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddMonCat.FilteredColimits.colimit_zero_eq`, `AddMonCat.coe_id`, `AddMonCat.FilteredColimits.M.map_mk`, `AddCommMonCat.forget₂Mon_preservesLimits`, `AddMonCat.equivalence_inverse_obj_coe`, `AddMonCat.neg_hom_apply`, `AddMonCat.forget_isCorepresentable`, `AddMonCat.hom_id`, `AddMonCat.FilteredColimits.cocone_naturality`, `AddGrpCat.forget₂_map_ofHom`, `AddMonCat.id_apply`, `AddCommMonCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `AddMonCat.ofHom_apply`, `AddMonCat.HasLimits.hasLimitsOfShape`, `AddMonCat.FilteredColimits.colimit_add_mk_eq'`, `AddMonCat.hasLimits`, `AddCommMonCat.coe_forget₂_obj`, `AddMonCat.forget_preservesLimits`, `AddMonCat.adjoinZero_obj_coe`, `AddGrpCat.instSmallElemForallObjCompMonCatForget₂AddMonoidHomCarrierCarrierForgetSections`, `AddMonCat.ofHom_comp`, `AddMonCat.hom_neg_apply`, `AddGrpCat.FilteredColimits.forget₂AddMon_preservesFilteredColimits`, `AddCommMonCat.forget₂_map_ofHom`, `AddMonCat.equivalence_unitIso`, `AddMonCat.HasLimits.hasLimit`, `AddMonCat.uliftFunctor_obj_coe`, `AddMonCat.equivalence_functor_map`, `AddGrpCat.instFullMonCatForget₂AddMonoidHomCarrierCarrier`, `AddMonCat.adjoinZero_map`, `AddGrpCat.forget₂Mon_preservesLimits`
`CommMonCat` 📖	CompData	66 math math: `CommMonCat.instFullMonCatForget₂MonoidHomCarrierCarrier`, `MulEquiv.toCommMonCatIso_hom`, `CommMonCat.forget₂_full`, `AddCommMonCat.equivalence_unitIso`, `CommMonCat.forget_preservesLimitsOfShape`, `CommGrpCat.forget₂CommMon_preservesLimitsOfShape`, `CommMonCat.coe_forget₂_obj`, `CommMonCat.hom_comp`, `CommMonCat.coyonedaType_obj_map`, `CommMonCat.coe_comp`, `CommMonCat.coyoneda_obj_map`, `CommMonCat.forget_preservesLimitsOfSize`, `CommGrpCat.forget₂CommMon_preservesLimitsOfSize`, `CategoryTheory.IsCommMonObj.ofRepresentableBy`, `AddCommMonCat.equivalence_functor_map`, `CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier`, `CategoryTheory.IsCommMon.ofRepresentableBy`, `CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections`, `CommMonCat.val_units_map_hom_apply`, `CommMonCat.coyonedaForget_inv_app_app`, `CommMonCat.ofHom_comp`, `CommMonCat.val_inv_units_map_hom_apply`, `CommMonCat.forget₂_map_ofHom`, `CommMonCat.hasLimitsOfSize`, `CommMonCat.forget_map`, `CommMonCat.comp_apply`, `CommMonCat.hom_forget₂_map`, `CommMonCat.coyonedaType_obj_obj_coe`, `CommMonCat.forget₂Mon_preservesLimitsOfSize`, `CommMonCat.hasLimits`, `CommMonCat.inv_hom_apply`, `CommRingCat.commMon_forget₂_obj_coe`, `CommMonCat.coe_id`, `CommRingCat.monoidAlgebra_map`, `CommMonCat.hom_id`, `AddCommMonCat.equivalence_inverse_obj_coe`, `CommMonCat.uliftFunctor_obj_coe`, `CommMonCat.instIsRightAdjointForgetMonoidHomCarrier`, `CommMonCat.forget_reflects_isos`, `CommMonCat.forget_preservesLimits`, `CommMonCat.FilteredColimits.forget₂Mon_preservesFilteredColimits`, `CommMonCat.coyoneda_map_app`, `CommMonCat.coyoneda_obj_obj_coe`, `instIsRightAdjointCommGrpCatCommMonCatUnits`, `CommMonCat.hasLimit`, `CommMonCat.units_obj_coe`, `CommMonCat.id_apply`, `MulEquiv.toCommMonCatIso_inv`, `CommMonCat.forget₂Mon_preservesLimits`, `CommMonCat.coyonedaForget_hom_app_app_hom`, `CommMonCat.uliftFunctor_map`, `AddCommMonCat.equivalence_functor_obj_coe`, `AddCommMonCat.equivalence_counitIso`, `CommRingCat.instIsLeftAdjointCommMonCatUnderMonoidAlgebra`, `CommRingCat.monoidAlgebra_obj`, `CommRingCat.commMon_forget₂_map`, `CommGrpCat.forget₂_commMonCat_map_ofHom`, `CommMonCat.FilteredColimits.forget_preservesFilteredColimits`, `AddCommMonCat.equivalence_inverse_map`, `CommMonCat.ofHom_id`, `CommMonCat.ofHom_apply`, `CommMonCat.hasLimitsOfShape`, `CommMonCat.forget_isCorepresentable`, `CommMonCat.ext_iff`, `CommMonCat.coyonedaType_map_app`, `CommMonCat.hom_inv_apply`
`addEquivIsoAddCommMonCatIso` 📖	CompOp	—
`addEquivIsoAddMonCatIso` 📖	CompOp	—
`mulEquivIsoCommMonCatIso` 📖	CompOp	—
`mulEquivIsoMonCatIso` 📖	CompOp	—

---

← Back to Index