ShrinkYoneda

📁 Source: Mathlib/CategoryTheory/ShrinkYoneda.lean

Statistics

Metric	Count
Definitions shrink, shrinkMap, fullyFaithfulShrinkYoneda, shrinkYoneda, shrinkYonedaEquiv, shrinkYonedaObjObjEquiv	6
Theorems shrinkMap_app, shrink_map, shrink_obj, instFaithfulFunctorOppositeTypeShrinkYoneda, instFullFunctorOppositeTypeShrinkYoneda, instSmallOppositeObjFunctorTypeYoneda, map_shrinkYonedaEquiv, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_naturality, shrinkYonedaEquiv_shrinkYoneda_map, shrinkYonedaEquiv_symm_map, shrinkYonedaEquiv_symm_map_assoc, shrinkYoneda_map, shrinkYoneda_obj	14
Total	20

CategoryTheory

Definitions

Name	Category	Theorems
fullyFaithfulShrinkYoneda 📖	CompOp	—
shrinkYoneda 📖	CompOp	10 math math: shrinkYoneda_map, shrinkYonedaEquiv_comp, shrinkYonedaEquiv_symm_map_assoc, shrinkYoneda_obj, shrinkYonedaEquiv_naturality, instFaithfulFunctorOppositeTypeShrinkYoneda, instFullFunctorOppositeTypeShrinkYoneda, map_shrinkYonedaEquiv, shrinkYonedaEquiv_symm_map, shrinkYonedaEquiv_shrinkYoneda_map
shrinkYonedaEquiv 📖	CompOp	6 math math: shrinkYonedaEquiv_comp, shrinkYonedaEquiv_symm_map_assoc, shrinkYonedaEquiv_naturality, map_shrinkYonedaEquiv, shrinkYonedaEquiv_symm_map, shrinkYonedaEquiv_shrinkYoneda_map
shrinkYonedaObjObjEquiv 📖	CompOp	2 math math: map_shrinkYonedaEquiv, shrinkYonedaEquiv_shrinkYoneda_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulFunctorOppositeTypeShrinkYoneda 📖	mathematical	—	Functor.Faithful Functor Opposite Category.opposite types Functor.category shrinkYoneda	—	Functor.FullyFaithful.faithful
instFullFunctorOppositeTypeShrinkYoneda 📖	mathematical	—	Functor.Full Functor Opposite Category.opposite types Functor.category shrinkYoneda	—	Functor.FullyFaithful.full
instSmallOppositeObjFunctorTypeYoneda 📖	mathematical	—	FunctorToTypes.Small Opposite Category.opposite Functor.obj Functor types Functor.category yoneda	—	instSmallHomOfLocallySmall
map_shrinkYonedaEquiv 📖	mathematical	—	Functor.map Opposite Category.opposite types Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom Functor Functor.category Functor.obj shrinkYoneda EquivLike.toFunLike Equiv.instEquivLike shrinkYonedaEquiv NatTrans.app Opposite.unop Equiv.symm shrinkYonedaObjObjEquiv	—	instSmallOppositeObjFunctorTypeYoneda Equiv.symm_apply_apply Category.comp_id
shrinkYonedaEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj shrinkYoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike shrinkYonedaEquiv CategoryStruct.comp NatTrans.app	—	—
shrinkYonedaEquiv_naturality 📖	mathematical	—	Functor.map Opposite Category.opposite types Opposite.op Quiver.Hom.op CategoryStruct.toQuiver Category.toCategoryStruct DFunLike.coe Equiv Quiver.Hom Functor Functor.category Functor.obj shrinkYoneda EquivLike.toFunLike Equiv.instEquivLike shrinkYonedaEquiv CategoryStruct.comp	—	instSmallOppositeObjFunctorTypeYoneda Equiv.symm_apply_apply Category.id_comp Category.comp_id NatTrans.naturality
shrinkYonedaEquiv_shrinkYoneda_map 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Functor.obj shrinkYoneda Opposite.op EquivLike.toFunLike Equiv.instEquivLike shrinkYonedaEquiv Functor.map Opposite.unop Equiv.symm shrinkYonedaObjObjEquiv	—	instSmallOppositeObjFunctorTypeYoneda Equiv.symm_apply_apply Category.id_comp
shrinkYonedaEquiv_symm_map 📖	mathematical	—	DFunLike.coe Equiv Functor.obj Opposite Category.opposite types Opposite.op Opposite.unop Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category shrinkYoneda EquivLike.toFunLike Equiv.instEquivLike Equiv.symm shrinkYonedaEquiv Functor.map CategoryStruct.comp Quiver.Hom.unop	—	Equiv.injective Equiv.surjective shrinkYonedaEquiv_naturality Equiv.apply_symm_apply Equiv.symm_apply_apply
shrinkYonedaEquiv_symm_map_assoc 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite types Category.toCategoryStruct Functor.category Functor.obj shrinkYoneda Opposite.unop DFunLike.coe Equiv Opposite.op Quiver.Hom CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm shrinkYonedaEquiv Functor.map Quiver.Hom.unop	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shrinkYonedaEquiv_symm_map
shrinkYoneda_map 📖	mathematical	—	Functor.map Functor Opposite Category.opposite types Functor.category shrinkYoneda FunctorToTypes.shrinkMap Functor.obj yoneda instSmallOppositeObjFunctorTypeYoneda	—	instSmallOppositeObjFunctorTypeYoneda
shrinkYoneda_obj 📖	mathematical	—	Functor.obj Functor Opposite Category.opposite types Functor.category shrinkYoneda FunctorToTypes.shrink yoneda instSmallOppositeObjFunctorTypeYoneda	—	—

CategoryTheory.FunctorToTypes

Definitions

Name	Category	Theorems
shrink 📖	CompOp	4 math math: shrinkMap_app, CategoryTheory.shrinkYoneda_obj, shrink_map, shrink_obj
shrinkMap 📖	CompOp	2 math math: CategoryTheory.shrinkYoneda_map, shrinkMap_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
shrinkMap_app 📖	mathematical	Small	CategoryTheory.NatTrans.app CategoryTheory.types shrink shrinkMap CategoryTheory.Functor.obj DFunLike.coe Equiv Shrink EquivLike.toFunLike Equiv.instEquivLike equivShrink Equiv.symm	—	—
shrink_map 📖	mathematical	Small	CategoryTheory.Functor.map CategoryTheory.types shrink Shrink CategoryTheory.Functor.obj DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike equivShrink Equiv.symm	—	—
shrink_obj 📖	mathematical	Small	CategoryTheory.Functor.obj CategoryTheory.types shrink Shrink	—	—

---

← Back to Index