Basic

📁 Source: Mathlib/CategoryTheory/Presentable/Basic.lean

Statistics

Metric	Count
Definitions IsAccessible, IsCardinalAccessible, HasCardinalFilteredColimits, IsCardinalPresentable, IsPresentable, isCardinalPresentable	6
Theorems exists_cardinal, preservesColimitOfShape, instIsAccessibleComp, instIsAccessibleObjConst, instIsCardinalAccessibleComp, instIsCardinalAccessibleId, instIsCardinalAccessibleObjConst, instIsCardinalAccessibleOfPreservesColimitsOfSize, isAccessible_of_isCardinalAccessible, isCardinalAccessible_of_le, isCardinalAccessible_of_natIso, preservesColimitsOfShape_of_isCardinalAccessible, preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall, hasColimitsOfShape, exists_eq_of_isColimit, exists_eq_of_isColimit', exists_hom_of_isColimit, instHasCardinalFilteredColimitsOfHasColimitsOfSize, instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable, instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, instIsCardinalPresentableObjIsCardinalPresentable, instIsClosedUnderIsomorphismsIsCardinalPresentable, isCardinalPresentable_iff, isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj, isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj, isCardinalPresentable_iff_of_isEquivalence, isCardinalPresentable_monotone, isCardinalPresentable_of_equivalence, isCardinalPresentable_of_isEquivalence, isCardinalPresentable_of_iso, isCardinalPresentable_of_le, isPresentable_of_isCardinalPresentable, preservesColimitsOfShape_of_isCardinalPresentable, preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall	34
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
HasCardinalFilteredColimits 📖	CompData	4 math math: IsCardinalAccessibleCategory.toHasCardinalFilteredColimits, HasCardinalFilteredColimits_iff_hasFilteredColimitsOfSize, instHasCardinalFilteredColimitsOfHasColimitsOfSize, HasCardinalFilteredColimits_iff_hasFilteredColimits
IsCardinalPresentable 📖	MathDef	17 math math: Presheaf.instIsCardinalPresentableFunctorOppositeFreeYonedaOfHasColimitsOfSize, instIsCardinalPresentableObjIsCardinalPresentable, isCardinalPresentable_of_isEquivalence, isCardinalPresentable_of_iso, Adjunction.isCardinalPresentable_leftAdjoint_obj, ObjectProperty.ColimitOfShape.isCardinalPresentable, Types.isCardinalPresentable_iff, isCardinalPresentable_iff_of_isEquivalence, isCardinalPresentable_iff, isCardinalPresentable_of_le, Presheaf.instIsCardinalPresentableFunctorOppositeTypeObjUliftYonedaOfHasColimitsOfSize, isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj, instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj, isCardinalPresentable_of_equivalence, Retract.isCardinalPresentable, HasCardinalLT.isCardinalPresentable
IsPresentable 📖	MathDef	4 math math: instIsPresentableOfIsAccessibleCategory, ObjectProperty.IsCardinalFilteredGenerator.presentable, isPresentable_of_isCardinalPresentable, Types.instIsPresentable
isCardinalPresentable 📖	CompOp	17 math math: instIsCardinalPresentableObjIsCardinalPresentable, instIsStableUnderRetractsIsCardinalPresentable, IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, instIsClosedUnderIsomorphismsIsCardinalPresentable, IsCardinalAccessibleCategory.final_toCostructuredArrow, isCardinalPresentable_monotone, ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, ObjectProperty.IsCardinalFilteredGenerator.isPresentable_eq_retractClosure, isCardinalPresentable_iff, instEssentiallySmallIsCardinalPresentableOfHasCardinalFilteredGenerator, ObjectProperty.IsCardinalFilteredGenerator.essentiallySmall_isPresentable, IsCardinalAccessibleCategory.instIsDenseFullSubcategoryIsCardinalPresentableι, instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι, isClosedUnderColimitsOfShape_isCardinalPresentable, IsCardinalAccessibleCategory.instIsCardinalFilteredCostructuredArrowFullSubcategoryIsCardinalPresentableι, ObjectProperty.isFinitelyPresentable_eq_isCardinalPresentable, isCardinalFilteredGenerator_isCardinalPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasCardinalFilteredColimitsOfHasColimitsOfSize 📖	mathematical	—	HasCardinalFilteredColimits	—	Limits.hasColimitsOfShapeOfHasColimitsOfSize
instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable 📖	mathematical	—	Functor.IsCardinalAccessible types Functor.obj Opposite Category.opposite Functor Functor.category uliftCoyoneda Opposite.op	—	isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj
instIsCardinalPresentableObjFullSubcategoryIsCardinalPresentableι 📖	mathematical	—	IsCardinalPresentable Functor.obj ObjectProperty.FullSubcategory isCardinalPresentable ObjectProperty.FullSubcategory.category ObjectProperty.ι	—	instIsCardinalPresentableObjIsCardinalPresentable
instIsCardinalPresentableObjIsCardinalPresentable 📖	mathematical	—	IsCardinalPresentable ObjectProperty.FullSubcategory.obj isCardinalPresentable	—	ObjectProperty.FullSubcategory.property
instIsClosedUnderIsomorphismsIsCardinalPresentable 📖	mathematical	—	ObjectProperty.IsClosedUnderIsomorphisms isCardinalPresentable	—	isCardinalPresentable_iff isCardinalPresentable_of_iso
isCardinalPresentable_iff 📖	mathematical	—	isCardinalPresentable IsCardinalPresentable	—	—
isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj 📖	mathematical	—	IsCardinalPresentable Functor.IsCardinalAccessible types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	—
isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj 📖	mathematical	—	IsCardinalPresentable Functor.IsCardinalAccessible types Functor.obj Opposite Category.opposite Functor Functor.category uliftCoyoneda Opposite.op	—	Functor.instIsCardinalAccessibleComp Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize Limits.Types.instPreservesColimitsOfSizeUliftFunctor Functor.preservesColimitsOfShape_of_isCardinalAccessible Limits.preservesColimitsOfShape_of_reflects_of_preserves Limits.reflectsColimitsOfShape_of_reflectsColimits Limits.fullyFaithful_reflectsColimits uliftFunctor_full uliftFunctor_faithful
isCardinalPresentable_iff_of_isEquivalence 📖	mathematical	—	IsCardinalPresentable Functor.obj	—	isCardinalPresentable_of_iso isCardinalPresentable_of_isEquivalence Functor.isEquivalence_inv
isCardinalPresentable_monotone 📖	mathematical	Cardinal Cardinal.instLE	ObjectProperty Category.toCategoryStruct Pi.hasLe Prop.le isCardinalPresentable	—	isCardinalPresentable_iff isCardinalPresentable_of_le
isCardinalPresentable_of_equivalence 📖	mathematical	—	IsCardinalPresentable Functor.obj Equivalence.functor	—	preservesColimitsOfShape_of_isCardinalPresentable types_ext Adjunction.homEquiv_unit Functor.map_comp Category.assoc Limits.preservesColimit_of_natIso Limits.comp_preservesColimit Limits.PreservesColimitsOfShape.preservesColimit Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Equivalence.isEquivalence_inverse preservesColimit_comp_of_createsColimit Limits.comp_preservesColimitsOfShape Limits.PreservesColimitsOfSize.preservesColimitsOfShape Limits.Types.instPreservesColimitsOfSizeUliftFunctor Limits.reflectsColimit_of_reflectsColimitsOfShape Limits.reflectsColimitsOfShape_of_reflectsColimits Limits.fullyFaithful_reflectsColimits uliftFunctor_full uliftFunctor_faithful
isCardinalPresentable_of_isEquivalence 📖	mathematical	—	IsCardinalPresentable Functor.obj	—	isCardinalPresentable_of_equivalence
isCardinalPresentable_of_iso 📖	mathematical	—	IsCardinalPresentable	—	Functor.isCardinalAccessible_of_natIso
isCardinalPresentable_of_le 📖	mathematical	Cardinal Cardinal.instLE	IsCardinalPresentable	—	Functor.isCardinalAccessible_of_le
isPresentable_of_isCardinalPresentable 📖	mathematical	—	IsPresentable	—	—
preservesColimitsOfShape_of_isCardinalPresentable 📖	mathematical	—	Limits.PreservesColimitsOfShape types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	Functor.preservesColimitsOfShape_of_isCardinalAccessible
preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall 📖	mathematical	—	Limits.PreservesColimitsOfShape types Functor.obj Opposite Category.opposite Functor Functor.category coyoneda Opposite.op	—	Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall

CategoryTheory.Functor

Definitions

Name	Category	Theorems
IsAccessible 📖	CompData	3 math math: isAccessible_of_isCardinalAccessible, instIsAccessibleComp, instIsAccessibleObjConst
IsCardinalAccessible 📖	CompData	11 math math: instIsCardinalAccessibleOfPreservesColimitsOfSize, isCardinalAccessible_of_natIso, IsAccessible.exists_cardinal, instIsCardinalAccessibleComp, instIsCardinalAccessibleObjConst, isCardinalAccessible_of_le, instIsCardinalAccessibleId, CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_coyoneda_obj, CategoryTheory.isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj, CategoryTheory.MorphismProperty.isCardinalAccessible_ι_isLocal, CategoryTheory.instIsCardinalAccessibleObjOppositeFunctorTypeUliftCoyonedaOpOfIsCardinalPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsAccessibleComp 📖	mathematical	—	IsAccessible comp	—	IsAccessible.exists_cardinal Fact.out isCardinalAccessible_of_le isAccessible_of_isCardinalAccessible instIsCardinalAccessibleComp
instIsAccessibleObjConst 📖	mathematical	—	IsAccessible obj CategoryTheory.Functor category const	—	Cardinal.fact_isRegular_aleph0 instIsCardinalAccessibleObjConst
instIsCardinalAccessibleComp 📖	mathematical	—	IsCardinalAccessible comp	—	preservesColimitsOfShape_of_isCardinalAccessible CategoryTheory.Limits.comp_preservesColimitsOfShape
instIsCardinalAccessibleId 📖	mathematical	—	IsCardinalAccessible id	—	instPreservesColimitsOfShapeOfIsLeftAdjoint isLeftAdjoint_of_isEquivalence isEquivalence_refl
instIsCardinalAccessibleObjConst 📖	mathematical	—	IsCardinalAccessible obj CategoryTheory.Functor category const	—	CategoryTheory.isFiltered_of_isCardinalFiltered CategoryTheory.IsIso.id CategoryTheory.IsFiltered.nonempty
instIsCardinalAccessibleOfPreservesColimitsOfSize 📖	mathematical	—	IsCardinalAccessible	—	CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
isAccessible_of_isCardinalAccessible 📖	mathematical	—	IsAccessible	—	—
isCardinalAccessible_of_le 📖	mathematical	Cardinal Cardinal.instLE	IsCardinalAccessible	—	CategoryTheory.IsCardinalFiltered.of_le preservesColimitsOfShape_of_isCardinalAccessible
isCardinalAccessible_of_natIso 📖	mathematical	—	IsCardinalAccessible	—	preservesColimitsOfShape_of_isCardinalAccessible CategoryTheory.Limits.preservesColimitsOfShape_of_natIso
preservesColimitsOfShape_of_isCardinalAccessible 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	IsCardinalAccessible.preservesColimitOfShape
preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	CategoryTheory.IsCardinalFiltered.of_equivalence preservesColimitsOfShape_of_isCardinalAccessible CategoryTheory.Limits.preservesColimitsOfShape_of_equiv

CategoryTheory.Functor.IsAccessible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_cardinal 📖	mathematical	—	CategoryTheory.Functor.IsCardinalAccessible	—	—

CategoryTheory.Functor.IsCardinalAccessible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
preservesColimitOfShape 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape	—	—

CategoryTheory.HasCardinalFilteredColimits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape	—	—

CategoryTheory.IsCardinalPresentable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_eq_of_isColimit 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Functor.map	—	CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall CategoryTheory.isFiltered_of_isCardinalFiltered CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
exists_eq_of_isColimit' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	CategoryTheory.Functor.map	—	CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall CategoryTheory.isFiltered_of_isCardinalFiltered CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit
exists_hom_of_isColimit 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit

---

← Back to Index