Indization

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

Statistics

Metric	Count
Definitions instAbelianInd	1
Theorems instIsIsoIndCoimageImageComparison	1
Total	2

CategoryTheory

Definitions

Name	Category	Theorems
instAbelianInd 📖	CompOp	1 math math: Limits.isGrothendieckAbelian_ind

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsIsoIndCoimageImageComparison 📖	mathematical	—	IsIso Ind instCategoryInd Abelian.coimage Preadditive.preadditiveHasZeroMorphisms instPreadditiveInd Abelian.toPreadditive Abelian.hasFiniteColimits Limits.HasKernels.has_limit Limits.hasKernels_of_hasEqualizers instHasLimitsOfShapeWalkingParallelPairInd Abelian.hasEqualizers Limits.HasCokernels.has_colimit Limits.hasCokernels_of_hasCoequalizers instHasColimitsOfShapeWalkingParallelPairInd Abelian.hasCoequalizers Limits.kernel Limits.kernel.ι Abelian.image Limits.cokernel Limits.cokernel.π Abelian.coimageImageComparison	—	Abelian.hasFiniteColimits Limits.HasKernels.has_limit Limits.hasKernels_of_hasEqualizers instHasLimitsOfShapeWalkingParallelPairInd Abelian.hasEqualizers Limits.HasCokernels.has_colimit Limits.hasCokernels_of_hasCoequalizers instHasColimitsOfShapeWalkingParallelPairInd Abelian.hasCoequalizers Ind.exists_nonempty_arrow_mk_iso_ind_lim Iso.isIso_hom Arrow.isIso_iff_isIso_of_isIso Limits.functorCategoryHasLimit Limits.hasLimitOfHasLimitsOfShape Limits.functorCategoryHasColimit Limits.hasColimitOfHasColimitsOfShape Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom Functor.preservesZeroMorphisms_of_preserves_terminal_object Limits.HasZeroObject.instFunctor Abelian.hasZeroObject Limits.hasZeroObject_of_hasFiniteBiproducts instHasFiniteBiproductsInd Limits.PreservesLimitsOfShape.preservesLimit instPreservesLimitsOfShapeFunctorIndLimOfFinCategoryOfHasLimitsOfShape Limits.hasLimitsOfShape_discrete Abelian.has_finite_products Finite.of_fintype Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeFunctorIndLimOfFinCategoryOfHasColimitsOfShape Iso.isIso_inv Functor.map_isIso Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison

---

← Back to Index