Bousfield localizations with respect to Serre classes

If G : D ⥤ C is an exact functor between abelian categories, with a fully faithful right adjoint F, then G identifies C to the localization of D with respect to the class of morphisms G.kernel.isoModSerre, i.e. D is the localization of C with respect to the Serre class G.kernel consisting of the objects in D that are sent to a zero object by G. (We also translate this in terms of a left Bousfield localization.)

theorem CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphisms {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] (G : Functor D C) [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] : G.kernel.isoModSerre = (MorphismProperty.isomorphisms C).inverseImage G

theorem CategoryTheory.Abelian.isoModSerre_kernel_eq_isLocal_of_rightAdjoint {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] {G : Functor D C} [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] {F : Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.kernel.isoModSerre = ObjectProperty.isLocal fun (x : D) => x ∈ Set.range F.obj

theorem CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] [Abelian C] [Abelian D] {G : Functor D C} [Limits.PreservesFiniteLimits G] [Limits.PreservesFiniteColimits G] {F : Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful] : G.IsLocalization G.kernel.isoModSerre