Ind

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Ind.lean

Statistics

Metric	Count
Definitions Ind, ind	2
Theorems ind_iff_exists, ind_ind, instIsClosedUnderIsomorphismsInd, le_ind, of_essentiallySmall_index	5
Total	7

CategoryTheory

Definitions

Name	Category	Theorems
Ind 📖	CompOp	27 math math: instHasFilteredColimitsInd, instHasColimitsOfShapeWalkingParallelPairInd, instFullIndYoneda, instPreservesLimitsIndYoneda, Limits.instAB5IndOfHasFiniteLimits, Ind.isIndObject_inclusion_obj, Ind.exists_nonempty_arrow_mk_iso_ind_lim, instHasLimitsInd, Limits.instHasExactColimitsOfShapeIndOfHasFiniteLimits, Ind.isSeparator_range_yoneda, instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape, instFaithfulIndYoneda, instIsIsoIndCoimageImageComparison, Limits.isGrothendieckAbelian_ind, instHasFiniteBiproductsInd, instHasLimitsOfShapeWalkingParallelPairInd, instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape, instHasLimitsOfShapeDiscreteInd, Ind.isSeparating_range_yoneda, instHasColimitsIndOfHasFiniteColimits, instHasColimitsOfShapeDiscreteIndOfFinite, instFaithfulIndFunctorOppositeTypeInclusion, instRepresentablyCoflatIndYoneda, instHasFiniteLimitsInd, instFullIndFunctorOppositeTypeInclusion, instHasCoproductsIndOfHasFiniteCoproducts, instPreservesFiniteColimitsIndYoneda

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
ind 📖	CompOp	7 math math: of_essentiallySmall_index, CategoryTheory.MorphismProperty.ind_iff_ind_underMk, instIsClosedUnderIsomorphismsInd, CategoryTheory.MorphismProperty.underObj_ind_eq_ind_underObj, le_ind, ind_iff_exists, ind_ind

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ind_iff_exists 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le isFinitelyPresentable	ind CategoryTheory.CategoryStruct.comp	—	CategoryTheory.IsFinitelyPresentable.exists_hom_of_isColimit CategoryTheory.instIsFinitelyPresentableObjFullSubcategoryIsFinitelyPresentableι CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithful CategoryTheory.IsFiltered.toIsFilteredOrEmpty CategoryTheory.IsFinitelyAccessibleCategory.instIsFilteredCostructuredArrowFullSubcategoryIsFinitelyPresentableι CategoryTheory.CostructuredArrow.instFullCompPre full_ιOfLE CategoryTheory.CostructuredArrow.instFaithfulCompPre faithful_ιOfLE CategoryTheory.IsFiltered.of_exists_of_isFiltered_of_fullyFaithful CategoryTheory.Functor.IsDenseAt.of_final CategoryTheory.Functor.IsDense.isDenseAt CategoryTheory.IsFinitelyAccessibleCategory.instIsDenseFullSubcategoryIsFinitelyPresentableι CategoryTheory.essentiallySmall_of_fully_faithful CategoryTheory.CostructuredArrow.essentiallySmall instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 CategoryTheory.HasCardinalFilteredGenerator.toLocallySmall Cardinal.fact_isRegular_aleph0 CategoryTheory.IsCardinalAccessibleCategory.toHasCardinalFilteredGenerator CategoryTheory.IsFinitelyAccessibleCategory.instEssentiallySmallIsFinitelyPresentable of_essentiallySmall_index FullSubcategory.property
ind_ind 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le isFinitelyPresentable	ind	—	le_antisymm CategoryTheory.Limits.ColimitPresentation.instLocallySmallTotal CategoryTheory.locallySmall_of_univLE UnivLE.self CategoryTheory.IsFiltered.of_equivalence CategoryTheory.Limits.ColimitPresentation.instIsFilteredTotalOfIsFinitelyPresentableObjDiag CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse le_ind
instIsClosedUnderIsomorphismsInd 📖	mathematical	—	IsClosedUnderIsomorphisms ind	—	—
le_ind 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le ind	—	CategoryTheory.isFiltered_of_directed_le_nonempty OrderTop.instIsDirectedOrder
of_essentiallySmall_index 📖	mathematical	CategoryTheory.Functor.obj CategoryTheory.Limits.ColimitPresentation.diag	ind	—	CategoryTheory.IsFiltered.of_equivalence CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse

---

← Back to Index