feat(CategoryTheory/Abelian): the inverse image of a Serre class by an exact functor (#22342)

We also define the (essential) image of a property of objects by a functor. `Functor.essImage` is also made an `ObjectProperty` instead of a `Set`.



Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Author: joelriou

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -100,7 +100,7 @@ def AffineScheme.ofHom {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
     AffineScheme.of X ⟶ AffineScheme.of Y :=
   f
 
-theorem mem_Spec_essImage (X : Scheme) : X ∈ Scheme.Spec.essImage ↔ IsAffine X :=
+theorem mem_Spec_essImage (X : Scheme) : Scheme.Spec.essImage X ↔ IsAffine X :=
   ⟨fun h => ⟨Functor.essImage.unit_isIso h⟩,
     fun _ => ΓSpec.adjunction.mem_essImage_of_unit_isIso _⟩
 

Mathlib/CategoryTheory/Abelian/SerreClass/Basic.lean

@@ -27,13 +27,14 @@ and is closed under subobjects, quotients and extensions.
 
 -/
 
-universe v u
+universe v v' u u'
 
 namespace CategoryTheory
 
 open Limits ZeroObject
 
 variable {C : Type u} [Category.{v} C] [Abelian C] (P : ObjectProperty C)
+  {D : Type u'} [Category.{v'} D] [Abelian D]
 
 namespace ObjectProperty
 
@@ -64,6 +65,10 @@ lemma prop_X₂_of_exact {S : ShortComplex C} (hS : S.Exact)
   exact (P.prop_X₂_of_shortExact (hS.shortExact d)
     (P.prop_of_epi d.left.f' h₁) (P.prop_of_mono d.right.g' h₃) :)
 
+instance (F : D ⥤ C) [PreservesFiniteLimits F]
+    [PreservesFiniteColimits F] :
+    (P.inverseImage F).IsSerreClass where
+
 end ObjectProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

@@ -189,7 +189,7 @@ instance [L.Faithful] [L.Full] {Y : D} : IsIso (R.map (h.counit.app Y)) :=
   isIso_of_hom_comp_eq_id _ (h.right_triangle_components Y)
 
 lemma isIso_counit_app_iff_mem_essImage [L.Faithful] [L.Full] {X : D} :
-    IsIso (h.counit.app X) ↔ X ∈ L.essImage := by
+    IsIso (h.counit.app X) ↔ L.essImage X := by
   constructor
   · intro
     exact ⟨R.obj X, ⟨asIso (h.counit.app X)⟩⟩
@@ -198,7 +198,7 @@ lemma isIso_counit_app_iff_mem_essImage [L.Faithful] [L.Full] {X : D} :
     infer_instance
 
 lemma mem_essImage_of_counit_isIso (A : D)
-    [IsIso (h.counit.app A)] : A ∈ L.essImage :=
+    [IsIso (h.counit.app A)] : L.essImage A :=
   ⟨R.obj A, ⟨asIso (h.counit.app A)⟩⟩
 
 lemma isIso_counit_app_of_iso [L.Faithful] [L.Full] {X : D} {Y : C} (e : X ≅ L.obj Y) :
@@ -212,7 +212,7 @@ instance [R.Faithful] [R.Full] {X : C} : IsIso (L.map (h.unit.app X)) :=
   isIso_of_comp_hom_eq_id _ (h.left_triangle_components X)
 
 lemma isIso_unit_app_iff_mem_essImage [R.Faithful] [R.Full] {Y : C} :
-    IsIso (h.unit.app Y) ↔ Y ∈ R.essImage := by
+    IsIso (h.unit.app Y) ↔ R.essImage Y := by
   constructor
   · intro
     exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩
@@ -222,7 +222,7 @@ lemma isIso_unit_app_iff_mem_essImage [R.Faithful] [R.Full] {Y : C} :
 
 /-- If `η_A` is an isomorphism, then `A` is in the essential image of `i`. -/
 theorem mem_essImage_of_unit_isIso (A : C)
-    [IsIso (h.unit.app A)] : A ∈ R.essImage :=
+    [IsIso (h.unit.app A)] : R.essImage A :=
   ⟨L.obj A, ⟨(asIso (h.unit.app A)).symm⟩⟩
 
 lemma isIso_unit_app_of_iso [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y ≅ R.obj X) :

Mathlib/CategoryTheory/Adjunction/Reflective.lean

@@ -80,13 +80,13 @@ reflection of `A`, with the isomorphism as `η_A`.
 
 (For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.)
 -/
-theorem Functor.essImage.unit_isIso [Reflective i] {A : C} (h : A ∈ i.essImage) :
+theorem Functor.essImage.unit_isIso [Reflective i] {A : C} (h : i.essImage A) :
     IsIso ((reflectorAdjunction i).unit.app A) := by
   rwa [isIso_unit_app_iff_mem_essImage]
 
 /-- If `η_A` is a split monomorphism, then `A` is in the reflective subcategory. -/
 theorem mem_essImage_of_unit_isSplitMono [Reflective i] {A : C}
-    [IsSplitMono ((reflectorAdjunction i).unit.app A)] : A ∈ i.essImage := by
+    [IsSplitMono ((reflectorAdjunction i).unit.app A)] : i.essImage A := by
   let η : 𝟭 C ⟶ reflector i ⋙ i := (reflectorAdjunction i).unit
   haveI : IsIso (η.app (i.obj ((reflector i).obj A))) :=
     Functor.essImage.unit_isIso ((i.obj_mem_essImage _))
@@ -126,7 +126,7 @@ This establishes there is a natural bijection `(A ⟶ B) ≃ (i.obj (L.obj A) 
 from the point of view of objects in `D`, `A` and `i.obj (L.obj A)` look the same: specifically
 that `η.app A` is an isomorphism.
 -/
-def unitCompPartialBijective [Reflective i] (A : C) {B : C} (hB : B ∈ i.essImage) :
+def unitCompPartialBijective [Reflective i] (A : C) {B : C} (hB : i.essImage B) :
     (A ⟶ B) ≃ (i.obj ((reflector i).obj A) ⟶ B) :=
   calc
     (A ⟶ B) ≃ (A ⟶ i.obj (Functor.essImage.witness hB)) := Iso.homCongr (Iso.refl _) hB.getIso.symm
@@ -135,17 +135,17 @@ def unitCompPartialBijective [Reflective i] (A : C) {B : C} (hB : B ∈ i.essIma
       Iso.homCongr (Iso.refl _) (Functor.essImage.getIso hB)
 
 @[simp]
-theorem unitCompPartialBijective_symm_apply [Reflective i] (A : C) {B : C} (hB : B ∈ i.essImage)
+theorem unitCompPartialBijective_symm_apply [Reflective i] (A : C) {B : C} (hB : i.essImage B)
     (f) : (unitCompPartialBijective A hB).symm f = (reflectorAdjunction i).unit.app A ≫ f := by
   simp [unitCompPartialBijective, unitCompPartialBijectiveAux_symm_apply]
 
 theorem unitCompPartialBijective_symm_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
-    (hB : B ∈ i.essImage) (hB' : B' ∈ i.essImage) (f : i.obj ((reflector i).obj A) ⟶ B) :
+    (hB : i.essImage B) (hB' : i.essImage B') (f : i.obj ((reflector i).obj A) ⟶ B) :
     (unitCompPartialBijective A hB').symm (f ≫ h) = (unitCompPartialBijective A hB).symm f ≫ h := by
   simp
 
 theorem unitCompPartialBijective_natural [Reflective i] (A : C) {B B' : C} (h : B ⟶ B')
-    (hB : B ∈ i.essImage) (hB' : B' ∈ i.essImage) (f : A ⟶ B) :
+    (hB : i.essImage B) (hB' : i.essImage B') (f : A ⟶ B) :
     (unitCompPartialBijective A hB') (f ≫ h) = unitCompPartialBijective A hB f ≫ h := by
   rw [← Equiv.eq_symm_apply, unitCompPartialBijective_symm_natural A h, Equiv.symm_apply_apply]
 
@@ -206,12 +206,12 @@ example [Coreflective j] {B : C} : IsIso ((coreflectorAdjunction j).counit.app (
 
 variable {j}
 
-lemma Functor.essImage.counit_isIso [Coreflective j] {A : D} (h : A ∈ j.essImage) :
+lemma Functor.essImage.counit_isIso [Coreflective j] {A : D} (h : j.essImage A) :
     IsIso ((coreflectorAdjunction j).counit.app A) := by
   rwa [isIso_counit_app_iff_mem_essImage]
 
 lemma mem_essImage_of_counit_isSplitEpi [Coreflective j] {A : D}
-    [IsSplitEpi ((coreflectorAdjunction j).counit.app A)] : A ∈ j.essImage := by
+    [IsSplitEpi ((coreflectorAdjunction j).counit.app A)] : j.essImage A := by
   let ε : coreflector j ⋙ j ⟶ 𝟭 D  := (coreflectorAdjunction j).counit
   haveI : IsIso (ε.app (j.obj ((coreflector j).obj A))) :=
     Functor.essImage.counit_isIso ((j.obj_mem_essImage _))

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -45,13 +45,13 @@ variable (i) [ChosenFiniteProducts C] [CartesianClosed C]
 `B ∈ D` implies `A ⟹ B ∈ D` for all `A`.
 -/
 class ExponentialIdeal : Prop where
-  exp_closed : ∀ {B}, B ∈ i.essImage → ∀ A, (A ⟹ B) ∈ i.essImage
+  exp_closed : ∀ {B}, i.essImage B → ∀ A, i.essImage (A ⟹ B)
 attribute [nolint docBlame] ExponentialIdeal.exp_closed
 
 /-- To show `i` is an exponential ideal it suffices to show that `A ⟹ iB` is "in" `D` for any `A` in
 `C` and `B` in `D`.
 -/
-theorem ExponentialIdeal.mk' (h : ∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ i.essImage) :
+theorem ExponentialIdeal.mk' (h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)) :
     ExponentialIdeal i :=
   ⟨fun hB A => by
     rcases hB with ⟨B', ⟨iB'⟩⟩

Mathlib/CategoryTheory/EssentialImage.lean

@@ -5,6 +5,7 @@ Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.NatIso
 import Mathlib.CategoryTheory.FullSubcategory
+import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 
 /-!
 # Essential image of a functor
@@ -37,34 +38,37 @@ isomorphic to an object in the image of the function `F.obj`. In other words, th
 under isomorphism of the function `F.obj`.
 This is the "non-evil" way of describing the image of a functor.
 -/
-def essImage (F : C ⥤ D) : Set D := fun Y => ∃ X : C, Nonempty (F.obj X ≅ Y)
+def essImage (F : C ⥤ D) : ObjectProperty D := fun Y => ∃ X : C, Nonempty (F.obj X ≅ Y)
 
 /-- Get the witnessing object that `Y` is in the subcategory given by `F`. -/
-def essImage.witness {Y : D} (h : Y ∈ F.essImage) : C :=
+def essImage.witness {Y : D} (h : F.essImage Y) : C :=
   h.choose
 
 /-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
 -- Porting note: in the next, the dot notation `h.witness` no longer works
-def essImage.getIso {Y : D} (h : Y ∈ F.essImage) : F.obj (essImage.witness h) ≅ Y :=
+def essImage.getIso {Y : D} (h : F.essImage Y) : F.obj (essImage.witness h) ≅ Y :=
   Classical.choice h.choose_spec
 
 /-- Being in the essential image is a "hygienic" property: it is preserved under isomorphism. -/
-theorem essImage.ofIso {Y Y' : D} (h : Y ≅ Y') (hY : Y ∈ essImage F) : Y' ∈ essImage F :=
+theorem essImage.ofIso {Y Y' : D} (h : Y ≅ Y') (hY : essImage F Y) : essImage F Y' :=
   hY.imp fun _ => Nonempty.map (· ≪≫ h)
 
+instance : F.essImage.IsClosedUnderIsomorphisms where
+  of_iso e h := essImage.ofIso e h
+
 /-- If `Y` is in the essential image of `F` then it is in the essential image of `F'` as long as
 `F ≅ F'`.
 -/
-theorem essImage.ofNatIso {F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : Y ∈ essImage F) :
-    Y ∈ essImage F' :=
+theorem essImage.ofNatIso {F' : C ⥤ D} (h : F ≅ F') {Y : D} (hY : essImage F Y) :
+    essImage F' Y :=
   hY.imp fun X => Nonempty.map fun t => h.symm.app X ≪≫ t
 
 /-- Isomorphic functors have equal essential images. -/
 theorem essImage_eq_of_natIso {F' : C ⥤ D} (h : F ≅ F') : essImage F = essImage F' :=
   funext fun _ => propext ⟨essImage.ofNatIso h, essImage.ofNatIso h.symm⟩
 
 /-- An object in the image is in the essential image. -/
-theorem obj_mem_essImage (F : D ⥤ C) (Y : D) : F.obj Y ∈ essImage F :=
+theorem obj_mem_essImage (F : D ⥤ C) (Y : D) : essImage F (F.obj Y) :=
   ⟨Y, ⟨Iso.refl _⟩⟩
 
 /-- The essential image of a functor, interpreted as a full subcategory of the target category. -/
@@ -113,7 +117,7 @@ image of `F`. In other words, for every `Y : D`, there is some `X : C` with `F.o
 @[stacks 001C]
 class EssSurj (F : C ⥤ D) : Prop where
   /-- All the objects of the target category are in the essential image. -/
-  mem_essImage (Y : D) : Y ∈ F.essImage
+  mem_essImage (Y : D) : F.essImage Y
 
 instance EssSurj.toEssImage : EssSurj F.toEssImage where
   mem_essImage := fun ⟨_, hY⟩ =>

Mathlib/CategoryTheory/ObjectProperty/Basic.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.Category.Basic
+import Mathlib.CategoryTheory.Functor.Basic
+import Mathlib.CategoryTheory.Iso
 
 /-!
 # Properties of objects in a category
@@ -20,12 +22,37 @@ regarding terms in `ObjectProperty C` when `C` is pretriangulated
 
 -/
 
-universe v u
+universe v v' u u'
 
 namespace CategoryTheory
 
 /-- A property of objects in a category `C` is a predicate `C → Prop`. -/
 @[nolint unusedArguments]
 abbrev ObjectProperty (C : Type u) [Category.{v} C] : Type u := C → Prop
 
+namespace ObjectProperty
+
+variable {C : Type u} {D : Type u'} [Category.{v} C] [Category.{v'} D]
+
+/-- The inverse image of a property of objects by a functor. -/
+def inverseImage (P : ObjectProperty D) (F : C ⥤ D) : ObjectProperty C :=
+  fun X ↦ P (F.obj X)
+
+@[simp]
+lemma prop_inverseImage_iff (P : ObjectProperty D) (F : C ⥤ D) (X : C) :
+    P.inverseImage F X ↔ P (F.obj X) := Iff.rfl
+
+/-- The essential image of a property of objects by a functor. -/
+def map (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D :=
+  fun Y ↦ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)
+
+lemma prop_map_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) :
+    P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y) := Iff.rfl
+
+lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) :
+    P.map F (F.obj X) :=
+  ⟨X, hX, ⟨Iso.refl _⟩⟩
+
+end ObjectProperty
+
 end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean

@@ -14,9 +14,12 @@ this file introduces the type class `P.IsClosedUnderIsomorphisms`.
 
 -/
 
+universe v v' u u'
+
 namespace CategoryTheory
 
-variable {C : Type*} [Category C] (P Q : ObjectProperty C)
+variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
+  (P Q : ObjectProperty C)
 
 namespace ObjectProperty
 
@@ -73,6 +76,15 @@ instance : IsClosedUnderIsomorphisms (isoClosure P) where
     rintro X Y e ⟨Z, hZ, ⟨f⟩⟩
     exact ⟨Z, hZ, ⟨e.symm.trans f⟩⟩
 
+instance (F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F) where
+  of_iso := by
+    rintro _ _ e ⟨X, hX, ⟨e'⟩⟩
+    exact ⟨X, hX, ⟨e' ≪≫ e⟩⟩
+
+instance (F : D ⥤ C) [P.IsClosedUnderIsomorphisms] :
+    IsClosedUnderIsomorphisms (P.inverseImage F) where
+  of_iso e hX := P.prop_of_iso (F.mapIso e) hX
+
 end ObjectProperty
 
 open ObjectProperty

Mathlib/CategoryTheory/ObjectProperty/ContainsZero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
-import Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
+import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
 
 /-!
 # Properties of objects which hold for a zero object
@@ -16,13 +16,13 @@ that `P` holds for all zero objects, as in some applications (e.g. triangulated
 
 -/
 
-universe v u
+universe v v' u u'
 
 namespace CategoryTheory
 
 open Limits ZeroObject
 
-variable {C : Type u} [Category.{v} C]
+variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
 
 namespace ObjectProperty
 
@@ -54,6 +54,19 @@ instance [HasZeroObject C] : (⊤ : ObjectProperty C).ContainsZero where
 instance [HasZeroObject C] : ContainsZero (IsZero (C := C)) where
   exists_zero := ⟨0, isZero_zero C, isZero_zero C⟩
 
+instance [P.ContainsZero] [HasZeroMorphisms C] [HasZeroMorphisms D]
+    (F : C ⥤ D) [F.PreservesZeroMorphisms] : (P.map F).ContainsZero where
+  exists_zero := by
+    obtain ⟨Z, h₁, h₂⟩ := P.exists_prop_of_containsZero
+    exact ⟨F.obj Z, F.map_isZero h₁, P.prop_map_obj F h₂⟩
+
+instance [P.ContainsZero] [P.IsClosedUnderIsomorphisms]
+    [HasZeroMorphisms C] [HasZeroMorphisms D]
+    (F : D ⥤ C) [F.PreservesZeroMorphisms] [HasZeroObject D] :
+    (P.inverseImage F).ContainsZero where
+  exists_zero :=
+    ⟨0, isZero_zero D, P.prop_of_isZero (F.map_isZero (isZero_zero D))⟩
+
 end ObjectProperty
 
 end CategoryTheory

Mathlib/CategoryTheory/ObjectProperty/EpiMono.lean

@@ -15,13 +15,13 @@ that `P` is closed under subobjects (resp. quotients).
 
 -/
 
-universe v u
+universe v v' u u'
 
 namespace CategoryTheory
 
 open Limits
 
-variable {C : Type u} [Category.{v} C]
+variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
 
 namespace ObjectProperty
 
@@ -47,6 +47,10 @@ lemma prop_X₁_of_shortExact [HasZeroMorphisms C] {S : ShortComplex C} (hS : S.
   have := hS.mono_f
   exact P.prop_of_mono S.f h₂
 
+instance (F : D ⥤ C) [F.PreservesMonomorphisms] :
+    (P.inverseImage F).IsClosedUnderSubobjects where
+  prop_of_mono f _ h := P.prop_of_mono (F.map f) h
+
 end
 
 section
@@ -69,6 +73,10 @@ lemma prop_X₃_of_shortExact [HasZeroMorphisms C] {S : ShortComplex C} (hS : S.
   have := hS.epi_g
   exact P.prop_of_epi S.g h₂
 
+instance (F : D ⥤ C) [F.PreservesEpimorphisms] :
+    (P.inverseImage F).IsClosedUnderQuotients where
+  prop_of_epi f _ h := P.prop_of_epi (F.map f) h
+
 end
 
 instance : (⊤ : ObjectProperty C).IsClosedUnderSubobjects where