Limits

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

Statistics

Metric	Count
Definitions isColimitMapCocone	1
Theorems injective, surjective, isCardinalAccessible_of_isLimit, isCardinalPresentable_of_isColimit, isCardinalPresentable_of_isColimit', isClosedUnderColimitsOfShape_isCardinalPresentable	6
Total	7

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCardinalPresentable_of_isColimit 📖	mathematical	HasCardinalLT Arrow IsCardinalPresentable Functor.obj	Limits.Cocone.pt	—	isCardinalPresentable_of_isEquivalence Equivalence.isEquivalence_functor isCardinalPresentable_iff_of_isEquivalence isCardinalPresentable_of_isColimit' Limits.PreservesColimitsOfShape.preservesColimit Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence
isCardinalPresentable_of_isColimit' 📖	mathematical	HasCardinalLT Arrow IsCardinalPresentable Functor.obj	Limits.Cocone.pt	—	Functor.isCardinalAccessible_of_isLimit Limits.PreservesLimitsOfShape.preservesLimit Limits.PreservesLimitsOfSize.preservesLimitsOfShape coyonedaFunctor_preservesLimits
isClosedUnderColimitsOfShape_isCardinalPresentable 📖	mathematical	HasCardinalLT Arrow	ObjectProperty.IsClosedUnderColimitsOfShape isCardinalPresentable	—	ObjectProperty.ColimitOfShape.prop_diag_obj isCardinalPresentable_of_isColimit

CategoryTheory.Functor

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCardinalAccessible_of_isLimit 📖	mathematical	HasCardinalLT CategoryTheory.Arrow IsCardinalAccessible CategoryTheory.types obj CategoryTheory.Functor category	CategoryTheory.Limits.Cone.pt	—	preservesColimitsOfShape_of_isCardinalAccessible CategoryTheory.Limits.evaluation_preservesLimit CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit

CategoryTheory.Functor.Accessible.Limits

Definitions

Name	Category	Theorems
isColimitMapCocone 📖	CompOp	—

CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective 📖	—	HasCardinalLT CategoryTheory.Arrow CategoryTheory.Functor.map CategoryTheory.types CategoryTheory.Limits.Cone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι	—	—	CategoryTheory.isFiltered_of_isCardinalFiltered Equiv.symm_apply_apply CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow Equiv.injective CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply CategoryTheory.IsCardinalFiltered.coeq_condition CategoryTheory.Functor.map_comp CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.FunctorToTypes.naturality
surjective 📖	mathematical	HasCardinalLT CategoryTheory.Arrow	CategoryTheory.NatTrans.app CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Limits.Cone.pt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor.mapCocone CategoryTheory.Limits.Cocone.ι	—	CategoryTheory.isFiltered_of_isCardinalFiltered Equiv.surjective CategoryTheory.Limits.Types.jointly_surjective_of_isColimit CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow CategoryTheory.FunctorToTypes.map_comp_apply CategoryTheory.Limits.Cocone.w CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Category.assoc CategoryTheory.IsCardinalFiltered.coeq_condition CategoryTheory.Functor.map_comp CategoryTheory.FunctorToTypes.naturality Equiv.injective Equiv.apply_symm_apply CategoryTheory.Limits.Types.isLimitEquivSections_apply CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

---

← Back to Index