ShrinkYoneda

📁 Source: Mathlib/CategoryTheory/Monoidal/Cartesian/ShrinkYoneda.lean

Statistics

Metric	Count
Definitions shrinkYonedaGrp, shrinkYonedaGrpObjObjEquiv, shrinkYonedaMon, shrinkYonedaMonObjObjEquiv	4
Theorems instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp, instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon, shrinkYonedaGrpObjObjEquiv_symm_comp, shrinkYonedaGrp_map, shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm, shrinkYonedaGrp_obj, shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm, shrinkYonedaMonObjObjEquiv_symm_comp, shrinkYonedaMon_map, shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm, shrinkYonedaMon_obj, shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm	12
Total	16

CategoryTheory

Definitions

Name	Category	Theorems
shrinkYonedaGrp 📖	CompOp	5 math math: shrinkYonedaGrp_obj, shrinkYonedaGrp_map, shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm, shrinkYonedaGrpObjObjEquiv_symm_comp, shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm
shrinkYonedaGrpObjObjEquiv 📖	CompOp	3 math math: shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm, shrinkYonedaGrpObjObjEquiv_symm_comp, shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm
shrinkYonedaMon 📖	CompOp	6 math math: shrinkYonedaMonObjObjEquiv_symm_comp, shrinkYonedaMon_map, shrinkYonedaMon_obj, shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm, instPreservesLimitsOfShapeMonFunctorOppositeMonCatShrinkYonedaMon, shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm
shrinkYonedaMonObjObjEquiv 📖	CompOp	3 math math: shrinkYonedaMonObjObjEquiv_symm_comp, shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm, shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp 📖	mathematical	—	Small GrpCat.carrier Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory Grp Grp.instCategory Functor Functor.category yonedaGrp	—	instSmallHomOfLocallySmall
instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon 📖	mathematical	—	Small MonCat.carrier Functor.obj Opposite Category.opposite MonCat MonCat.instCategory Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Functor.category yonedaMon	—	instSmallHomOfLocallySmall
shrinkYonedaGrpObjObjEquiv_symm_comp 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Opposite.op Grp.X GrpCat.carrier Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory Grp Grp.instCategory Functor Functor.category shrinkYonedaGrp MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Hom.monoid GrpObj.toMonObj Grp.grp DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaGrpObjObjEquiv CategoryStruct.comp ConcreteCategory.hom MonoidHom MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier Functor.map Quiver.Hom.op	—	shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm
shrinkYonedaGrp_map 📖	mathematical	—	Functor.map Grp Grp.instCategory Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category shrinkYonedaGrp GrpCat.shrinkFunctorMap Functor.obj yonedaGrp instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp	—	instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp
shrinkYonedaGrp_map_app_shrinkYonedaObjObjEquiv_symm 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory Grp Grp.instCategory Functor Functor.category shrinkYonedaGrp GrpCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier NatTrans.app Functor.map MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Grp.X MulOne.toMul Hom.monoid GrpObj.toMonObj Grp.grp EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaGrpObjObjEquiv CategoryStruct.comp Mon.Hom.hom SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Grp.toMon InducedCategory.Hom.hom Mon Mon.instCategory	—	instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp MulEquiv.apply_symm_apply
shrinkYonedaGrp_obj 📖	mathematical	—	Functor.obj Grp Grp.instCategory Functor Opposite Category.opposite GrpCat GrpCat.instCategory Functor.category shrinkYonedaGrp GrpCat.shrinkFunctor yonedaGrp instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp	—	—
shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite GrpCat GrpCat.instCategory Grp Grp.instCategory Functor Functor.category shrinkYonedaGrp GrpCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid GrpCat.str MonoidHom.instFunLike GrpCat.instConcreteCategoryMonoidHomCarrier Functor.map MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Grp.X MulOne.toMul Hom.monoid GrpObj.toMonObj Grp.grp EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaGrpObjObjEquiv CategoryStruct.comp Quiver.Hom.unop	—	instSmallCarrierObjOppositeGrpCatGrpFunctorYonedaGrp MulEquiv.apply_symm_apply
shrinkYonedaMonObjObjEquiv_symm_comp 📖	mathematical	—	DFunLike.coe MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Opposite.op Mon.X SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory MonCat.carrier Functor.obj Opposite Category.opposite MonCat MonCat.instCategory Mon Mon.instCategory Functor Functor.category shrinkYonedaMon MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Hom.monoid Mon.mon MonCat.str EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaMonObjObjEquiv CategoryStruct.comp ConcreteCategory.hom MonoidHom MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier Functor.map Quiver.Hom.op	—	shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm
shrinkYonedaMon_map 📖	mathematical	—	Functor.map Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category shrinkYonedaMon MonCat.shrinkFunctorMap Functor.obj yonedaMon instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon	—	instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon
shrinkYonedaMon_map_app_shrinkYonedaObjObjEquiv_symm 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite MonCat MonCat.instCategory Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Functor.category shrinkYonedaMon MonCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier NatTrans.app Functor.map MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Mon.X MulOne.toMul Hom.monoid Mon.mon EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaMonObjObjEquiv CategoryStruct.comp Mon.Hom.hom	—	instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon MulEquiv.apply_symm_apply
shrinkYonedaMon_obj 📖	mathematical	—	Functor.obj Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Opposite Category.opposite MonCat MonCat.instCategory Functor.category shrinkYonedaMon MonCat.shrinkFunctor yonedaMon instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon	—	—
shrinkYonedaMon_obj_map_shrinkYonedaMonObjObjEquiv_symm 📖	mathematical	—	DFunLike.coe Functor.obj Opposite Category.opposite MonCat MonCat.instCategory Mon SemiCartesianMonoidalCategory.toMonoidalCategory CartesianMonoidalCategory.toSemiCartesianMonoidalCategory Mon.instCategory Functor Functor.category shrinkYonedaMon MonCat.carrier ConcreteCategory.hom MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass MonCat.str MonoidHom.instFunLike MonCat.instConcreteCategoryMonoidHomCarrier Functor.map MulEquiv Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct Opposite.unop Mon.X MulOne.toMul Hom.monoid Mon.mon EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm shrinkYonedaMonObjObjEquiv CategoryStruct.comp Quiver.Hom.unop	—	instSmallCarrierObjOppositeMonCatMonFunctorYonedaMon MulEquiv.apply_symm_apply

---

← Back to Index