From f39ad92c08639e4afd72b95e43b3441086358d6e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 25 Jan 2025 11:05:09 +0100
Subject: [PATCH 1/4] fixing the build

---
 Mathlib/CategoryTheory/Sites/Subsheaf.lean    |  53 +++--
 Mathlib/CategoryTheory/Subpresheaf/Basic.lean |   3 +-
 Mathlib/CategoryTheory/Subpresheaf/Image.lean | 205 +++++++++++++-----
 .../CategoryTheory/Subpresheaf/Sieves.lean    |   1 -
 4 files changed, 185 insertions(+), 77 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
index 3be19de81341b..2ade365d5e9d2 100644
--- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
@@ -194,16 +194,17 @@ variable (J)
 
 /-- A morphism factors through the sheafification of the image presheaf. -/
 @[simps!]
-def toImagePresheafSheafify (f : F' ⟶ F) : F' ⟶ ((imagePresheaf f).sheafify J).toPresheaf :=
-  toImagePresheaf f ≫ Subpresheaf.homOfLe ((imagePresheaf f).le_sheafify J)
+def Subpresheaf.toRangeSheafify (f : F' ⟶ F) : F' ⟶ ((Subpresheaf.range f).sheafify J).toPresheaf :=
+  toRange f ≫ Subpresheaf.homOfLe ((range f).le_sheafify J)
+
 
 variable {J}
 
 /-- The image sheaf of a morphism between sheaves, defined to be the sheafification of
 `image_presheaf`. -/
 @[simps]
-def imageSheaf {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf J (Type w) :=
-  ⟨((imagePresheaf f.1).sheafify J).toPresheaf, by
+def Sheaf.image {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf J (Type w) :=
+  ⟨((Subpresheaf.range f.1).sheafify J).toPresheaf, by
     rw [isSheaf_iff_isSheaf_of_type]
     apply Subpresheaf.sheafify_isSheaf
     rw [← isSheaf_iff_isSheaf_of_type]
@@ -211,34 +212,35 @@ def imageSheaf {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf J (Type w) :=
 
 /-- A morphism factors through the image sheaf. -/
 @[simps]
-def toImageSheaf {F F' : Sheaf J (Type w)} (f : F ⟶ F') : F ⟶ imageSheaf f :=
-  ⟨toImagePresheafSheafify J f.1⟩
+def Sheaf.toImage {F F' : Sheaf J (Type w)} (f : F ⟶ F') : F ⟶ Sheaf.image f :=
+  ⟨Subpresheaf.toRangeSheafify J f.1⟩
 
 /-- The inclusion of the image sheaf to the target. -/
 @[simps]
-def imageSheafι {F F' : Sheaf J (Type w)} (f : F ⟶ F') : imageSheaf f ⟶ F' :=
+def Sheaf.imageι {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Sheaf.image f ⟶ F' :=
   ⟨Subpresheaf.ι _⟩
 
+
 @[reassoc (attr := simp)]
-theorem toImageSheaf_ι {F F' : Sheaf J (Type w)} (f : F ⟶ F') :
-    toImageSheaf f ≫ imageSheafι f = f := by
+theorem Sheaf.toImage_ι {F F' : Sheaf J (Type w)} (f : F ⟶ F') :
+    toImage f ≫ imageι f = f := by
   ext1
-  simp [toImagePresheafSheafify]
+  simp [Subpresheaf.toRangeSheafify]
 
-instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (imageSheafι f) :=
+instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Mono (Sheaf.imageι f) :=
   (sheafToPresheaf J _).mono_of_mono_map
     (by
       dsimp
       infer_instance)
 
-instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (toImageSheaf f) := by
+instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (Sheaf.toImage f) := by
   refine ⟨@fun G' g₁ g₂ e => ?_⟩
   ext U ⟨s, hx⟩
   apply ((isSheaf_iff_isSheaf_of_type J _).mp G'.2 _ hx).isSeparatedFor.ext
   rintro V i ⟨y, e'⟩
   change (g₁.val.app _ ≫ G'.val.map _) _ = (g₂.val.app _ ≫ G'.val.map _) _
   rw [← NatTrans.naturality, ← NatTrans.naturality]
-  have E : (toImageSheaf f).val.app (op V) y = (imageSheaf f).val.map i.op ⟨s, hx⟩ :=
+  have E : (Sheaf.toImage f).val.app (op V) y = (Sheaf.image f).val.map i.op ⟨s, hx⟩ :=
     Subtype.ext e'
   have := congr_arg (fun f : F ⟶ G' => (Sheaf.Hom.val f).app _ y) e
   dsimp at this ⊢
@@ -246,9 +248,9 @@ instance {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Epi (toImageSheaf f) := by
 
 /-- The mono factorization given by `image_sheaf` for a morphism. -/
 def imageMonoFactorization {F F' : Sheaf J (Type w)} (f : F ⟶ F') : Limits.MonoFactorisation f where
-  I := imageSheaf f
-  m := imageSheafι f
-  e := toImageSheaf f
+  I := Sheaf.image f
+  m := Sheaf.imageι f
+  e := Sheaf.toImage f
 
 /-- The mono factorization given by `image_sheaf` for a morphism is an image. -/
 noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F ⟶ F') :
@@ -257,14 +259,13 @@ noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F 
   isImage :=
     { lift := fun I => by
         haveI M := (Sheaf.Hom.mono_iff_presheaf_mono J (Type (max v u)) _).mp I.m_mono
-        haveI := isIso_toImagePresheaf I.m.1
-        refine ⟨Subpresheaf.homOfLe ?_ ≫ inv (toImagePresheaf I.m.1)⟩
+        refine ⟨Subpresheaf.homOfLe ?_ ≫ inv (Subpresheaf.toRange I.m.1)⟩
         apply Subpresheaf.sheafify_le
         · conv_lhs => rw [← I.fac]
-          apply imagePresheaf_comp_le
+          apply Subpresheaf.range_comp_le
         · rw [← isSheaf_iff_isSheaf_of_type]
           exact F'.2
-        · apply Presieve.isSheaf_iso J (asIso <| toImagePresheaf I.m.1)
+        · apply Presieve.isSheaf_iso J (asIso <| Subpresheaf.toRange I.m.1)
           rw [← isSheaf_iff_isSheaf_of_type]
           exact I.I.2
       lift_fac := fun I => by
@@ -273,10 +274,18 @@ noncomputable def imageFactorization {F F' : Sheaf J (Type (max v u))} (f : F 
         generalize_proofs h
         rw [← Subpresheaf.homOfLe_ι h, Category.assoc]
         congr 1
-        rw [IsIso.inv_comp_eq, toImagePresheaf_ι] }
+        rw [IsIso.inv_comp_eq, Subpresheaf.toRange_ι] }
 
 instance : Limits.HasImages (Sheaf J (Type max v u)) :=
-  ⟨@fun _ _ f => ⟨⟨imageFactorization f⟩⟩⟩
+  ⟨fun f => ⟨⟨imageFactorization f⟩⟩⟩
+
+@[deprecated (since := "2025-01-25")] alias toImagePresheafSheafify :=
+  Subpresheaf.toRangeSheafify
+@[deprecated (since := "2025-01-25")] alias imageSheaf := Sheaf.image
+@[deprecated (since := "2025-01-25")] alias toImageSheaf := Sheaf.toImage
+@[deprecated (since := "2025-01-25")] alias imageSheafι := Sheaf.imageι
+@[deprecated (since := "2025-01-25")] alias toImageSheaf_ι := Sheaf.toImage_ι
+
 
 end Image
 
diff --git a/Mathlib/CategoryTheory/Subpresheaf/Basic.lean b/Mathlib/CategoryTheory/Subpresheaf/Basic.lean
index 080283e8b1880..2a751fadcfb62 100644
--- a/Mathlib/CategoryTheory/Subpresheaf/Basic.lean
+++ b/Mathlib/CategoryTheory/Subpresheaf/Basic.lean
@@ -6,7 +6,6 @@ Authors: Andrew Yang
 import Mathlib.CategoryTheory.Elementwise
 import Mathlib.Data.Set.Basic
 
-
 /-!
 
 # Subpresheaf of types
@@ -47,6 +46,8 @@ variable {F F' F'' : Cᵒᵖ ⥤ Type w} (G G' : Subpresheaf F)
 instance : PartialOrder (Subpresheaf F) :=
   PartialOrder.lift Subpresheaf.obj (fun _ _ => Subpresheaf.ext)
 
+lemma Subpresheaf.le_def (S T : Subpresheaf F) : S ≤ T ↔ ∀ U, S.obj U ≤ T.obj U := Iff.rfl
+
 instance : Top (Subpresheaf F) :=
   ⟨⟨fun _ => ⊤, @fun U _ _ x _ => by simp⟩⟩
 
diff --git a/Mathlib/CategoryTheory/Subpresheaf/Image.lean b/Mathlib/CategoryTheory/Subpresheaf/Image.lean
index 367029af657f0..bc05804591975 100644
--- a/Mathlib/CategoryTheory/Subpresheaf/Image.lean
+++ b/Mathlib/CategoryTheory/Subpresheaf/Image.lean
@@ -1,20 +1,18 @@
 /-
 Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Andrew Yang
+Authors: Andrew Yang, Joël Riou
 -/
-
 import Mathlib.CategoryTheory.Subpresheaf.Basic
 import Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
 
 /-!
 # The image of a subpresheaf
 
-Given a morphism of presheaves of types `f : F' ⟶ F`, we define `imagePresheaf f`
-as a subpresheaf of `F`.
-
-## TODO (@joelriou)
-* introduce `Subpresheaf.image` and `Subpresheaf.preimage`
+Given a morphism of presheaves of types `p : F' ⟶ F`, we define its range
+`Subpresheaf.range p`. More generally, if `G' : Subpresheaf F'`, we
+define `G'.image p : Subpresheaf F` as the image of `G'` by `f`, and
+if `G : Subpresheaf F`, we define its preimage `G.preimage f : Subpresheaf F'`.
 
 -/
 
@@ -22,63 +20,164 @@ universe w v u
 
 namespace CategoryTheory
 
-variable {C : Type u} [Category.{v} C] {F F' F'' : Cᵒᵖ ⥤ Type w} {G : Subpresheaf F}
+variable {C : Type u} [Category.{v} C] {F F' F'' : Cᵒᵖ ⥤ Type w}
 
-/-- If the image of a morphism falls in a subpresheaf, then the morphism factors through it. -/
-@[simps!]
-def Subpresheaf.lift (f : F' ⟶ F) (hf : ∀ U x, f.app U x ∈ G.obj U) : F' ⟶ G.toPresheaf where
-  app U x := ⟨f.app U x, hf U x⟩
-  naturality := by
-    have := elementwise_of% f.naturality
-    intros
-    refine funext fun x => Subtype.ext ?_
-    simp only [toPresheaf_obj, types_comp_apply]
-    exact this _ _
+namespace Subpresheaf
 
-@[reassoc (attr := simp)]
-theorem Subpresheaf.lift_ι (f : F' ⟶ F) (hf : ∀ U x, f.app U x ∈ G.obj U) :
-    G.lift f hf ≫ G.ι = f := by
-  ext
-  rfl
+section range
 
-/-- The image presheaf of a morphism, whose components are the set-theoretic images. -/
+/-- The range of a morphism of presheaves of types, as a subpresheaf of the target. -/
 @[simps]
-def imagePresheaf (f : F' ⟶ F) : Subpresheaf F where
-  obj U := Set.range (f.app U)
+def range (p : F' ⟶ F) : Subpresheaf F where
+  obj U := Set.range (p.app U)
   map := by
     rintro U V i _ ⟨x, rfl⟩
-    have := elementwise_of% f.naturality
-    exact ⟨_, this i x⟩
+    exact ⟨_, FunctorToTypes.naturality  _ _ p i x⟩
+
+variable (F) in
+lemma range_id : range (𝟙 F) = ⊤ := by aesop
 
 @[simp]
-theorem imagePresheaf_id : imagePresheaf (𝟙 F) = ⊤ := by
-  ext
-  simp
+lemma range_ι (G : Subpresheaf F) : range G.ι = G := by aesop
+
+end range
+
+section lift
 
-/-- A morphism factors through the image presheaf. -/
+variable (f : F' ⟶ F) {G : Subpresheaf F} (hf : range f ≤ G)
+
+/-- If the image of a morphism falls in a subpresheaf, then the morphism factors through it. -/
 @[simps!]
-def toImagePresheaf (f : F' ⟶ F) : F' ⟶ (imagePresheaf f).toPresheaf :=
-  (imagePresheaf f).lift f fun _ _ => Set.mem_range_self _
+def lift : F' ⟶ G.toPresheaf where
+  app U x := ⟨f.app U x, hf U (by simp)⟩
+  naturality _ _ g := by
+    ext x
+    simpa [Subtype.ext_iff] using FunctorToTypes.naturality _ _ f g x
+
+@[reassoc (attr := simp)]
+theorem lift_ι : lift f hf ≫ G.ι = f := rfl
+
+end lift
+
+section range
+
+variable (p : F' ⟶ F)
+
+/-- Given a morphism `p : F' ⟶ F` of presheaves of types, this is the morphism
+from `F'` to its range. -/
+def toRange :
+    F' ⟶ (range p).toPresheaf :=
+  lift p (by rfl)
 
 @[reassoc (attr := simp)]
-theorem toImagePresheaf_ι (f : F' ⟶ F) : toImagePresheaf f ≫ (imagePresheaf f).ι = f :=
-  (imagePresheaf f).lift_ι _ _
-
-theorem imagePresheaf_comp_le (f₁ : F ⟶ F') (f₂ : F' ⟶ F'') :
-    imagePresheaf (f₁ ≫ f₂) ≤ imagePresheaf f₂ := fun U _ hx => ⟨f₁.app U hx.choose, hx.choose_spec⟩
-
-instance isIso_toImagePresheaf {F F' : Cᵒᵖ ⥤ Type w} (f : F ⟶ F') [hf : Mono f] :
-  IsIso (toImagePresheaf f) := by
-  have : ∀ (X : Cᵒᵖ), IsIso ((toImagePresheaf f).app X) := by
-    intro X
-    rw [isIso_iff_bijective]
-    constructor
-    · intro x y e
-      have := (NatTrans.mono_iff_mono_app f).mp hf X
-      rw [mono_iff_injective] at this
-      exact this (congr_arg Subtype.val e :)
-    · rintro ⟨_, ⟨x, rfl⟩⟩
-      exact ⟨x, rfl⟩
-  apply NatIso.isIso_of_isIso_app
+lemma toRange_ι : toRange p ≫ (range p).ι = p := rfl
+
+lemma toRange_app_val {i : Cᵒᵖ} (x : F'.obj i) :
+    ((toRange p).app i x).val = p.app i x := by
+  simp [toRange]
+
+@[simp]
+lemma range_toRange : range (toRange p) = ⊤ := by
+  ext i ⟨x, hx⟩
+  dsimp at hx ⊢
+  simp only [Set.mem_range, Set.mem_univ, iff_true]
+  simp only [Set.mem_range] at hx
+  obtain ⟨y, rfl⟩ := hx
+  exact ⟨y, rfl⟩
+
+lemma epi_iff_range_eq_top :
+    Epi p ↔ range p = ⊤ := by
+  simp [NatTrans.epi_iff_epi_app, epi_iff_surjective, Subpresheaf.ext_iff, funext_iff,
+    Set.range_eq_univ]
+
+instance : Epi (toRange p) := by simp [epi_iff_range_eq_top]
+
+instance [Mono p] : IsIso (toRange p) := by
+  have := mono_of_mono_fac (toRange_ι p)
+  rw [NatTrans.isIso_iff_isIso_app]
+  intro i
+  rw [isIso_iff_bijective]
+  constructor
+  · rw [← mono_iff_injective]
+    infer_instance
+  · rw [← epi_iff_surjective]
+    infer_instance
+
+lemma range_comp_le (f : F ⟶ F') (g : F' ⟶ F'') :
+    range (f ≫ g) ≤ range g := fun _ _ _ ↦ by aesop
+
+end range
+
+section image
+
+variable (G : Subpresheaf F) (f : F ⟶ F')
+
+/-- The image of a subpresheaf by a morphism of presheaves of types. -/
+@[simps]
+def image : Subpresheaf F' where
+  obj i := (f.app i) '' (G.obj i)
+  map := by
+    rintro Δ Δ' φ _ ⟨x, hx, rfl⟩
+    exact ⟨F.map φ x, G.map φ hx, by apply FunctorToTypes.naturality⟩
+
+lemma image_top : (⊤ : Subpresheaf F).image f = range f := by aesop
+
+lemma image_comp (g : F' ⟶ F'') :
+    G.image (f ≫ g) = (G.image f).image g := by aesop
+
+lemma range_comp (g : F' ⟶ F'') :
+    range (f ≫ g) = (range f).image g := by aesop
+
+end image
+
+section preimage
+
+/-- The preimage of a subpresheaf by a morphism of presheaves of types. -/
+@[simps]
+def preimage (G : Subpresheaf F) (p : F' ⟶ F) : Subpresheaf F' where
+  obj n := p.app n ⁻¹' (G.obj n)
+  map f := (Set.preimage_mono (G.map f)).trans (by
+    simp only [Set.preimage_preimage, FunctorToTypes.naturality _ _ p f]
+    rfl)
+
+lemma image_le_iff (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') :
+    G.image f ≤ G' ↔ G ≤ G'.preimage f := by
+  simp [Subpresheaf.le_def]
+
+/-- Given a morphism `p : F' ⟶ F` of presheaves of types and `G : Subpresheaf F`,
+this is the morphism from the preimage of `G` by `p` to `G`. -/
+def fromPreimage (G : Subpresheaf F) (p : F' ⟶ F) :
+    (G.preimage p).toPresheaf ⟶ G.toPresheaf :=
+  lift ((G.preimage p).ι ≫ p) (by
+    rw [range_comp, range_ι, image_le_iff])
+
+@[reassoc]
+lemma fromPreimage_ι (G : Subpresheaf F) (p : F' ⟶ F) :
+    G.fromPreimage p ≫ G.ι = (G.preimage p).ι ≫ p := rfl
+
+lemma preimage_eq_top_iff (G : Subpresheaf F) (p : F' ⟶ F) :
+    G.preimage p = ⊤ ↔ range p ≤ G := by
+  rw [← image_top, image_le_iff]
+  aesop
+
+@[simp]
+lemma preimage_image_of_epi (G : Subpresheaf F) (p : F' ⟶ F) [hp : Epi p] :
+    (G.preimage p).image p = G := by
+  apply le_antisymm
+  · rw [image_le_iff]
+  · intro i x hx
+    simp only [NatTrans.epi_iff_epi_app, epi_iff_surjective] at hp
+    obtain ⟨y, rfl⟩ := hp _ x
+    exact ⟨y, hx, rfl⟩
+
+end preimage
+
+end Subpresheaf
+
+@[deprecated (since := "2025-01-25")] alias imagePresheaf := Subpresheaf.range
+@[deprecated (since := "2025-01-25")] alias imagePresheaf_id := Subpresheaf.range_id
+@[deprecated (since := "2025-01-25")] alias toImagePresheaf := Subpresheaf.toRange
+@[deprecated (since := "2025-01-25")] alias toImagePresheaf_ι := Subpresheaf.toRange_ι
+@[deprecated (since := "2025-01-25")] alias imagePresheaf_comp_le := Subpresheaf.range_comp_le
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Subpresheaf/Sieves.lean b/Mathlib/CategoryTheory/Subpresheaf/Sieves.lean
index 12ffd8506ee78..7c84f551edcd1 100644
--- a/Mathlib/CategoryTheory/Subpresheaf/Sieves.lean
+++ b/Mathlib/CategoryTheory/Subpresheaf/Sieves.lean
@@ -3,7 +3,6 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-
 import Mathlib.CategoryTheory.Subpresheaf.Basic
 import Mathlib.CategoryTheory.Sites.IsSheafFor
 

From 1ab7d0069a03a9d9ba3fdbb5f307c7453c61683b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 25 Jan 2025 11:06:38 +0100
Subject: [PATCH 2/4] removed blank line

---
 Mathlib/CategoryTheory/Sites/Subsheaf.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
index 2ade365d5e9d2..03d5262b3fe05 100644
--- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
@@ -286,7 +286,6 @@ instance : Limits.HasImages (Sheaf J (Type max v u)) :=
 @[deprecated (since := "2025-01-25")] alias imageSheafι := Sheaf.imageι
 @[deprecated (since := "2025-01-25")] alias toImageSheaf_ι := Sheaf.toImage_ι
 
-
 end Image
 
 end CategoryTheory

From e96834b88149f1c670b7f478179e081721e29786 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 25 Jan 2025 11:11:44 +0100
Subject: [PATCH 3/4] fixing the build

---
 .../Sites/LocallyInjective.lean               |  4 +--
 .../Sites/LocallySurjective.lean              | 28 +++++++++----------
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/LocallyInjective.lean b/Mathlib/CategoryTheory/Sites/LocallyInjective.lean
index 64b1d4140a669..9f60ac73c6f1a 100644
--- a/Mathlib/CategoryTheory/Sites/LocallyInjective.lean
+++ b/Mathlib/CategoryTheory/Sites/LocallyInjective.lean
@@ -243,8 +243,8 @@ lemma mono_of_isLocallyInjective [IsLocallyInjective φ] : Mono φ := by
   infer_instance
 
 instance {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallyInjective (imageSheafι f) := by
-  dsimp [imageSheafι]
+    IsLocallyInjective (Sheaf.imageι f) := by
+  dsimp [Sheaf.imageι]
   infer_instance
 
 end Sheaf
diff --git a/Mathlib/CategoryTheory/Sites/LocallySurjective.lean b/Mathlib/CategoryTheory/Sites/LocallySurjective.lean
index e3c5a1393050f..a4fe2b6272f33 100644
--- a/Mathlib/CategoryTheory/Sites/LocallySurjective.lean
+++ b/Mathlib/CategoryTheory/Sites/LocallySurjective.lean
@@ -50,7 +50,7 @@ def imageSieve {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
     rw [op_comp, G.map_comp, comp_apply, ← ht, elementwise_of% f.naturality]
 
 theorem imageSieve_eq_sieveOfSection {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
-    imageSieve f s = (imagePresheaf (whiskerRight f (forget A))).sieveOfSection s :=
+    imageSieve f s = (Subpresheaf.range (whiskerRight f (forget A))).sieveOfSection s :=
   rfl
 
 theorem imageSieve_whisker_forget {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : C} (s : G.obj (op U)) :
@@ -92,13 +92,13 @@ instance {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) [IsLocallySurjective J f] :
   imageSieve_mem s := imageSieve_mem J f s
 
 theorem isLocallySurjective_iff_imagePresheaf_sheafify_eq_top {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
-    IsLocallySurjective J f ↔ (imagePresheaf (whiskerRight f (forget A))).sheafify J = ⊤ := by
+    IsLocallySurjective J f ↔ (Subpresheaf.range (whiskerRight f (forget A))).sheafify J = ⊤ := by
   simp only [Subpresheaf.ext_iff, funext_iff, Set.ext_iff, top_subpresheaf_obj,
     Set.top_eq_univ, Set.mem_univ, iff_true]
   exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩
 
 theorem isLocallySurjective_iff_imagePresheaf_sheafify_eq_top' {F G : Cᵒᵖ ⥤ Type w} (f : F ⟶ G) :
-    IsLocallySurjective J f ↔ (imagePresheaf f).sheafify J = ⊤ := by
+    IsLocallySurjective J f ↔ (Subpresheaf.range f).sheafify J = ⊤ := by
   apply isLocallySurjective_iff_imagePresheaf_sheafify_eq_top
 
 theorem isLocallySurjective_iff_whisker_forget {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
@@ -248,7 +248,7 @@ lemma isLocallySurjective_comp_iff
     infer_instance
 
 instance {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) :
-    IsLocallySurjective J (toImagePresheafSheafify J f) where
+    IsLocallySurjective J (Subpresheaf.toRangeSheafify J f) where
   imageSieve_mem {X} := by
     rintro ⟨s, hs⟩
     refine J.superset_covering ?_ hs
@@ -257,20 +257,20 @@ instance {F₁ F₂ : Cᵒᵖ ⥤ Type w} (f : F₁ ⟶ F₂) :
 
 /-- The image of `F` in `J.sheafify F` is isomorphic to the sheafification. -/
 noncomputable def sheafificationIsoImagePresheaf (F : Cᵒᵖ ⥤ Type max u v) :
-    J.sheafify F ≅ ((imagePresheaf (J.toSheafify F)).sheafify J).toPresheaf where
+    J.sheafify F ≅ ((Subpresheaf.range (J.toSheafify F)).sheafify J).toPresheaf where
   hom :=
-    J.sheafifyLift (toImagePresheafSheafify J _)
+    J.sheafifyLift (Subpresheaf.toRangeSheafify J _)
       ((isSheaf_iff_isSheaf_of_type J _).mpr <|
         Subpresheaf.sheafify_isSheaf _ <|
           (isSheaf_iff_isSheaf_of_type J _).mp <| GrothendieckTopology.sheafify_isSheaf J _)
   inv := Subpresheaf.ι _
   hom_inv_id :=
-    J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
+    J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
   inv_hom_id := by
     rw [← cancel_mono (Subpresheaf.ι _), Category.id_comp, Category.assoc]
     refine Eq.trans ?_ (Category.comp_id _)
     congr 1
-    exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [toImagePresheafSheafify])
+    exact J.sheafify_hom_ext _ _ (J.sheafify_isSheaf _) (by simp [Subpresheaf.toRangeSheafify])
 
 section
 
@@ -328,8 +328,8 @@ instance isLocallySurjective_of_iso [IsIso φ] : IsLocallySurjective φ := by
   infer_instance
 
 instance {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallySurjective (toImageSheaf f) := by
-  dsimp [toImageSheaf]
+    IsLocallySurjective (Sheaf.toImage f) := by
+  dsimp [Sheaf.toImage]
   infer_instance
 
 variable [J.HasSheafCompose (forget A)]
@@ -339,11 +339,11 @@ instance [IsLocallySurjective φ] :
   (Presheaf.isLocallySurjective_iff_whisker_forget J φ.val).1 inferInstance
 
 theorem isLocallySurjective_iff_isIso {F G : Sheaf J (Type w)} (f : F ⟶ G) :
-    IsLocallySurjective f ↔ IsIso (imageSheafι f) := by
+    IsLocallySurjective f ↔ IsIso (Sheaf.imageι f) := by
   dsimp only [IsLocallySurjective]
-  rw [imageSheafι, Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top',
+  rw [Sheaf.imageι, Presheaf.isLocallySurjective_iff_imagePresheaf_sheafify_eq_top',
     Subpresheaf.eq_top_iff_isIso]
-  exact isIso_iff_of_reflects_iso (f := imageSheafι f) (F := sheafToPresheaf J (Type w))
+  exact isIso_iff_of_reflects_iso (f := Sheaf.imageι f) (F := sheafToPresheaf J (Type w))
 
 instance epi_of_isLocallySurjective' {F₁ F₂ : Sheaf J (Type w)} (φ : F₁ ⟶ F₂)
     [IsLocallySurjective φ] : Epi φ where
@@ -369,7 +369,7 @@ lemma isLocallySurjective_iff_epi {F G : Sheaf J (Type w)} (φ : F ⟶ G)
   · intro
     infer_instance
   · intro
-    have := epi_of_epi_fac (toImageSheaf_ι φ)
+    have := epi_of_epi_fac (Sheaf.toImage_ι φ)
     rw [isLocallySurjective_iff_isIso φ]
     apply isIso_of_mono_of_epi
 

From 530dd846e697868d79aa1beb15aca6c42cc3aa89 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Sat, 25 Jan 2025 21:26:53 +0100
Subject: [PATCH 4/4] added preimage_comp and preimage_id

---
 Mathlib/CategoryTheory/Subpresheaf/Image.lean | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/Mathlib/CategoryTheory/Subpresheaf/Image.lean b/Mathlib/CategoryTheory/Subpresheaf/Image.lean
index bc05804591975..4247b888fb3af 100644
--- a/Mathlib/CategoryTheory/Subpresheaf/Image.lean
+++ b/Mathlib/CategoryTheory/Subpresheaf/Image.lean
@@ -140,6 +140,13 @@ def preimage (G : Subpresheaf F) (p : F' ⟶ F) : Subpresheaf F' where
     simp only [Set.preimage_preimage, FunctorToTypes.naturality _ _ p f]
     rfl)
 
+@[simp]
+lemma preimage_id (G : Subpresheaf F) :
+    G.preimage (𝟙 F) = G := by aesop
+
+lemma preimage_comp (G : Subpresheaf F) (f : F'' ⟶ F') (g : F' ⟶ F) :
+    G.preimage (f ≫ g) = (G.preimage g).preimage f := by aesop
+
 lemma image_le_iff (G : Subpresheaf F) (f : F ⟶ F') (G' : Subpresheaf F') :
     G.image f ≤ G' ↔ G ≤ G'.preimage f := by
   simp [Subpresheaf.le_def]