IndObject

📁 Source: Mathlib/CategoryTheory/Limits/Indization/IndObject.lean

Statistics

Metric	Count
Definitions IndObjectPresentation, F, I, cocone, coconeIsColimit, extend, instSmallCategoryI, isColimit, ofCocone, toCostructuredArrow, yoneda, ι, ℐ, IsIndObject, presentation	15
Theorems cocone_pt, extend_F, extend_I, extend_isColimit_desc_app, extend_ι_app_app, extend_ℐ, hI, instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, instIsFilteredI, ofCocone_F, ofCocone_I, ofCocone_isColimit, ofCocone_ι, ofCocone_ℐ, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, toCostructuredArrow_obj_left, toCostructuredArrow_obj_right_as, yoneda_F, yoneda_I, yoneda_isColimit_desc, yoneda_ι_app, yoneda_ℐ, finallySmall, iff_of_iso, instIsClosedUnderIsomorphismsFunctorOppositeType, isFiltered, map, mk, nonempty_presentation, isIndObject_iff, isIndObject_iff_preservesFiniteLimits, isIndObject_limit_comp_yoneda, isIndObject_of_isFiltered_of_finallySmall, isIndObject_yoneda	35
Total	50

CategoryTheory.Limits

Definitions

Name	Category	Theorems
IndObjectPresentation 📖	CompData	1 math math: IsIndObject.nonempty_presentation
IsIndObject 📖	CompData	14 math math: isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair, CategoryTheory.instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape, closedUnderLimitsOfShape_walkingParallelPair_isIndObject, CategoryTheory.Ind.isIndObject_inclusion_obj, CategoryTheory.instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject, isIndObject_iff, isIndObject_limit_comp_yoneda, IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType, isIndObject_of_isFiltered_of_finallySmall, isIndObject_yoneda, IsIndObject.iff_of_iso, isIndObject_iff_preservesFiniteLimits, IsIndObject.mk, CategoryTheory.instIsClosedUnderColimitsOfShapeFunctorOppositeTypeIsIndObjectOfIsFiltered

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIndObject_iff 📖	mathematical	—	IsIndObject CategoryTheory.IsFiltered CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow CategoryTheory.FinallySmall	—	IsIndObject.isFiltered IsIndObject.finallySmall isIndObject_of_isFiltered_of_finallySmall
isIndObject_iff_preservesFiniteLimits 📖	mathematical	—	IsIndObject PreservesFiniteLimits Opposite CategoryTheory.Category.opposite CategoryTheory.types	—	isIndObject_iff preservesFiniteLimits_of_isFiltered_costructuredArrow_yoneda isFiltered_costructuredArrow_yoneda_of_preservesFiniteLimits CategoryTheory.essentiallySmallSelf CategoryTheory.finallySmall_of_essentiallySmall
isIndObject_limit_comp_yoneda 📖	mathematical	—	IsIndObject limit CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda instHasLimitCompOfPreservesLimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.yonedaFunctor_preservesLimits	—	IsIndObject.map instHasLimitCompOfPreservesLimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.yonedaFunctor_preservesLimits CategoryTheory.Iso.isIso_hom isIndObject_yoneda
isIndObject_of_isFiltered_of_finallySmall 📖	mathematical	—	IsIndObject	—	CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.Functor.final_of_natIso CategoryTheory.final_fromFinalModel CategoryTheory.Functor.final_of_comp_full_faithful' CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFullInclusion CategoryTheory.IsFiltered.SmallFilteredIntermediate.instFaithfulInclusion Nonempty.map CategoryTheory.IsFiltered.nonempty CategoryTheory.IsFiltered.SmallFilteredIntermediate.instOfNonempty
isIndObject_yoneda 📖	mathematical	—	IsIndObject CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda	—	—

CategoryTheory.Limits.IndObjectPresentation

Definitions

Name	Category	Theorems
F 📖	CompOp	9 math math: extend_ι_app_app, extend_F, toCostructuredArrow_obj_left, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, extend_isColimit_desc_app, ofCocone_F, cocone_pt, yoneda_F
I 📖	CompOp	15 math math: hI, CategoryTheory.NonemptyParallelPairPresentationAux.hf, extend_ι_app_app, instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, instIsFilteredI, toCostructuredArrow_obj_right_as, toCostructuredArrow_obj_left, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, ofCocone_I, extend_isColimit_desc_app, cocone_pt, yoneda_I, CategoryTheory.NonemptyParallelPairPresentationAux.hg, extend_I
cocone 📖	CompOp	5 math math: extend_ι_app_app, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, extend_isColimit_desc_app, cocone_pt
coconeIsColimit 📖	CompOp	1 math math: extend_isColimit_desc_app
extend 📖	CompOp	5 math math: extend_ι_app_app, extend_F, extend_ℐ, extend_isColimit_desc_app, extend_I
instSmallCategoryI 📖	CompOp	8 math math: CategoryTheory.NonemptyParallelPairPresentationAux.hf, instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, instIsFilteredI, toCostructuredArrow_obj_right_as, toCostructuredArrow_obj_left, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, CategoryTheory.NonemptyParallelPairPresentationAux.hg
isColimit 📖	CompOp	3 math math: yoneda_isColimit_desc, ofCocone_isColimit, extend_isColimit_desc_app
ofCocone 📖	CompOp	5 math math: ofCocone_I, ofCocone_isColimit, ofCocone_ι, ofCocone_F, ofCocone_ℐ
toCostructuredArrow 📖	CompOp	7 math math: CategoryTheory.NonemptyParallelPairPresentationAux.hf, instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow, toCostructuredArrow_obj_right_as, toCostructuredArrow_obj_left, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, CategoryTheory.NonemptyParallelPairPresentationAux.hg
yoneda 📖	CompOp	5 math math: yoneda_isColimit_desc, yoneda_ι_app, yoneda_I, yoneda_F, yoneda_ℐ
ι 📖	CompOp	3 math math: extend_ι_app_app, yoneda_ι_app, ofCocone_ι
ℐ 📖	CompOp	10 math math: hI, extend_ι_app_app, extend_ℐ, toCostructuredArrow_obj_left, toCostructuredArrow_map_left, toCostructuredArrow_obj_hom, extend_isColimit_desc_app, ofCocone_ℐ, cocone_pt, yoneda_ℐ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt I ℐ CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp F CategoryTheory.yoneda cocone	—	—
extend_F 📖	mathematical	—	F extend	—	—
extend_I 📖	mathematical	—	I extend	—	—
extend_isColimit_desc_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Limits.Cocone.pt I ℐ CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.comp F CategoryTheory.yoneda CategoryTheory.Limits.Cocone.extend cocone CategoryTheory.Limits.IsColimit.desc isColimit extend coconeIsColimit CategoryTheory.inv CategoryTheory.Functor.obj CategoryTheory.NatIso.isIso_app_of_isIso	—	CategoryTheory.NatIso.isIso_app_of_isIso CategoryTheory.NatIso.isIso_inv_app
extend_ι_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.obj I ℐ CategoryTheory.Functor CategoryTheory.Functor.category Opposite.unop Opposite.op CategoryTheory.Functor.comp F CategoryTheory.yoneda CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.extend cocone ι extend CategoryTheory.Limits.Cocone.ι	—	—
extend_ℐ 📖	mathematical	—	ℐ extend	—	—
hI 📖	mathematical	—	CategoryTheory.IsFiltered I ℐ	—	—
instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow 📖	mathematical	—	CategoryTheory.Functor.Final I instSmallCategoryI CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow	—	CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre
instIsFilteredI 📖	mathematical	—	CategoryTheory.IsFiltered I instSmallCategoryI	—	hI
ofCocone_F 📖	mathematical	—	F CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda ofCocone	—	—
ofCocone_I 📖	mathematical	—	I CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda ofCocone	—	—
ofCocone_isColimit 📖	mathematical	—	isColimit CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda ofCocone	—	—
ofCocone_ι 📖	mathematical	—	ι CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda ofCocone CategoryTheory.Limits.Cocone.ι	—	—
ofCocone_ℐ 📖	mathematical	—	ℐ CategoryTheory.Limits.Cocone.pt CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.yoneda ofCocone	—	—
toCostructuredArrow_map_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow I ℐ CategoryTheory.Functor.comp F CategoryTheory.Limits.Cocone.pt cocone CategoryTheory.instCategoryCostructuredArrow CategoryTheory.CostructuredArrow.pre instSmallCategoryI CategoryTheory.Limits.Cocone.toCostructuredArrow CategoryTheory.Functor.map toCostructuredArrow	—	—
toCostructuredArrow_obj_hom 📖	mathematical	—	CategoryTheory.Comma.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj I instSmallCategoryI CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.NatTrans.app CategoryTheory.Functor.comp ℐ F CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι cocone	—	—
toCostructuredArrow_obj_left 📖	mathematical	—	CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj I instSmallCategoryI CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow ℐ F	—	—
toCostructuredArrow_obj_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.obj I instSmallCategoryI CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow	—	—
yoneda_F 📖	mathematical	—	F CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda yoneda CategoryTheory.Functor.fromPUnit	—	—
yoneda_I 📖	mathematical	—	I CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda yoneda CategoryTheory.Discrete	—	—
yoneda_isColimit_desc 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.yoneda CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct isColimit yoneda CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι	—	—
yoneda_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Functor.comp CategoryTheory.Functor.fromPUnit CategoryTheory.yoneda CategoryTheory.Functor.obj CategoryTheory.Functor.const ι yoneda CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
yoneda_ℐ 📖	mathematical	—	ℐ CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda yoneda CategoryTheory.discreteCategory	—	—

CategoryTheory.Limits.IsIndObject

Definitions

Name	Category	Theorems
presentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finallySmall 📖	mathematical	CategoryTheory.Limits.IsIndObject	CategoryTheory.FinallySmall CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.FinallySmall.mk' CategoryTheory.Limits.IndObjectPresentation.instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow
iff_of_iso 📖	mathematical	—	CategoryTheory.Limits.IsIndObject	—	map CategoryTheory.IsIso.inv_isIso
instIsClosedUnderIsomorphismsFunctorOppositeType 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.Limits.IsIndObject	—	map CategoryTheory.Iso.isIso_hom
isFiltered 📖	mathematical	CategoryTheory.Limits.IsIndObject	CategoryTheory.IsFiltered CategoryTheory.CostructuredArrow CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.IsFiltered.of_final CategoryTheory.Limits.IndObjectPresentation.instFinalICostructuredArrowFunctorOppositeTypeYonedaToCostructuredArrow CategoryTheory.Limits.IndObjectPresentation.instIsFilteredI
map 📖	—	CategoryTheory.Limits.IsIndObject	—	—	—
mk 📖	mathematical	—	CategoryTheory.Limits.IsIndObject	—	—
nonempty_presentation 📖	mathematical	CategoryTheory.Limits.IsIndObject	CategoryTheory.Limits.IndObjectPresentation	—	—

---

← Back to Index