Category

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

Statistics

Metric	Count
Definitions colimitPresentationCompYoneda, equivalence, inclusion, fullyFaithful, leftExactFunctorEquivalence, lim, limCompInclusion, presentation, yoneda, fullyFaithful, yonedaCompInclusion, parallelPairIsoParallelPairCompIndYoneda, instCategoryInd, instCreatesColimitsOfShapeIndFunctorOppositeTypeInclusionOfIsFiltered, instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits, instCreatesLimitsOfShapeIndFunctorOppositeTypeDiscreteInclusionOfHasLimitsOfShape, instCreatesLimitsOfShapeIndFunctorOppositeTypeWalkingParallelPairInclusionOfHasLimitsOfShape, instCreatesLimitsOfSizeIndFunctorOppositeTypeInclusionOfHasLimits	18
Theorems exists_nonempty_arrow_mk_iso_ind_lim, isIndObject_inclusion_obj, instFaithfulIndFunctorOppositeTypeInclusion, instFaithfulIndYoneda, instFullIndFunctorOppositeTypeInclusion, instFullIndYoneda, instHasColimitsIndOfHasFiniteColimits, instHasColimitsOfShapeDiscreteIndOfFinite, instHasColimitsOfShapeWalkingParallelPairInd, instHasCoproductsIndOfHasFiniteCoproducts, instHasFilteredColimitsInd, instHasFiniteLimitsInd, instHasLimitsInd, instHasLimitsOfShapeDiscreteInd, instHasLimitsOfShapeWalkingParallelPairInd, instIsClosedUnderColimitsOfShapeFunctorOppositeTypeIsIndObjectOfIsFiltered, instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape, instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape, instPreservesFiniteColimitsIndYoneda, instPreservesLimitsIndYoneda, instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape, instRepresentablyCoflatIndYoneda	22
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
instCategoryInd 📖	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
instCreatesColimitsOfShapeIndFunctorOppositeTypeInclusionOfIsFiltered 📖	CompOp	—
instCreatesFiniteLimitsIndFunctorOppositeTypeInclusionOfHasFiniteLimits 📖	CompOp	—
instCreatesLimitsOfShapeIndFunctorOppositeTypeDiscreteInclusionOfHasLimitsOfShape 📖	CompOp	—
instCreatesLimitsOfShapeIndFunctorOppositeTypeWalkingParallelPairInclusionOfHasLimitsOfShape 📖	CompOp	—
instCreatesLimitsOfSizeIndFunctorOppositeTypeInclusionOfHasLimits 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulIndFunctorOppositeTypeInclusion 📖	mathematical	—	Functor.Faithful Ind instCategoryInd Functor Opposite Category.opposite types Functor.category Ind.inclusion	—	Functor.Faithful.comp Equivalence.faithful_functor ObjectProperty.faithful_ι
instFaithfulIndYoneda 📖	mathematical	—	Functor.Faithful Ind instCategoryInd Ind.yoneda	—	Limits.isIndObject_yoneda Functor.Faithful.comp ObjectProperty.instFaithfulFullSubcategoryLift Yoneda.yoneda_faithful Equivalence.faithful_inverse
instFullIndFunctorOppositeTypeInclusion 📖	mathematical	—	Functor.Full Ind instCategoryInd Functor Opposite Category.opposite types Functor.category Ind.inclusion	—	Functor.Full.comp Equivalence.full_functor ObjectProperty.full_ι
instFullIndYoneda 📖	mathematical	—	Functor.Full Ind instCategoryInd Ind.yoneda	—	Limits.isIndObject_yoneda Functor.Full.comp ObjectProperty.instFullFullSubcategoryLift Yoneda.yoneda_full Equivalence.full_inverse
instHasColimitsIndOfHasFiniteColimits 📖	mathematical	—	Limits.HasColimits Ind instCategoryInd	—	Limits.has_colimits_of_hasCoequalizers_and_coproducts instHasCoproductsIndOfHasFiniteCoproducts Limits.hasFiniteCoproducts_of_hasFiniteColimits instHasColimitsOfShapeWalkingParallelPairInd Limits.hasColimitsOfShape_of_hasFiniteColimits
instHasColimitsOfShapeDiscreteIndOfFinite 📖	mathematical	—	Limits.HasColimitsOfShape Discrete discreteCategory Ind instCategoryInd	—	Limits.hasColimitsOfShape_of_has_filtered_colimits instHasFilteredColimitsInd instIsFilteredForall Limits.IndObjectPresentation.instIsFilteredI Limits.hasColimitOfHasColimitsOfShape final_eval Limits.hasColimit_of_iso Limits.instHasColimitCompOfPreservesColimit Limits.functorCategoryHasColimit Limits.comp_preservesColimit Limits.PreservesColimitsOfShape.preservesColimit whiskeringRight_preservesColimitsOfShape Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts Limits.instPreservesFiniteCoproductsOfPreservesFiniteColimits instPreservesFiniteColimitsIndYoneda Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Limits.instIsLeftAdjointFunctorColim
instHasColimitsOfShapeWalkingParallelPairInd 📖	mathematical	—	Limits.HasColimitsOfShape Limits.WalkingParallelPair Limits.walkingParallelPairHomCategory Ind instCategoryInd	—	nonempty_indParallelPairPresentation ObjectProperty.FullSubcategory.property Limits.hasColimit_of_iso instIsFilteredI Limits.instHasColimitCompOfPreservesColimit Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape
instHasCoproductsIndOfHasFiniteCoproducts 📖	mathematical	—	Limits.HasCoproducts Ind instCategoryInd	—	Limits.hasColimitsOfShape_of_equivalence instHasColimitsOfShapeDiscreteIndOfFinite instFiniteULift Finite.of_fintype Limits.hasColimitsOfShape_discrete Limits.hasCoproducts_of_finite_and_filtered instHasFilteredColimitsInd
instHasFilteredColimitsInd 📖	mathematical	—	Limits.HasFilteredColimits Ind instCategoryInd	—	hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape Limits.functorCategoryHasColimitsOfShape Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self
instHasFiniteLimitsInd 📖	mathematical	—	Limits.HasFiniteLimits Ind instCategoryInd	—	Limits.hasFiniteLimits_of_hasLimitsLimits_of_createsFiniteLimits Limits.hasFiniteLimits_of_hasLimitsOfSize₀ Limits.functorCategoryHasLimitsOfSize Limits.Types.hasLimitsOfSize univLE_of_max UnivLE.self
instHasLimitsInd 📖	mathematical	—	Limits.HasLimits Ind instCategoryInd	—	hasLimits_of_hasLimits_createsLimits Limits.functorCategoryHasLimitsOfSize Limits.Types.hasLimitsOfSize UnivLE.self
instHasLimitsOfShapeDiscreteInd 📖	mathematical	—	Limits.HasLimitsOfShape Discrete discreteCategory Ind instCategoryInd	—	hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape Limits.functorCategoryHasLimitsOfShape Limits.Types.instHasProductsType
instHasLimitsOfShapeWalkingParallelPairInd 📖	mathematical	—	Limits.HasLimitsOfShape Limits.WalkingParallelPair Limits.walkingParallelPairHomCategory Ind instCategoryInd	—	hasLimitsOfShape_of_hasLimitsOfShape_createsLimitsOfShape Limits.functorCategoryHasLimitsOfShape Limits.Types.hasLimitsOfShape UnivLE.small univLE_of_max UnivLE.self
instIsClosedUnderColimitsOfShapeFunctorOppositeTypeIsIndObjectOfIsFiltered 📖	mathematical	—	ObjectProperty.IsClosedUnderColimitsOfShape Functor Opposite Category.opposite types Functor.category Limits.IsIndObject	—	ObjectProperty.IsClosedUnderColimitsOfShape.mk' Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType Limits.isIndObject_colimit
instIsClosedUnderLimitsOfShapeFunctorOppositeTypeIsIndObjectDiscreteOfHasLimitsOfShape 📖	mathematical	—	ObjectProperty.IsClosedUnderLimitsOfShape Functor Opposite Category.opposite types Functor.category Limits.IsIndObject Discrete discreteCategory	—	ObjectProperty.IsClosedUnderLimitsOfShape.mk' Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType Limits.isIndObject_limit_of_discrete_of_hasLimitsOfShape
instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape 📖	mathematical	—	Limits.PreservesColimitsOfShape Functor Functor.category Ind instCategoryInd Ind.lim	—	Limits.comp_preservesColimitsOfShape whiskeringRight_preservesColimitsOfShape Limits.preservesColimitsOfShapeOfPreservesFiniteColimits instPreservesFiniteColimitsIndYoneda Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Limits.instIsLeftAdjointFunctorColim
instPreservesFiniteColimitsIndYoneda 📖	mathematical	—	Limits.PreservesFiniteColimits Ind instCategoryInd Ind.yoneda	—	preservesFiniteColimits_of_coflat instRepresentablyCoflatIndYoneda
instPreservesLimitsIndYoneda 📖	mathematical	—	Limits.PreservesLimits Ind instCategoryInd Ind.yoneda	—	Limits.preservesLimits_of_reflects_of_preserves Limits.preservesLimits_of_natIso yonedaFunctor_preservesLimits Limits.fullyFaithful_reflectsLimits instFullIndFunctorOppositeTypeInclusion instFaithfulIndFunctorOppositeTypeInclusion
instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape 📖	mathematical	—	Limits.PreservesLimitsOfShape Functor Functor.category Ind instCategoryInd Ind.lim	—	Limits.preservesLimitsOfShape_of_reflects_of_preserves Limits.preservesLimitsOfShape_of_natIso Limits.functorCategoryHasColimitsOfShape Limits.Types.hasColimitsOfShape UnivLE.small UnivLE.self Limits.comp_preservesLimitsOfShape whiskeringRight_preservesLimitsOfShape Limits.preservesLimitsOfShapeOfPreservesFiniteLimits Limits.PreservesLimits.preservesFiniteLimits yonedaFunctor_preservesLimits instPreservesLimitsOfShapeFunctorColim Limits.Types.hasLimitsOfShape Countable.toSmall Finite.to_countable Finite.of_fintype Limits.filtered_colim_preservesFiniteLimits Limits.reflectsLimitsOfShape_of_reflectsLimits Types.instReflectsLimitsOfSizeForgetTypeHom Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint Functor.isLeftAdjoint_of_isEquivalence Types.instIsEquivalenceForgetTypeHom Functor.corepresentable_preservesLimitsOfShape Types.instIsCorepresentableForgetTypeHom Limits.fullyFaithful_reflectsLimits instFullIndFunctorOppositeTypeInclusion instFaithfulIndFunctorOppositeTypeInclusion
instRepresentablyCoflatIndYoneda 📖	mathematical	—	RepresentablyCoflat Ind instCategoryInd Ind.yoneda	—	Limits.isIndObject_iff Ind.isIndObject_inclusion_obj IsFiltered.of_equivalence CostructuredArrow.isEquivalence_post instFullIndFunctorOppositeTypeInclusion instFaithfulIndFunctorOppositeTypeInclusion

CategoryTheory.Ind

Definitions

Name	Category	Theorems
colimitPresentationCompYoneda 📖	CompOp	—
equivalence 📖	CompOp	—
inclusion 📖	CompOp	3 math math: isIndObject_inclusion_obj, CategoryTheory.instFaithfulIndFunctorOppositeTypeInclusion, CategoryTheory.instFullIndFunctorOppositeTypeInclusion
leftExactFunctorEquivalence 📖	CompOp	—
lim 📖	CompOp	3 math math: exists_nonempty_arrow_mk_iso_ind_lim, CategoryTheory.instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape, CategoryTheory.instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape
limCompInclusion 📖	CompOp	—
presentation 📖	CompOp	—
yoneda 📖	CompOp	7 math math: CategoryTheory.instFullIndYoneda, CategoryTheory.instPreservesLimitsIndYoneda, isSeparator_range_yoneda, CategoryTheory.instFaithfulIndYoneda, isSeparating_range_yoneda, CategoryTheory.instRepresentablyCoflatIndYoneda, CategoryTheory.instPreservesFiniteColimitsIndYoneda
yonedaCompInclusion 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nonempty_arrow_mk_iso_ind_lim 📖	mathematical	—	CategoryTheory.Iso CategoryTheory.Arrow CategoryTheory.Ind CategoryTheory.instCategoryInd CategoryTheory.instCategoryArrow CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category lim CategoryTheory.Functor.map	—	CategoryTheory.nonempty_indParallelPairPresentation CategoryTheory.ObjectProperty.FullSubcategory.property CategoryTheory.instIsFilteredI CategoryTheory.NatTrans.naturality
isIndObject_inclusion_obj 📖	mathematical	—	CategoryTheory.Limits.IsIndObject CategoryTheory.Functor.obj CategoryTheory.Ind CategoryTheory.instCategoryInd CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.category inclusion	—	CategoryTheory.ObjectProperty.FullSubcategory.property

CategoryTheory.Ind.inclusion

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

CategoryTheory.Ind.yoneda

Definitions

Name	Category	Theorems
fullyFaithful 📖	CompOp	—

CategoryTheory.IndParallelPairPresentation

Definitions

Name	Category	Theorems
parallelPairIsoParallelPairCompIndYoneda 📖	CompOp	—

---

← Back to Index