Documentation

Mathlib.CategoryTheory.Abelian.Subcategory

Subcategories of abelian categories #

Let C be an abelian category. Given P : ObjectProperty C which contains zero, is closed under kernels, cokernels and finite products, we show that the full subcategory defined by P is abelian.

source
theorem CategoryTheory.ObjectProperty.preservesMonomorphisms_ι_of_isNormalEpiCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [Limits.HasFiniteCoproducts C] [Limits.HasKernels C] [Limits.HasCokernels C] [IsNormalEpiCategory C] [Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderKernels] :
P.ι.PreservesMonomorphisms
source
instance CategoryTheory.ObjectProperty.instIsNormalMonoCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] :
IsNormalMonoCategory P.FullSubcategory
source
theorem CategoryTheory.ObjectProperty.preservesEpimorphisms_ι_of_isNormalMonoCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] [Limits.HasFiniteProducts C] [Limits.HasKernels C] [Limits.HasCokernels C] [IsNormalMonoCategory C] [Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderCokernels] :
P.ι.PreservesEpimorphisms
source
instance CategoryTheory.ObjectProperty.instIsNormalEpiCategoryFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernels {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] :
IsNormalEpiCategory P.FullSubcategory
source
@[implicit_reducible]
instance CategoryTheory.ObjectProperty.instAbelianFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernelsOfIsClosedUnderFiniteProducts {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Abelian C] [P.ContainsZero] [P.IsClosedUnderKernels] [P.IsClosedUnderCokernels] [P.IsClosedUnderFiniteProducts] :
Abelian P.FullSubcategory
Equations
  • One or more equations did not get rendered due to their size.