Small

📁 Source: Mathlib/CategoryTheory/Comma/StructuredArrow/Small.lean

Statistics

Metric	Count
Definitions Small, Small, Small	3
Theorems essentiallySmall, instSmallOfLocallySmall, small_inverseImage_proj_of_locallySmall, small_proj_preimage_of_locallySmall, essentiallySmall, instSmallOfLocallySmall, small_inverseImage_proj_of_locallySmall, small_proj_preimage_of_locallySmall	8
Total	11

CategoryTheory.CostructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essentiallySmall 📖	mathematical	—	CategoryTheory.EssentiallySmall CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.essentiallySmall_congr isEquivalence_pre CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.essentiallySmall_of_small_of_locallySmall instSmallOfLocallySmall UnivLE.small UnivLE.self CategoryTheory.locallySmall_of_univLE
instSmallOfLocallySmall 📖	mathematical	—	Small CategoryTheory.CostructuredArrow	—	small_of_surjective small_sigma CategoryTheory.instSmallHomOfLocallySmall mk_surjective
small_inverseImage_proj_of_locallySmall 📖	mathematical	—	CategoryTheory.ObjectProperty.Small CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	CategoryTheory.ObjectProperty.instSmallOfObjOfSmall small_sigma CategoryTheory.instSmallHomOfLocallySmall
small_proj_preimage_of_locallySmall 📖	mathematical	—	CategoryTheory.ObjectProperty.Small CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	small_inverseImage_proj_of_locallySmall

CategoryTheory.FunctorToTypes

Definitions

Name	Category	Theorems
Small 📖	MathDef	1 math math: CategoryTheory.instSmallOppositeObjFunctorTypeYoneda

CategoryTheory.Precoverage

Definitions

Name	Category	Theorems
Small 📖	CompData	6 math math: CategoryTheory.MorphismProperty.instSmallPrecoverage, TopCat.instSmallPrecoverage, AlgebraicGeometry.Scheme.instSmallPrecoverage, Small.inf, CategoryTheory.Types.instSmallJointlySurjectivePrecoverage, instSmallComap

CategoryTheory.Precoverage.ZeroHypercover

Definitions

Name	Category	Theorems
Small 📖	CompData	5 math math: instSmallOfSmallI₀, CategoryTheory.Precoverage.Small.zeroHypercoverSmall, instSmall, CategoryTheory.Precoverage.instSmallOfSmall, instSmallPullback₁

CategoryTheory.StructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essentiallySmall 📖	mathematical	—	CategoryTheory.EssentiallySmall CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.essentiallySmall_congr isEquivalence_pre CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.essentiallySmall_of_small_of_locallySmall instSmallOfLocallySmall UnivLE.small UnivLE.self CategoryTheory.locallySmall_of_univLE
instSmallOfLocallySmall 📖	mathematical	—	Small CategoryTheory.StructuredArrow	—	small_of_surjective small_sigma CategoryTheory.instSmallHomOfLocallySmall mk_surjective
small_inverseImage_proj_of_locallySmall 📖	mathematical	—	CategoryTheory.ObjectProperty.Small CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	CategoryTheory.ObjectProperty.instSmallOfObjOfSmall small_sigma CategoryTheory.instSmallHomOfLocallySmall
small_proj_preimage_of_locallySmall 📖	mathematical	—	CategoryTheory.ObjectProperty.Small CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.ObjectProperty.inverseImage proj	—	small_inverseImage_proj_of_locallySmall

---

← Back to Index