Localization with respect to a Serre class

In this file, we shall study the localization of an abelian category C with respect to the class of morphisms P.isoModSerre where P : ObjectProperty C is a Serre class. We shall show that the localized category is an abelian category (TODO @joelriou).

theorem CategoryTheory.ObjectProperty.exists_epiModSerre_comp_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ (X' : C) (s : X' ⟶ X) (_ : P.epiModSerre s), CategoryStruct.comp s f = 0) ↔ P (Abelian.image f)

theorem CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ (X' : C) (s : X' ⟶ X) (_ : P.isoModSerre s), CategoryStruct.comp s f = 0) ↔ P (Abelian.image f)

theorem CategoryTheory.ObjectProperty.exists_comp_monoModSerre_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.monoModSerre s), CategoryStruct.comp f s = 0) ↔ P (Abelian.image f)

theorem CategoryTheory.ObjectProperty.exists_comp_isoModSerre_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] (P : ObjectProperty C) [P.IsSerreClass] {X Y : C} (f : X ⟶ Y) : (∃ (Y' : C) (s : Y ⟶ Y') (_ : P.isoModSerre s), CategoryStruct.comp f s = 0) ↔ P (Abelian.image f)

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

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

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

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

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.isZero_obj_iff {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] (L : Functor C D) (P : ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] (X : C) : Limits.IsZero (L.obj X) ↔ P X

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasZeroObject {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] (L : Functor C D) (P : ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : Limits.HasZeroObject D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] (L : Functor C D) (P : ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : L.map f = 0 ↔ P (Abelian.image f)

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.map_comp_eq_zero_iff_of_epi_mono {C : Type u} [Category.{v, u} C] [Abelian C] {D : Type u'} [Category.{v', u'} D] (L : Functor C D) (P : ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y) [Epi f] [Mono g] : CategoryStruct.comp (L.map f) (L.map g) = 0 ↔ P Z