Subcategory

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

Statistics

Metric	Count
Definitions instAbelianFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernelsOfIsClosedUnderFiniteProducts	1
Theorems instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels, preservesEpimorphisms_ι_of_isNormalMonoCategory, preservesMonomorphisms_ι_of_isNormalEpiCategory	4
Total	5

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
instAbelianFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernelsOfIsClosedUnderFiniteProducts 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory FullSubcategory FullSubcategory.category instHasZeroMorphismsFullSubcategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesEpimorphisms_ι_of_isNormalMonoCategory CategoryTheory.Abelian.has_finite_products CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.toIsNormalMonoCategory CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.HasKernels.has_limit prop_kernel FullSubcategory.property hom_ext CategoryTheory.Limits.kernel.condition CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.fullSubcategoryInclusion_additive CategoryTheory.Functor.map_epi CategoryTheory.Limits.comp_zero CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFiniteColimits.reflects CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits CategoryTheory.Limits.fullyFaithful_reflectsColimits full_ι faithful_ι
instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory FullSubcategory FullSubcategory.category instHasZeroMorphismsFullSubcategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	preservesMonomorphisms_ι_of_isNormalEpiCategory CategoryTheory.Limits.hasFiniteCoproducts_of_hasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Abelian.has_kernels CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.toIsNormalEpiCategory CategoryTheory.Abelian.hasZeroObject CategoryTheory.Limits.HasCokernels.has_colimit prop_cokernel FullSubcategory.property hom_ext CategoryTheory.Limits.cokernel.condition CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.fullSubcategoryInclusion_additive CategoryTheory.Functor.map_mono CategoryTheory.Limits.zero_comp CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape CategoryTheory.Limits.ReflectsFiniteLimits.reflects CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits CategoryTheory.Limits.fullyFaithful_reflectsLimits full_ι faithful_ι
preservesEpimorphisms_ι_of_isNormalMonoCategory 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms FullSubcategory FullSubcategory.category ι	—	preservesCokernels_ι CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels instHasZeroObjectFullSubcategoryOfContainsZero CategoryTheory.Functor.preservesZeroMorphisms_of_full full_ι
preservesMonomorphisms_ι_of_isNormalEpiCategory 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms FullSubcategory FullSubcategory.category ι	—	preservesKernels_ι CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels instHasZeroObjectFullSubcategoryOfContainsZero CategoryTheory.Functor.preservesZeroMorphisms_of_full full_ι

---

← Back to Index