LocallySmall

📁 Source: Mathlib/CategoryTheory/Localization/LocallySmall.lean

Statistics

Metric	Count
Definitions LocallySmall, hasLocalizationOfLocallySmall, hasLocalizationOfLocallySmall'	3
Theorems hasLocalizationOfLocallySmall'_def, locallySmall_of_hasLocalization	2
Total	5

CategoryTheory

Definitions

Name	Category	Theorems
LocallySmall 📖	CompData	30 math math: IsGrothendieckAbelian.locallySmall, locallySmall_fullSubcategory, instLocallySmallFunctor, locallySmall_max, locallySmall_of_thin, Shrink.instLocallySmallShrink, instLocallySmallSmallModel, essentiallySmall_iff, Over.locallySmall, Limits.ColimitPresentation.instLocallySmallTotal, locallySmall_of_essentiallySmall, instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject, CountableCategory.instLocallySmallObjAsType, CategoryOfElements.instLocallySmallElements, Limits.WalkingMultispan.instLocallySmall, locallySmall_of_univLE, locallySmall_of_faithful, SmallObject.locallySmall, locallySmall_congr, Under.locallySmall, instLocallySmallOpposite, Comma.locallySmall, StructuredArrow.locallySmall, HomologicalComplex.locallySmall, locallySmall_of_small_arrow, MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall, HasCardinalFilteredGenerator.toLocallySmall, MorphismProperty.locallySmall_of_hasLocalization, CostructuredArrow.locallySmall, locallySmall_self

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
hasLocalizationOfLocallySmall 📖	CompOp	—
hasLocalizationOfLocallySmall' 📖	CompOp	1 math math: hasLocalizationOfLocallySmall'_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLocalizationOfLocallySmall'_def 📖	mathematical	—	hasLocalizationOfLocallySmall'	—	CategoryTheory.Localization.essSurj
locallySmall_of_hasLocalization 📖	mathematical	—	CategoryTheory.LocallySmall	—	small_of_injective instIsLocalizationLocalization'Q' CategoryTheory.instSmallHomOfLocallySmall CategoryTheory.locallySmall_of_univLE UnivLE.self CategoryTheory.Functor.map_injective CategoryTheory.Equivalence.faithful_functor

---

← Back to Index