Shrink

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

Statistics

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

GrpCat

Definitions

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

Theorems

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

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSmallCompGrpCatForgetMonoidHomCarrierOfSmallObj 📖	mathematical	Small GrpCat.carrier CategoryTheory.Functor.obj GrpCat GrpCat.instCategory	CategoryTheory.FunctorToTypes.Small CategoryTheory.Functor.comp GrpCat GrpCat.instCategory CategoryTheory.types CategoryTheory.forget MonoidHom GrpCat.carrier MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier	—	—

---

← Back to Index