EssentiallySmall

📁 Source: Mathlib/CategoryTheory/EssentiallySmall.lean

Statistics

Metric	Count
Definitions `equivalence`, `instCategoryShrink`, `ShrinkHoms`, `equivalence`, `fromShrinkHoms`, `functor`, `instCategory`, `instUnique`, `inverse`, `toShrinkHoms`, `SmallModel`, `equivSmallModel`, `smallCategorySmallModel`	13
Theorems `essentiallySmallOfSmall`, `equiv_smallCategory`, `mk'`, `hom_small`, `instLocallySmallShrink`, `comp_def`, `equivalence_counitIso`, `equivalence_functor`, `equivalence_inverse`, `equivalence_unitIso`, `from_to`, `functor_map`, `functor_obj`, `id_def`, `instIsDiscrete`, `instIsEquivalenceFunctor`, `instIsEquivalenceInverse`, `inverse_map`, `inverse_obj`, `to_from`, `essentiallySmallSelf`, `essentiallySmall_congr`, `essentiallySmall_fullSubcategory_mem`, `essentiallySmall_iff`, `essentiallySmall_iff_of_thin`, `essentiallySmall_of_fully_faithful`, `essentiallySmall_of_small_of_locallySmall`, `instEssentiallySmallOpposite`, `instLocallySmallFunctor`, `instLocallySmallOpposite`, `instLocallySmallSmallModel`, `instSmallArrowOfLocallySmall`, `instSmallDiscrete`, `instSmallFunctorOfLocallySmall`, `instSmallHomOfLocallySmall`, `locallySmall_congr`, `locallySmall_fullSubcategory`, `locallySmall_max`, `locallySmall_of_essentiallySmall`, `locallySmall_of_faithful`, `locallySmall_of_thin`, `locallySmall_of_univLE`, `locallySmall_self`, `small_skeleton_of_essentiallySmall`	44
Total	57

CategoryTheory

Definitions

Name	Category	Theorems
`ShrinkHoms` 📖	CompOp	20 math math: `ShrinkHoms.id_def`, `ShrinkHoms.isGrothendieckAbelian`, `ShrinkHoms.instIsDiscrete`, `hasCardinalLT_arrow_shrinkHoms_iff`, `ShrinkHoms.equivalence_functor`, `ShrinkHoms.hasFiniteLimits`, `instWellPoweredShrinkHoms`, `ShrinkHoms.hasLimitsOfShape`, `ShrinkHoms.instAdditiveInverse`, `ShrinkHoms.equivalence_counitIso`, `ShrinkHoms.instIsEquivalenceInverse`, `ShrinkHoms.comp_def`, `ShrinkHoms.inverse_map`, `ShrinkHoms.equivalence_inverse`, `ShrinkHoms.instIsEquivalenceFunctor`, `ShrinkHoms.functor_map`, `ShrinkHoms.functor_obj`, `ShrinkHoms.equivalence_unitIso`, `ShrinkHoms.inverse_obj`, `ShrinkHoms.instAdditiveFunctor`
`SmallModel` 📖	CompOp	5 math math: `Equivalence.precoherent_isSheaf_iff_of_essentiallySmall`, `instLocallySmallSmallModel`, `Equivalence.instPrecoherentSmallModel`, `Equivalence.preregular_isSheaf_iff_of_essentiallySmall`, `Equivalence.instPreregularSmallModel`
`equivSmallModel` 📖	CompOp	2 math math: `Equivalence.precoherent_isSheaf_iff_of_essentiallySmall`, `Equivalence.preregular_isSheaf_iff_of_essentiallySmall`
`smallCategorySmallModel` 📖	CompOp	5 math math: `Equivalence.precoherent_isSheaf_iff_of_essentiallySmall`, `instLocallySmallSmallModel`, `Equivalence.instPrecoherentSmallModel`, `Equivalence.preregular_isSheaf_iff_of_essentiallySmall`, `Equivalence.instPreregularSmallModel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essentiallySmallSelf` 📖	mathematical	—	`EssentiallySmall`	—	`EssentiallySmall.mk'`
`essentiallySmall_congr` 📖	mathematical	—	`EssentiallySmall`	—	`EssentiallySmall.mk'`
`essentiallySmall_fullSubcategory_mem` 📖	mathematical	—	`EssentiallySmall` `ObjectProperty.FullSubcategory` `Set` `Set.instMembership` `ObjectProperty.FullSubcategory.category`	—	`small_of_injective` `ObjectProperty.FullSubcategory.property` `ObjectProperty.FullSubcategory.ext` `essentiallySmall_of_small_of_locallySmall` `locallySmall_fullSubcategory`
`essentiallySmall_iff` 📖	mathematical	—	`EssentiallySmall` `Small` `Skeleton` `LocallySmall`	—	`locallySmall_of_essentiallySmall` `Equivalence.inducedFunctorOfEquiv`
`essentiallySmall_iff_of_thin` 📖	mathematical	`Quiver.IsThin` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	`EssentiallySmall` `Small` `Skeleton`	—	—
`essentiallySmall_of_fully_faithful` 📖	mathematical	—	`EssentiallySmall`	—	`essentiallySmall_iff` `small_of_injective` `small_skeleton_of_essentiallySmall` `Functor.mapSkeleton_injective` `locallySmall_of_faithful` `locallySmall_of_essentiallySmall`
`essentiallySmall_of_small_of_locallySmall` 📖	mathematical	—	`EssentiallySmall`	—	`essentiallySmall_iff` `small_of_surjective`
`instEssentiallySmallOpposite` 📖	mathematical	—	`EssentiallySmall` `Opposite` `Category.opposite`	—	`EssentiallySmall.mk'`
`instLocallySmallFunctor` 📖	mathematical	—	`LocallySmall` `Functor` `Functor.category`	—	`small_of_injective` `small_Pi` `UnivLE.small` `UnivLE.self` `instSmallHomOfLocallySmall` `NatTrans.ext'`
`instLocallySmallOpposite` 📖	mathematical	—	`LocallySmall` `Opposite` `Category.opposite`	—	`small_of_injective` `instSmallHomOfLocallySmall` `Equiv.injective`
`instLocallySmallSmallModel` 📖	mathematical	—	`LocallySmall` `SmallModel` `smallCategorySmallModel`	—	`locallySmall_congr`
`instSmallArrowOfLocallySmall` 📖	mathematical	—	`Small` `Arrow`	—	`small_of_injective` `small_sigma` `instSmallHomOfLocallySmall`
`instSmallDiscrete` 📖	mathematical	—	`Small` `Discrete`	—	`small_map`
`instSmallFunctorOfLocallySmall` 📖	mathematical	—	`Small` `Functor`	—	`small_of_injective` `small_Pi` `instSmallArrowOfLocallySmall` `Functor.ext` `Arrow.mk_eq_mk_iff`
`instSmallHomOfLocallySmall` 📖	mathematical	—	`Small` `Quiver.Hom` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	—	`LocallySmall.hom_small`
`locallySmall_congr` 📖	mathematical	—	`LocallySmall`	—	`locallySmall_of_faithful` `Equivalence.faithful_inverse` `Equivalence.faithful_functor`
`locallySmall_fullSubcategory` 📖	mathematical	—	`LocallySmall` `ObjectProperty.FullSubcategory` `ObjectProperty.FullSubcategory.category`	—	`locallySmall_of_faithful` `ObjectProperty.faithful_ι`
`locallySmall_max` 📖	mathematical	—	`LocallySmall`	—	`small_max`
`locallySmall_of_essentiallySmall` 📖	mathematical	—	`LocallySmall`	—	`locallySmall_congr` `locallySmall_self`
`locallySmall_of_faithful` 📖	mathematical	—	`LocallySmall`	—	`small_of_injective` `instSmallHomOfLocallySmall` `Functor.map_injective`
`locallySmall_of_thin` 📖	mathematical	`Quiver.IsThin` `CategoryStruct.toQuiver` `Category.toCategoryStruct`	`LocallySmall`	—	`small_subsingleton`
`locallySmall_of_univLE` 📖	mathematical	—	`LocallySmall`	—	`UnivLE.small`
`locallySmall_self` 📖	mathematical	—	`LocallySmall`	—	`UnivLE.small` `UnivLE.self`
`small_skeleton_of_essentiallySmall` 📖	mathematical	—	`Small` `Skeleton`	—	`essentiallySmall_iff`

CategoryTheory.Discrete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`essentiallySmallOfSmall` 📖	mathematical	—	`CategoryTheory.EssentiallySmall` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory`	—	—

CategoryTheory.EssentiallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equiv_smallCategory` 📖	mathematical	—	`CategoryTheory.Equivalence`	—	—
`mk'` 📖	mathematical	—	`CategoryTheory.EssentiallySmall`	—	—

CategoryTheory.LocallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_small` 📖	mathematical	—	`Small` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct`	—	—

CategoryTheory.Shrink

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	—
`instCategoryShrink` 📖	CompOp	2 math math: `instLocallySmallShrink`, `CategoryTheory.hasCardinalLT_arrow_shrink_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallySmallShrink` 📖	mathematical	—	`CategoryTheory.LocallySmall` `Shrink` `instCategoryShrink`	—	`CategoryTheory.locallySmall_of_faithful` `CategoryTheory.Equivalence.faithful_inverse`

CategoryTheory.ShrinkHoms

Definitions

Name	Category	Theorems
`equivalence` 📖	CompOp	4 math math: `equivalence_functor`, `equivalence_counitIso`, `equivalence_inverse`, `equivalence_unitIso`
`fromShrinkHoms` 📖	CompOp	6 math math: `id_def`, `to_from`, `from_to`, `comp_def`, `inverse_map`, `inverse_obj`
`functor` 📖	CompOp	7 math math: `equivalence_functor`, `equivalence_counitIso`, `instIsEquivalenceFunctor`, `functor_map`, `functor_obj`, `equivalence_unitIso`, `instAdditiveFunctor`
`instCategory` 📖	CompOp	20 math math: `id_def`, `isGrothendieckAbelian`, `instIsDiscrete`, `CategoryTheory.hasCardinalLT_arrow_shrinkHoms_iff`, `equivalence_functor`, `hasFiniteLimits`, `CategoryTheory.instWellPoweredShrinkHoms`, `hasLimitsOfShape`, `instAdditiveInverse`, `equivalence_counitIso`, `instIsEquivalenceInverse`, `comp_def`, `inverse_map`, `equivalence_inverse`, `instIsEquivalenceFunctor`, `functor_map`, `functor_obj`, `equivalence_unitIso`, `inverse_obj`, `instAdditiveFunctor`
`instUnique` 📖	CompOp	—
`inverse` 📖	CompOp	7 math math: `instAdditiveInverse`, `equivalence_counitIso`, `instIsEquivalenceInverse`, `inverse_map`, `equivalence_inverse`, `equivalence_unitIso`, `inverse_obj`
`toShrinkHoms` 📖	CompOp	3 math math: `to_from`, `from_to`, `functor_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShrinkHoms` `CategoryTheory.Category.toCategoryStruct` `instCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `fromShrinkHoms` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink` `Equiv.symm`	—	—
`equivalence_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `CategoryTheory.ShrinkHoms` `instCategory` `equivalence` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.comp` `inverse` `functor` `CategoryTheory.Functor.id` `CategoryTheory.Iso.refl` `CategoryTheory.Functor.obj`	—	—
`equivalence_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CategoryTheory.ShrinkHoms` `instCategory` `equivalence` `functor`	—	—
`equivalence_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CategoryTheory.ShrinkHoms` `instCategory` `equivalence` `inverse`	—	—
`equivalence_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `CategoryTheory.ShrinkHoms` `instCategory` `equivalence` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `functor` `inverse` `CategoryTheory.Iso.refl` `CategoryTheory.Functor.obj`	—	—
`from_to` 📖	mathematical	—	`toShrinkHoms` `fromShrinkHoms`	—	—
`functor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShrinkHoms` `instCategory` `functor` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Shrink` `CategoryTheory.instSmallHomOfLocallySmall` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	`CategoryTheory.instSmallHomOfLocallySmall`
`functor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShrinkHoms` `instCategory` `functor` `toShrinkHoms`	—	—
`id_def` 📖	mathematical	—	`CategoryTheory.CategoryStruct.id` `CategoryTheory.ShrinkHoms` `CategoryTheory.Category.toCategoryStruct` `instCategory` `DFunLike.coe` `Equiv` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `fromShrinkHoms` `Shrink` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivShrink`	—	—
`instIsDiscrete` 📖	mathematical	—	`CategoryTheory.IsDiscrete` `CategoryTheory.ShrinkHoms` `instCategory` `CategoryTheory.locallySmall_of_univLE` `univLE_of_max` `UnivLE.self`	—	`CategoryTheory.locallySmall_of_univLE` `univLE_of_max` `UnivLE.self` `Shrink.ext` `CategoryTheory.IsDiscrete.subsingleton` `CategoryTheory.IsDiscrete.eq_of_hom`
`instIsEquivalenceFunctor` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.ShrinkHoms` `instCategory` `functor`	—	`CategoryTheory.Equivalence.isEquivalence_functor`
`instIsEquivalenceInverse` 📖	mathematical	—	`CategoryTheory.Functor.IsEquivalence` `CategoryTheory.ShrinkHoms` `instCategory` `inverse`	—	`CategoryTheory.Equivalence.isEquivalence_inverse`
`inverse_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShrinkHoms` `instCategory` `inverse` `DFunLike.coe` `Equiv` `Shrink` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `fromShrinkHoms` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivShrink`	—	—
`inverse_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShrinkHoms` `instCategory` `inverse` `fromShrinkHoms`	—	—
`to_from` 📖	mathematical	—	`fromShrinkHoms` `toShrinkHoms`	—	—

---

← Back to Index