Indization

📁 Source: Mathlib/CategoryTheory/Abelian/GrothendieckAxioms/Indization.lean

Statistics

Metric	Count
Definitions	0
Theorems instAB5IndOfHasFiniteLimits, instHasExactColimitsOfShapeIndOfHasFiniteLimits, isGrothendieckAbelian_ind	3
Total	3

CategoryTheory.Limits

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAB5IndOfHasFiniteLimits 📖	mathematical	—	CategoryTheory.AB5 CategoryTheory.Ind CategoryTheory.instCategoryInd CategoryTheory.instHasFilteredColimitsInd	—	CategoryTheory.instHasFilteredColimitsInd hasColimitsOfShape_of_has_filtered_colimits instHasExactColimitsOfShapeIndOfHasFiniteLimits
instHasExactColimitsOfShapeIndOfHasFiniteLimits 📖	mathematical	—	CategoryTheory.HasExactColimitsOfShape CategoryTheory.Ind CategoryTheory.instCategoryInd hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.instHasFilteredColimitsInd	—	CategoryTheory.HasExactColimitsOfShape.domain_of_functor hasColimitsOfShape_of_has_filtered_colimits CategoryTheory.instHasFilteredColimitsInd functorCategoryHasColimitsOfShape Types.hasColimitsOfShape UnivLE.small UnivLE.self CategoryTheory.instHasExactColimitsOfShapeFunctorOfHasFiniteLimits CategoryTheory.AB5OfSize.ofShape hasFilteredColimitsOfSize_of_hasColimitsOfSize Types.hasColimitsOfSize instAB5Type hasFiniteLimits_of_hasCountableLimits hasCountableLimits_of_hasLimits Types.hasLimitsOfSize preservesFiniteLimits_of_createsFiniteLimits_and_hasFiniteLimits instHasFiniteLimitsFunctor reflectsFiniteLimits_of_reflectsIsomorphisms CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.instFullIndFunctorOppositeTypeInclusion CategoryTheory.instFaithfulIndFunctorOppositeTypeInclusion CategoryTheory.instHasFiniteLimitsInd CategoryTheory.preservesColimitOfShape_of_createsColimitsOfShape_and_hasColimitsOfShape
isGrothendieckAbelian_ind 📖	mathematical	—	CategoryTheory.IsGrothendieckAbelian CategoryTheory.Ind CategoryTheory.instCategoryInd CategoryTheory.instAbelianInd	—	CategoryTheory.locallySmall_of_univLE UnivLE.self CategoryTheory.instHasFilteredColimitsInd instAB5IndOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits hasColimitOfHasColimitsOfShape CategoryTheory.instHasCoproductsIndOfHasFiniteCoproducts hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Ind.isSeparator_range_yoneda

---

← Back to Index