LocallySmall

📁 Source: Mathlib/CategoryTheory/Limits/Indization/LocallySmall.lean

Statistics

Metric	Count
Definitions colimitYonedaHomEquiv	1
Theorems colimitYonedaHomEquiv_π_apply, instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject, instSmallHomFunctorOppositeTypeColimitCompYoneda	3
Total	4

CategoryTheory

Definitions

Name	Category	Theorems
colimitYonedaHomEquiv 📖	CompOp	1 math math: colimitYonedaHomEquiv_π_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitYonedaHomEquiv_π_apply 📖	mathematical	—	Limits.limit.π Opposite Category.opposite types Functor.comp Functor.op Limits.hasLimitOfHasLimitsOfShape DFunLike.coe Equiv Quiver.Hom Functor CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Limits.colimit yoneda Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Functor.obj Functor.flip Limits.limit EquivLike.toFunLike Equiv.instEquivLike colimitYonedaHomEquiv NatTrans.app Opposite.op Opposite.unop Limits.colimit.ι CategoryStruct.id	—	Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Limits.hasLimitOfHasLimitsOfShape Iso.trans_assoc Limits.instHasLimitCompOfPreservesLimit Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesLimitsOfSize.preservesLimitsOfShape Limits.Types.instPreservesLimitsOfSizeUliftFunctor preservesLimitIso_inv_π types_comp_apply Limits.HasLimit.isoOfNatIso_hom_π Limits.colimitYonedaHomIsoLimitOp_π_apply
instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject 📖	mathematical	—	LocallySmall ObjectProperty.FullSubcategory Functor Opposite Category.opposite types Functor.category Limits.IsIndObject ObjectProperty.FullSubcategory.category	—	ObjectProperty.FullSubcategory.property Limits.functorCategoryHasColimit Limits.Types.hasColimit UnivLE.small UnivLE.self small_map instSmallHomFunctorOppositeTypeColimitCompYoneda Limits.Types.hasColimitsOfShape Limits.Types.hasLimitsOfShape Opposite.small univLE_of_max
instSmallHomFunctorOppositeTypeColimitCompYoneda 📖	mathematical	—	Small Quiver.Hom Functor Opposite Category.opposite types CategoryStruct.toQuiver Category.toCategoryStruct Functor.category Limits.colimit Functor.comp yoneda Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Functor.obj Functor.flip	—	Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Limits.hasLimitOfHasLimitsOfShape

---

← Back to Index