The class of isomorphisms modulo a Serre class

Let C be an abelian category and P : ObjectProperty C a Serre class. We define P.isoModSerre : MorphismProperty C, which is the class of morphisms f such that kernel f and cokernel f satisfy P. We show that P.isoModSerre is multiplicative, satisfies the two out of three property and is stable under retracts. (Similarly, we define P.monoModSerre and P.epiModSerre.)

TODO

• show that a localized category with respect to P.isoModSerre is abelian.

def CategoryTheory.ObjectProperty.monoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty C

The class of monomorphisms modulo a Serre class: given a Serre class P : ObjectProperty C, this is the class of morphisms f such that kernel f satisfies P.

def CategoryTheory.ObjectProperty.epiModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty C

The class of epimorphisms modulo a Serre class: given a Serre class P : ObjectProperty C, this is the class of morphisms f such that cokernel f satisfies P.

def CategoryTheory.ObjectProperty.isoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty C

The class of isomorphisms modulo a Serre class: given a Serre class P : ObjectProperty C, this is the class of morphisms f such that kernel f and cokernel f satisfy P.

theorem CategoryTheory.ObjectProperty.monoModSerre_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : P.monoModSerre f ↔ P (Limits.kernel f)

theorem CategoryTheory.ObjectProperty.monomorphisms_le_monoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty.monomorphisms C ≤ P.monoModSerre

theorem CategoryTheory.ObjectProperty.monoModSerre_of_mono {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Mono f] : P.monoModSerre f

theorem CategoryTheory.ObjectProperty.epiModSerre_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : P.epiModSerre f ↔ P (Limits.cokernel f)

theorem CategoryTheory.ObjectProperty.epimorphisms_le_epiModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty.epimorphisms C ≤ P.epiModSerre

theorem CategoryTheory.ObjectProperty.epiModSerre_of_epi {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Epi f] : P.epiModSerre f

theorem CategoryTheory.ObjectProperty.isoModSerre_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : P.isoModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f

theorem CategoryTheory.ObjectProperty.isoModSerre_iff_of_mono {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Mono f] : P.isoModSerre f ↔ P.epiModSerre f

theorem CategoryTheory.ObjectProperty.isoModSerre_iff_of_epi {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Epi f] : P.isoModSerre f ↔ P.monoModSerre f

theorem CategoryTheory.ObjectProperty.isoModSerre_of_mono {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Mono f] (hf : P.epiModSerre f) : P.isoModSerre f

theorem CategoryTheory.ObjectProperty.isoModSerre_of_epi {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [Epi f] (hf : P.monoModSerre f) : P.isoModSerre f

theorem CategoryTheory.ObjectProperty.isomorphisms_le_isoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : MorphismProperty.isomorphisms C ≤ P.isoModSerre

theorem CategoryTheory.ObjectProperty.isoModSerre_of_isIso {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) [IsIso f] : P.isoModSerre f

instance CategoryTheory.ObjectProperty.instIsMultiplicativeMonoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.monoModSerre.IsMultiplicative

instance CategoryTheory.ObjectProperty.instIsMultiplicativeEpiModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.epiModSerre.IsMultiplicative

instance CategoryTheory.ObjectProperty.instIsMultiplicativeIsoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsMultiplicative

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsMonoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.monoModSerre.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsEpiModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.epiModSerre.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instIsStableUnderRetractsIsoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.IsStableUnderRetracts

instance CategoryTheory.ObjectProperty.instHasTwoOutOfThreePropertyIsoModSerre {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] : P.isoModSerre.HasTwoOutOfThreeProperty

theorem CategoryTheory.ObjectProperty.le_kernel_of_isoModSerre_isInvertedBy {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (P : ObjectProperty C) [P.IsSerreClass] (F : Functor C D) [F.PreservesZeroMorphisms] (hF : P.isoModSerre.IsInvertedBy F) : P ≤ F.kernel

theorem CategoryTheory.ObjectProperty.isoModSerre_isInvertedBy_iff {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] [Abelian D] (P : ObjectProperty C) [P.IsSerreClass] (F : Functor C D) [Limits.PreservesFiniteLimits F] [Limits.PreservesFiniteColimits F] : P.isoModSerre.IsInvertedBy F ↔ P ≤ F.kernel