Localization with respect to a Serre class

The main definition in this file is ObjectProperty.SerreClassLocalization.abelian which shows that if L : C ⥤ D is a localization functor with respect to the class of morphisms P.isoModSerre for a Serre class P : ObjectProperty C in the abelian category C, then D is an abelian category.

We also show that a functor G : D ⥤ E to an abelian category is exact iff the composition L ⋙ G is.

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

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_tfae {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) : [Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), CategoryStruct.comp (L.map z) (L.map f) = 0 → L.map z = 0].TFAE

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_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) : Mono (L.map f) ↔ P.monoModSerre f

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_tfae {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) : [Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), CategoryStruct.comp (L.map f) (L.map z) = 0 → L.map z = 0].TFAE

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_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) : Epi (L.map f) ↔ P.epiModSerre f

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_monomorphisms {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] : (MorphismProperty.monomorphisms D).inverseImage L = P.monoModSerre

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_epimorphisms {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] : (MorphismProperty.epimorphisms D).inverseImage L = P.epiModSerre

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesMonomorphisms {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] : L.PreservesMonomorphisms

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesEpimorphisms {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] : L.PreservesEpimorphisms

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.mono_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 : D} (f : X ⟶ Y) : Mono f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Mono f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.epi_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 : D} (f : X ⟶ Y) : Epi f ↔ ∃ (X' : C) (Y' : C) (f' : X' ⟶ Y') (_ : Epi f'), Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f)

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesKernel {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) : Limits.PreservesLimit (Limits.parallelPair f 0) L

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesCokernel {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) : Limits.PreservesColimit (Limits.parallelPair f 0) L

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasKernels {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.HasKernels D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasCokernels {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.HasCokernels D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasEqualizers {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.HasEqualizers D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasCoequalizers {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.HasCoequalizers D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasBinaryProducts {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.HasBinaryProducts D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.hasFiniteProducts {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.HasFiniteProducts D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalMonoCategory {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] : IsNormalMonoCategory D

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalEpiCategory {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] : IsNormalEpiCategory D

@[implicit_reducible]

def CategoryTheory.ObjectProperty.SerreClassLocalization.abelian {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] : Abelian D

If L : C ⥤ D is a localization functor with respect to a Serre class P in the abelian category C, then D is an abelian category. Note that we assume that D has already been equipped with a preadditive structure, and that L is additive. Otherwise, see the results in the file Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean which applies because P.isoModSerre has a calculus of left and right fractions.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits {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.PreservesFiniteLimits L

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits {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.PreservesFiniteColimits L

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.isIso_map_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) : IsIso (L.map f) ↔ P.isoModSerre f

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_isomorphisms {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] : (MorphismProperty.isomorphisms D).inverseImage L = P.isoModSerre

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits_comp_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] {E : Type u''} [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] (G : Functor D E) : Limits.PreservesFiniteLimits (L.comp G) ↔ Limits.PreservesFiniteLimits G

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteColimits_comp_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] {E : Type u''} [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] (G : Functor D E) : Limits.PreservesFiniteColimits (L.comp G) ↔ Limits.PreservesFiniteColimits G

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.exactFunctor_comp_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] {E : Type u''} [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] (G : Functor D E) : exactFunctor C E (L.comp G) ↔ exactFunctor D E G

def CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : Functor (D ⥤ₑ E) (C ⥤ₑ E)

When L : C ⥤ D is a localization functor with respect to a Serre class in the abelian category C, this is the functor (D ⥤ₑ E) ⥤ C ⥤ₑ E obtained by precomposition with L.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft_obj_obj {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] (G : D ⥤ₑ E) : ((whiskeringLeft L P E).obj G).obj = L.comp G.obj

noncomputable def CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeft {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : (whiskeringLeft L P E).FullyFaithful

When L : C ⥤ D is a localization functor with respect to a Serre class in the abelian category C, the functor whiskeringLeft L P E: (D ⥤ₑ E) ⥤ C ⥤ₑ E is fully faithful.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.ObjectProperty.SerreClassLocalization.instFaithfulExactFunctorWhiskeringLeft {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : (whiskeringLeft L P E).Faithful

instance CategoryTheory.ObjectProperty.SerreClassLocalization.instFullExactFunctorWhiskeringLeft {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : (whiskeringLeft L P E).Full

theorem CategoryTheory.ObjectProperty.SerreClassLocalization.essImage_whiskeringLeft {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] (E : Type u'') [Category.{v'', u''} E] [Abelian E] [L.IsLocalization P.isoModSerre] [Preadditive D] [L.Additive] : (whiskeringLeft L P E).essImage = fun (G : C ⥤ₑ E) => P.isoModSerre.IsInvertedBy G.obj

Let L : C ⥤ D be a localization functor with respect to a Serre class P in the abelian category C. If G : C ⥤ₑ E is an exact functor to an abelian category, it "factors" through D (i.e. it is in the essential image of whiskeringLeft L P E : (D ⥤ₑ E) ⥤ C ⥤ₑ E) iff G inverts the class of morphisms P.isoModSerre.