FinallySmall

📁 Source: Mathlib/CategoryTheory/Limits/FinallySmall.lean

Statistics

Metric	Count
Definitions FinalModel, FinallySmall, InitialModel, InitiallySmall, fromFinalModel, fromInitialModel, smallCategoryFinalModel, smallCategoryInitialModel	8
Theorems exists_small_weakly_terminal_set, final_smallCategory, mk', exists_small_weakly_initial_set, initial_smallCategory, mk', hasColimitsOfShape_of_finallySmall, hasLimitsOfShape_of_initiallySmall, final_fromFinalModel, finallySmall_iff_exists_small_weakly_terminal_set, finallySmall_of_essentiallySmall, finallySmall_of_final_of_essentiallySmall, finallySmall_of_final_of_finallySmall, finallySmall_of_small_weakly_terminal_set, initial_fromInitialModel, initiallySmall_iff_exists_small_weakly_initial_set, initiallySmall_of_essentiallySmall, initiallySmall_of_initial_of_essentiallySmall, initiallySmall_of_initial_of_initiallySmall, initiallySmall_of_small_weakly_initial_set, instFinallySmallOfHasTerminal, instFinallySmallOppositeOfInitiallySmall, instInitiallySmallOfHasInitial, instInitiallySmallOppositeOfFinallySmall, instInitiallySmallOverOfLocallySmall	25
Total	33

CategoryTheory

Definitions

Name	Category	Theorems
FinalModel 📖	CompOp	1 math math: final_fromFinalModel
FinallySmall 📖	CompData	10 math math: finallySmall_of_small_weakly_terminal_set, instFinallySmallOfHasTerminal, Limits.isIndObject_iff, Limits.IsIndObject.finallySmall, finallySmall_of_final_of_finallySmall, finallySmall_of_essentiallySmall, instFinallySmallOppositeOfInitiallySmall, finallySmall_of_final_of_essentiallySmall, FinallySmall.mk', finallySmall_iff_exists_small_weakly_terminal_set
InitialModel 📖	CompOp	1 math math: initial_fromInitialModel
InitiallySmall 📖	CompData	10 math math: initiallySmall_of_initial_of_initiallySmall, instInitiallySmallOverOfLocallySmall, initiallySmall_of_small_weakly_initial_set, initiallySmall_of_essentiallySmall, instInitiallySmallOfHasInitial, initiallySmall_of_initial_of_essentiallySmall, InitiallySmall.mk', initiallySmall_iff_exists_small_weakly_initial_set, instInitiallySmallOppositeOfFinallySmall, GrothendieckTopology.Point.initiallySmall
fromFinalModel 📖	CompOp	1 math math: final_fromFinalModel
fromInitialModel 📖	CompOp	1 math math: initial_fromInitialModel
smallCategoryFinalModel 📖	CompOp	1 math math: final_fromFinalModel
smallCategoryInitialModel 📖	CompOp	1 math math: initial_fromInitialModel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
final_fromFinalModel 📖	mathematical	—	Functor.Final FinalModel smallCategoryFinalModel fromFinalModel	—	FinallySmall.final_smallCategory
finallySmall_iff_exists_small_weakly_terminal_set 📖	mathematical	—	FinallySmall Set Set.instMembership Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	—	FinallySmall.exists_small_weakly_terminal_set finallySmall_of_small_weakly_terminal_set
finallySmall_of_essentiallySmall 📖	mathematical	—	FinallySmall	—	FinallySmall.mk' Functor.final_of_isRightAdjoint Functor.isRightAdjoint_of_isEquivalence Equivalence.isEquivalence_inverse
finallySmall_of_final_of_essentiallySmall 📖	mathematical	—	FinallySmall	—	finallySmall_of_essentiallySmall finallySmall_of_final_of_finallySmall
finallySmall_of_final_of_finallySmall 📖	mathematical	—	FinallySmall	—	Functor.final_comp final_fromFinalModel FinallySmall.mk'
finallySmall_of_small_weakly_terminal_set 📖	mathematical	Set Set.instMembership Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	FinallySmall	—	Functor.final_of_exists_of_isFiltered_of_fullyFaithful ObjectProperty.full_ι ObjectProperty.faithful_ι finallySmall_of_final_of_essentiallySmall essentiallySmall_fullSubcategory_mem locallySmall_of_univLE UnivLE.self
initial_fromInitialModel 📖	mathematical	—	Functor.Initial InitialModel smallCategoryInitialModel fromInitialModel	—	InitiallySmall.initial_smallCategory
initiallySmall_iff_exists_small_weakly_initial_set 📖	mathematical	—	InitiallySmall Set Set.instMembership Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	—	InitiallySmall.exists_small_weakly_initial_set initiallySmall_of_small_weakly_initial_set
initiallySmall_of_essentiallySmall 📖	mathematical	—	InitiallySmall	—	InitiallySmall.mk' Functor.initial_of_isLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Equivalence.isEquivalence_inverse
initiallySmall_of_initial_of_essentiallySmall 📖	mathematical	—	InitiallySmall	—	initiallySmall_of_essentiallySmall initiallySmall_of_initial_of_initiallySmall
initiallySmall_of_initial_of_initiallySmall 📖	mathematical	—	InitiallySmall	—	Functor.initial_comp initial_fromInitialModel InitiallySmall.mk'
initiallySmall_of_small_weakly_initial_set 📖	mathematical	Set Set.instMembership Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct	InitiallySmall	—	Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful ObjectProperty.full_ι ObjectProperty.faithful_ι initiallySmall_of_initial_of_essentiallySmall essentiallySmall_fullSubcategory_mem locallySmall_of_univLE UnivLE.self
instFinallySmallOfHasTerminal 📖	mathematical	—	FinallySmall	—	Functor.final_const_terminal isFiltered_of_directed_le_nonempty OrderTop.instIsDirectedOrder FinallySmall.mk'
instFinallySmallOppositeOfInitiallySmall 📖	mathematical	—	FinallySmall Opposite Category.opposite	—	Functor.final_op_of_initial initial_fromInitialModel
instInitiallySmallOfHasInitial 📖	mathematical	—	InitiallySmall	—	Functor.initial_const_initial isCofiltered_of_directed_ge_nonempty OrderBot.instIsCodirectedOrder InitiallySmall.mk'
instInitiallySmallOppositeOfFinallySmall 📖	mathematical	—	InitiallySmall Opposite Category.opposite	—	Functor.initial_op_of_final final_fromFinalModel
instInitiallySmallOverOfLocallySmall 📖	mathematical	—	InitiallySmall Over instCategoryOver	—	initiallySmall_of_essentiallySmall CostructuredArrow.essentiallySmall essentiallySmall_of_small_of_locallySmall UnivLE.small UnivLE.self locallySmall_of_univLE initiallySmall_of_initial_of_initiallySmall instInitialCostructuredArrowOverToOver initial_fromInitialModel

CategoryTheory.FinallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_small_weakly_terminal_set 📖	mathematical	—	Set Set.instMembership Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	small_range UnivLE.small UnivLE.self CategoryTheory.IsConnected.is_nonempty CategoryTheory.Functor.Final.out CategoryTheory.final_fromFinalModel Set.mem_range_self
final_smallCategory 📖	mathematical	—	CategoryTheory.Functor.Final	—	—
mk' 📖	mathematical	—	CategoryTheory.FinallySmall	—	—

CategoryTheory.InitiallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_small_weakly_initial_set 📖	mathematical	—	Set Set.instMembership Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	small_range UnivLE.small UnivLE.self CategoryTheory.IsConnected.is_nonempty CategoryTheory.Functor.Initial.out CategoryTheory.initial_fromInitialModel Set.mem_range_self
initial_smallCategory 📖	mathematical	—	CategoryTheory.Functor.Initial	—	—
mk' 📖	mathematical	—	CategoryTheory.InitiallySmall	—	—

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimitsOfShape_of_finallySmall 📖	mathematical	—	HasColimitsOfShape	—	CategoryTheory.Functor.Final.hasColimitsOfShape_of_final CategoryTheory.final_fromFinalModel hasColimitsOfShapeOfHasColimitsOfSize
hasLimitsOfShape_of_initiallySmall 📖	mathematical	—	HasLimitsOfShape	—	CategoryTheory.Functor.Initial.hasLimitsOfShape_of_initial CategoryTheory.initial_fromInitialModel hasLimitsOfShapeOfHasLimits

---

← Back to Index