feat(CategoryTheory): the localization w.r.t. a Serre class is an abelian category

Mathlib.lean

@@ -2280,6 +2280,7 @@ public import Mathlib.CategoryTheory.Abelian.Refinements
 public import Mathlib.CategoryTheory.Abelian.RightDerived
 public import Mathlib.CategoryTheory.Abelian.SerreClass.Basic
 public import Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
+public import Mathlib.CategoryTheory.Abelian.SerreClass.Localization
 public import Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
 public import Mathlib.CategoryTheory.Abelian.Subobject
 public import Mathlib.CategoryTheory.Abelian.Transfer

Mathlib/CategoryTheory/Abelian/Basic.lean

@@ -10,6 +10,7 @@ public import Mathlib.CategoryTheory.Preadditive.Biproducts
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
 public import Mathlib.CategoryTheory.Limits.Shapes.Images
 public import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
+public import Mathlib.CategoryTheory.MorphismProperty.Limits
 public import Mathlib.CategoryTheory.Abelian.NonPreadditive
 
 /-!
@@ -790,6 +791,12 @@ theorem mono_inl_of_factor_thru_epi_mono_factorization (f : X ⟶ Y) (g : X ⟶
 
 end MonoPushout
 
+instance : (MorphismProperty.monomorphisms C).IsStableUnderCobaseChange :=
+  .mk' (fun _ _ _ _ _ _ (_ : Mono _) ↦ inferInstanceAs (Mono _))
+
+instance : (MorphismProperty.epimorphisms C).IsStableUnderBaseChange :=
+  .mk' (fun _ _ _ _ _ _ (_ : Epi _) ↦ inferInstanceAs (Epi _))
+
 end CategoryTheory.Abelian
 
 namespace CategoryTheory.NonPreadditiveAbelian

Mathlib/CategoryTheory/Abelian/SerreClass/MorphismProperty.lean

@@ -5,10 +5,14 @@ Authors: Joël Riou
 -/
 module
 
+public import Mathlib.Algebra.Homology.Square
 public import Mathlib.CategoryTheory.Abelian.SerreClass.Basic
+public import Mathlib.CategoryTheory.Abelian.CommSq
 public import Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
+public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
 public import Mathlib.CategoryTheory.MorphismProperty.Composition
 public import Mathlib.CategoryTheory.MorphismProperty.Retract
+public import Mathlib.CategoryTheory.MorphismProperty.Limits
 public import Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
 
 /-!
@@ -85,6 +89,16 @@ lemma epiModSerre_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] :
     P.epiModSerre f :=
   P.epimorphisms_le_epiModSerre f (epimorphisms.infer_property f)
 
+@[simp]
+lemma epiModSerre_zero_iff (X Y : C) :
+    P.epiModSerre (0 : X ⟶ Y) ↔ P Y :=
+  P.prop_iff_of_iso cokernelZeroIsoTarget
+
+@[simp]
+lemma monoModSerre_zero_iff (X Y : C) :
+    P.monoModSerre (0 : X ⟶ Y) ↔ P X :=
+  P.prop_iff_of_iso kernelZeroIsoSource
+
 lemma isoModSerre_iff {X Y : C} (f : X ⟶ Y) :
     P.isoModSerre f ↔ P.monoModSerre f ∧ P.epiModSerre f := Iff.rfl
 
@@ -108,6 +122,11 @@ lemma isoModSerre_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (hf : P.monoModSerre f)
     P.isoModSerre f := by
   rwa [isoModSerre_iff_of_epi]
 
+@[simp]
+lemma isoModSerre_zero_iff (X Y : C) :
+    P.isoModSerre (0 : X ⟶ Y) ↔ P X ∧ P Y := by
+  simp [isoModSerre_iff]
+
 lemma isomorphisms_le_isoModSerre : isomorphisms C ≤ P.isoModSerre :=
   fun _ _ f (_ : IsIso f) ↦ ⟨P.monoModSerre_of_mono f, P.epiModSerre_of_epi f⟩
 
@@ -169,6 +188,34 @@ lemma isoModSerre_isInvertedBy_iff (F : C ⥤ D)
       (cokernelIsCokernel f)).map F).epi_f (((hF _ h₂).eq_of_tgt _ _))
   exact isIso_of_mono_of_epi (F.map f)
 
+instance : P.monoModSerre.IsStableUnderBaseChange where
+  of_isPullback sq h :=
+    have := isIso_kernel_map_of_isPullback sq.flip
+    P.prop_of_iso (asIso (kernel.map _ _ _ _ sq.w.symm)).symm h
+
+instance : P.epiModSerre.IsStableUnderBaseChange where
+  of_isPullback sq h :=
+    have := Abelian.mono_cokernel_map_of_isPullback sq.flip
+    P.prop_of_mono (cokernel.map _ _ _ _ sq.w.symm) h
+
+instance : P.isoModSerre.IsStableUnderBaseChange := by
+  dsimp [isoModSerre]
+  infer_instance
+
+instance : P.monoModSerre.IsStableUnderCobaseChange where
+  of_isPushout sq h :=
+    have := Abelian.epi_kernel_map_of_isPushout sq.flip
+    P.prop_of_epi (kernel.map _ _ _ _ sq.w.symm) h
+
+instance : P.epiModSerre.IsStableUnderCobaseChange where
+  of_isPushout sq h :=
+    have := isIso_cokernel_map_of_isPushout sq.flip
+    P.prop_of_iso (asIso (cokernel.map _ _ _ _ sq.w.symm)) h
+
+instance : P.isoModSerre.IsStableUnderCobaseChange := by
+  dsimp [isoModSerre]
+  infer_instance
+
 end ObjectProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Limits/ExactFunctor.lean

@@ -6,6 +6,7 @@ Authors: Markus Himmel
 module
 
 public import Mathlib.CategoryTheory.Limits.Preserves.Finite
+public import Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
 
 /-!
 # Bundled exact functors
@@ -41,6 +42,11 @@ variable {C D} in
 lemma leftExactFunctor_iff (F : C ⥤ D) :
     leftExactFunctor C D F ↔ PreservesFiniteLimits F := Iff.rfl
 
+instance : (leftExactFunctor C D).IsClosedUnderIsomorphisms where
+  of_iso e h := by
+    simp only [leftExactFunctor_iff] at h ⊢
+    exact preservesFiniteLimits_of_natIso e
+
 /-- Bundled left-exact functors. -/
 abbrev LeftExactFunctor := (leftExactFunctor C D).FullSubcategory
 
@@ -64,6 +70,11 @@ variable {C D} in
 lemma rightExactFunctor_iff (F : C ⥤ D) :
     rightExactFunctor C D F ↔ PreservesFiniteColimits F := Iff.rfl
 
+instance : (rightExactFunctor C D).IsClosedUnderIsomorphisms where
+  of_iso e h := by
+    simp only [rightExactFunctor_iff] at h ⊢
+    exact preservesFiniteColimits_of_natIso e
+
 /-- Bundled right-exact functors. -/
 abbrev RightExactFunctor := (rightExactFunctor C D).FullSubcategory
 
@@ -87,6 +98,10 @@ variable {C D} in
 lemma exactFunctor_iff (F : C ⥤ D) :
     exactFunctor C D F ↔ PreservesFiniteLimits F ∧ PreservesFiniteColimits F := Iff.rfl
 
+instance : (exactFunctor C D).IsClosedUnderIsomorphisms := by
+  dsimp [exactFunctor]
+  infer_instance
+
 /-- Bundled exact functors. -/
 abbrev ExactFunctor := (exactFunctor C D).FullSubcategory
 

Mathlib/CategoryTheory/Localization/Construction.lean

@@ -191,6 +191,9 @@ def objEquiv : C ≃ W.Localization where
     rintro ⟨⟨X⟩⟩
     rfl
 
+instance : W.Q.EssSurj where
+  mem_essImage Y := ⟨(objEquiv W).symm Y, ⟨Iso.refl _⟩⟩
+
 /-- A `MorphismProperty` in `W.Localization` is satisfied by all
 morphisms in the localized category if it contains the image of the
 morphisms in the original category, the inverses of the morphisms

Mathlib/CategoryTheory/Localization/Predicate.lean

@@ -267,6 +267,13 @@ lemma faithful_whiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*)
     ((whiskeringLeft C D E).obj L).Faithful :=
   inferInstanceAs (whiskeringLeftFunctor' L W E).Faithful
 
+/-- The precomposition with a localization functor gives fully faithful functors. -/
+def fullyFaithfulWhiskeringLeft (L : C ⥤ D) (W) [L.IsLocalization W] (E : Type*) [Category* E] :
+    ((whiskeringLeft C D E).obj L).FullyFaithful := by
+  have := full_whiskeringLeft L W E
+  have := faithful_whiskeringLeft L W E
+  exact FullyFaithful.ofFullyFaithful _
+
 variable {E}
 
 theorem natTrans_ext (L : C ⥤ D) (W) [L.IsLocalization W] {F₁ F₂ : D ⥤ E} {τ τ' : F₁ ⟶ F₂}