Shrink

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

Statistics

Metric	Count
Definitions shrinkFunctor, shrinkFunctorMap	2
Theorems shrinkFunctorMap_app, shrinkFunctor_map, shrinkFunctor_obj_coe, instSmallCompMonCatForgetMonoidHomCarrierOfSmallObj	4
Total	6

MonCat

Definitions

Name	Category	Theorems
shrinkFunctor 📖	CompOp	4 math math: shrinkFunctor_obj_coe, shrinkFunctorMap_app, CategoryTheory.shrinkYonedaMon_obj, shrinkFunctor_map
shrinkFunctorMap 📖	CompOp	2 math math: CategoryTheory.shrinkYonedaMon_map, shrinkFunctorMap_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shrinkFunctorMap_app 📖	mathematical	Small carrier CategoryTheory.Functor.obj MonCat instCategory	CategoryTheory.NatTrans.app MonCat instCategory shrinkFunctor shrinkFunctorMap ofHom Shrink carrier CategoryTheory.Functor.obj Shrink.instMonoid str MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass Shrink.instMulOneClass MulEquiv.toMonoidHom MulEquiv.symm Shrink.instMul MulOne.toMul Shrink.mulEquiv Hom.hom	—	—
shrinkFunctor_map 📖	mathematical	Small carrier CategoryTheory.Functor.obj MonCat instCategory	CategoryTheory.Functor.map MonCat instCategory shrinkFunctor ofHom Shrink carrier CategoryTheory.Functor.obj Shrink.instMonoid str MonoidHom.comp MulOneClass.toMulOne Monoid.toMulOneClass Shrink.instMulOneClass MulEquiv.toMonoidHom MulEquiv.symm Shrink.instMul MulOne.toMul Shrink.mulEquiv Hom.hom	—	—
shrinkFunctor_obj_coe 📖	mathematical	Small carrier CategoryTheory.Functor.obj MonCat instCategory	carrier CategoryTheory.Functor.obj MonCat instCategory shrinkFunctor Shrink	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSmallCompMonCatForgetMonoidHomCarrierOfSmallObj 📖	mathematical	Small MonCat.carrier CategoryTheory.Functor.obj MonCat MonCat.instCategory	CategoryTheory.FunctorToTypes.Small CategoryTheory.Functor.comp MonCat MonCat.instCategory CategoryTheory.types CategoryTheory.forget MonoidHom MonCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier	—	—

---

← Back to Index