Yoneda

📁 Source: Mathlib/Algebra/Category/Grp/Yoneda.lean

Statistics

Metric	Count
Definitions coyoneda, coyonedaForget, coyonedaType, coyoneda, coyonedaForget, coyonedaType	6
Theorems coyonedaForget_hom_app_app_hom, coyonedaForget_inv_app_app, coyonedaType_map_app, coyonedaType_obj_map, coyonedaType_obj_obj_coe, coyoneda_map_app, coyoneda_obj_map, coyoneda_obj_obj_coe, coyonedaForget_hom_app_app_hom, coyonedaForget_inv_app_app, coyonedaType_map_app, coyonedaType_obj_map, coyonedaType_obj_obj_coe, coyoneda_map_app, coyoneda_obj_map, coyoneda_obj_obj_coe	16
Total	22

AddCommGrpCat

Definitions

Name	Category	Theorems
coyoneda 📖	CompOp	5 math math: coyoneda_obj_obj_coe, coyonedaForget_inv_app_app, coyonedaForget_hom_app_app_hom, coyoneda_map_app, coyoneda_obj_map
coyonedaForget 📖	CompOp	2 math math: coyonedaForget_inv_app_app, coyonedaForget_hom_app_app_hom
coyonedaType 📖	CompOp	3 math math: coyonedaType_obj_map, coyonedaType_obj_obj_coe, coyonedaType_map_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyonedaForget_hom_app_app_hom 📖	mathematical	—	Hom.hom Opposite.unop AddCommGrpCat CategoryTheory.NatTrans.app instCategory CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.coyoneda CategoryTheory.Iso.hom coyonedaForget	—	—
coyonedaForget_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommGrpCat instCategory CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda CategoryTheory.Functor.comp coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.forget AddMonoidHom carrier AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Iso.inv coyonedaForget Hom.hom Opposite.unop	—	—
coyonedaType_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommGrpCat instCategory of Pi.addCommGroup Opposite.unop carrier str ofHom Pi.addMonoidHom AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Pi.addZeroClass AddMonoidHom.comp AddZeroClass.toAddZero Hom.hom Pi.evalAddMonoidHom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coyonedaType_obj_map 📖	mathematical	—	CategoryTheory.Functor.map AddCommGrpCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType ofHom Pi.addCommGroup Opposite.unop carrier str Pi.addMonoidHom AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Pi.addZeroClass AddMonoidHom.comp AddZeroClass.toAddZero Hom.hom Pi.evalAddMonoidHom	—	—
coyonedaType_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj AddCommGrpCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType	—	—
coyoneda_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommGrpCat instCategory of AddMonoidHom carrier Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instAddCommGroup ofHom DFunLike.coe AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid AddMonoidHom.instAddCommMonoid AddMonoidHom.instFunLike AddMonoidHom.compHom Hom.hom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda AddMonoidHom.compHom' Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coyoneda_obj_map 📖	mathematical	—	CategoryTheory.Functor.map AddCommGrpCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda ofHom AddMonoidHom carrier Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str AddMonoidHom.instAddCommGroup DFunLike.coe AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid AddMonoidHom.instAddCommMonoid AddMonoidHom.instFunLike AddMonoidHom.compHom Hom.hom	—	—
coyoneda_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj AddCommGrpCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda AddMonoidHom Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup str	—	—

CommGrpCat

Definitions

Name	Category	Theorems
coyoneda 📖	CompOp	5 math math: coyonedaForget_hom_app_app_hom, coyoneda_obj_obj_coe, coyonedaForget_inv_app_app, coyoneda_obj_map, coyoneda_map_app
coyonedaForget 📖	CompOp	2 math math: coyonedaForget_hom_app_app_hom, coyonedaForget_inv_app_app
coyonedaType 📖	CompOp	3 math math: coyonedaType_map_app, coyonedaType_obj_map, coyonedaType_obj_obj_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyonedaForget_hom_app_app_hom 📖	mathematical	—	Hom.hom Opposite.unop CommGrpCat CategoryTheory.NatTrans.app instCategory CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.coyoneda CategoryTheory.Iso.hom coyonedaForget	—	—
coyonedaForget_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommGrpCat instCategory CategoryTheory.types CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.coyoneda CategoryTheory.Functor.comp coyoneda CategoryTheory.Functor.whiskeringRight CategoryTheory.forget MonoidHom carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.Iso.inv coyonedaForget Hom.hom Opposite.unop	—	—
coyonedaType_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommGrpCat instCategory of Pi.commGroup Opposite.unop carrier str ofHom Pi.monoidHom Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pi.mulOneClass MonoidHom.comp MulOneClass.toMulOne Hom.hom Pi.evalMonoidHom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coyonedaType_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CommGrpCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType ofHom Pi.commGroup Opposite.unop carrier str Pi.monoidHom Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup Pi.mulOneClass MonoidHom.comp MulOneClass.toMulOne Hom.hom Pi.evalMonoidHom	—	—
coyonedaType_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj CommGrpCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType	—	—
coyoneda_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommGrpCat instCategory of MonoidHom carrier Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instCommGroup ofHom DFunLike.coe CommMonoid.toMonoid CommGroup.toCommMonoid MonoidHom.instCommMonoid MonoidHom.instFunLike MonoidHom.compHom Hom.hom CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda MonoidHom.compHom' Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
coyoneda_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CommGrpCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda ofHom MonoidHom carrier Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str MonoidHom.instCommGroup DFunLike.coe CommMonoid.toMonoid CommGroup.toCommMonoid MonoidHom.instCommMonoid MonoidHom.instFunLike MonoidHom.compHom Hom.hom	—	—
coyoneda_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj CommGrpCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda MonoidHom Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup str	—	—

---

← Back to Index