Yoneda

📁 Source: Mathlib/Algebra/Category/MonCat/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

AddCommMonCat

Definitions

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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coyonedaForget_hom_app_app_hom 📖	mathematical	—	Hom.hom Opposite.unop AddCommMonCat 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 AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.coyoneda CategoryTheory.Iso.hom coyonedaForget	—	—
coyonedaForget_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommMonCat 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 AddCommMonoid.toAddMonoid str AddMonoidHom.instFunLike instConcreteCategoryAddMonoidHomCarrier CategoryTheory.Iso.inv coyonedaForget Hom.hom Opposite.unop	—	—
coyonedaType_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommMonCat instCategory of Pi.addCommMonoid Opposite.unop carrier str ofHom Pi.addMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid 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 AddCommMonCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType ofHom Pi.addCommMonoid Opposite.unop carrier str Pi.addMonoidHom AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Pi.addZeroClass AddMonoidHom.comp AddZeroClass.toAddZero Hom.hom Pi.evalAddMonoidHom	—	—
coyonedaType_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj AddCommMonCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType	—	—
coyoneda_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app AddCommMonCat instCategory of AddMonoidHom carrier Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instAddCommMonoid ofHom DFunLike.coe 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 AddCommMonCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda ofHom AddMonoidHom carrier Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str AddMonoidHom.instAddCommMonoid DFunLike.coe AddMonoidHom.instFunLike AddMonoidHom.compHom Hom.hom	—	—
coyoneda_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj AddCommMonCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda AddMonoidHom Opposite.unop AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid str	—	—

CommMonCat

Definitions

Name	Category	Theorems
coyoneda 📖	CompOp	5 math math: coyoneda_obj_map, coyonedaForget_inv_app_app, coyoneda_map_app, coyoneda_obj_obj_coe, coyonedaForget_hom_app_app_hom
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 CommMonCat 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 CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.coyoneda CategoryTheory.Iso.hom coyonedaForget	—	—
coyonedaForget_inv_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommMonCat 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 CommMonoid.toMonoid str MonoidHom.instFunLike instConcreteCategoryMonoidHomCarrier CategoryTheory.Iso.inv coyonedaForget Hom.hom Opposite.unop	—	—
coyonedaType_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommMonCat instCategory of Pi.commMonoid Opposite.unop carrier str ofHom Pi.monoidHom Monoid.toMulOneClass CommMonoid.toMonoid 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 CommMonCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType ofHom Pi.commMonoid Opposite.unop carrier str Pi.monoidHom Monoid.toMulOneClass CommMonoid.toMonoid Pi.mulOneClass MonoidHom.comp MulOneClass.toMulOne Hom.hom Pi.evalMonoidHom	—	—
coyonedaType_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj CommMonCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category coyonedaType	—	—
coyoneda_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CommMonCat instCategory of MonoidHom carrier Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instCommMonoid ofHom DFunLike.coe 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 CommMonCat instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda ofHom MonoidHom carrier Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str MonoidHom.instCommMonoid DFunLike.coe MonoidHom.instFunLike MonoidHom.compHom Hom.hom	—	—
coyoneda_obj_obj_coe 📖	mathematical	—	carrier CategoryTheory.Functor.obj CommMonCat instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category coyoneda MonoidHom Opposite.unop MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid str	—	—

---

← Back to Index