diff --git a/Mathlib/AlgebraicGeometry/Sites/Small.lean b/Mathlib/AlgebraicGeometry/Sites/Small.lean
index 65525c1c014f1d..eb2ee33aaa6afc 100644
--- a/Mathlib/AlgebraicGeometry/Sites/Small.lean
+++ b/Mathlib/AlgebraicGeometry/Sites/Small.lean
@@ -72,7 +72,7 @@ lemma Cover.toPresieveOver_le_arrows_iff {X : Over S} (R : Sieve X)
     (𝒰 : Cover.{u} (precoverage P) X.left) [𝒰.Over S] :
     𝒰.toPresieveOver ≤ R.arrows ↔
       Presieve.ofArrows 𝒰.X 𝒰.f ≤ (Sieve.overEquiv X R).arrows := by
-  simp_rw [← Sieve.giGenerate.gc.le_iff_le, ← Sieve.overEquiv_le_overEquiv_iff]
+  simp_rw [← Sieve.giGenerate.gc.le_iff_le, ← (Sieve.overEquiv X).map_rel_iff]
   rw [overEquiv_generate_toPresieveOver_eq_ofArrows]
 
 variable [P.IsMultiplicative] [P.RespectsIso]
diff --git a/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean b/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean
index 0330de4a5c5ae8..25a9d3550f1cc0 100644
--- a/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean
+++ b/Mathlib/CategoryTheory/Sites/Descent/DescentData.lean
@@ -616,7 +616,7 @@ noncomputable def fullyFaithfulToDescentData [F.IsPrestack J] (hf : Sieve.ofArro
     intro M N
     refine ((isSheaf_iff_isSheaf_of_type _ _).1
       (IsPrestack.isSheaf J M N)).isSheafFor _ ?_
-    rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, Equiv.apply_symm_apply])
+    rwa [GrothendieckTopology.mem_over_iff, Sieve.generate_sieve, OrderIso.apply_symm_apply])
 
 lemma isPrestackFor [F.IsPrestack J] {S : C} (R : Presieve S) (hR : Sieve.generate R ∈ J S) :
     F.IsPrestackFor R := by
diff --git a/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean b/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean
index fd2a5da5fe7d2a..cfb85be4edb1c8 100644
--- a/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean
+++ b/Mathlib/CategoryTheory/Sites/Descent/Precoverage.lean
@@ -64,7 +64,7 @@ public lemma faithful_pullFunctor :
     refine F.presheafHomObjHomEquiv.injective ?_i
     have : (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm
       (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈ J.over (X i) _ := by
-      simpa only [J.mem_over_iff, Equiv.apply_symm_apply] using! J.pullback_stable (f i) hf'
+      simpa only [J.mem_over_iff, OrderIso.apply_symm_apply] using! J.pullback_stable (f i) hf'
     refine (((isSheaf_iff_isSheaf_of_type _ _).1
       (IsPrestack.isSheaf _ _ _)).isSeparated _ this).ext ?_
     rintro Z g ⟨Y, p, c, ⟨j⟩, hp⟩
@@ -104,7 +104,7 @@ abbrev sieve (i : ι) : Sieve (Over.mk (𝟙 (X i))) :=
 include hf' in
 variable (f) in
 lemma sieve_mem (i : ι) : sieve f f' i ∈ J.over _ _ := by
-  simpa only [J.mem_over_iff, Equiv.apply_symm_apply] using! J.pullback_stable (f i) hf'
+  simpa only [J.mem_over_iff, OrderIso.apply_symm_apply] using! J.pullback_stable (f i) hf'
 
 set_option backward.defeqAttrib.useBackward true in
 lemma mem_sieve {i : ι} {Z : C} (q : Z ⟶ X i) ⦃j : ι'⦄ (a : Z ⟶ X' j)
@@ -275,7 +275,7 @@ lemma comm ⦃W : C⦄ (q : W ⟶ S) ⦃i₁ i₂ : ι⦄
     Category.assoc, DescentData.hom_comp, D₂.hom_self _ _ hf₁, Category.comp_id]
   have H : (Sieve.overEquiv (Over.mk f₁)).symm
       (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ J.over _ _ := by
-    rw [J.mem_over_iff, Equiv.apply_symm_apply]
+    rw [J.mem_over_iff, OrderIso.apply_symm_apply]
     exact J.pullback_stable _ hf'
   refine ((isSheaf_iff_isSheaf_of_type _ _).1
     (IsPrestack.isSheaf J (D₁.obj i₁) (D₂.obj i₁)) _ H).isSeparatedFor.ext ?_
diff --git a/Mathlib/CategoryTheory/Sites/Over.lean b/Mathlib/CategoryTheory/Sites/Over.lean
index b008c77f36e1fb..3a512a92661ab2 100644
--- a/Mathlib/CategoryTheory/Sites/Over.lean
+++ b/Mathlib/CategoryTheory/Sites/Over.lean
@@ -33,70 +33,74 @@ open Category
 
 variable {C : Type u} [Category.{v} C]
 
+namespace Presieve
+
 @[simp]
-lemma Presieve.map_functorPullback_overForget {X : C} {Y : Over X} (R : Presieve Y.left) :
-    Presieve.map (Over.forget X) (.functorPullback (Over.forget X) R) = R := by
-  refine le_antisymm (map_functorPullback _) fun Z g hg ↦ ?_
-  let g' : Over.mk (g ≫ Y.hom) ⟶ Y := Over.homMk g
-  exact Presieve.map.of (u := g') hg
+lemma functorPullback_map_overForget {X : C} {Y : Over X} (S : Presieve Y) :
+    (S.map (Over.forget X)).functorPullback (Over.forget X) = S := by
+  let R : Presieve Y.left := fun Z g ↦ S (Over.homMk g : Over.mk (g ≫ Y.hom) ⟶ Y)
+  suffices hR : (R.functorPullback (Over.forget X)) = S by
+    rw [← hR, functorPullback_map_functorPullback]
+  funext Z f
+  obtain ⟨Z, fZ, rfl⟩ := Z.mk_surjective
+  obtain ⟨g : Z ⟶ Y.left, rfl : g ≫ Y.hom = fZ, rfl⟩ := Over.homMk_surjective f
+  rfl
 
-namespace Sieve
+@[simp]
+lemma map_functorPullback_overForget {X : C} {Y : Over X} (R : Presieve Y.left) :
+    (R.functorPullback (Over.forget X)).map (Over.forget X) = R :=
+  le_antisymm (map_functorPullback _) fun Z g hg ↦
+    map.of (u := (Over.homMk g : Over.mk (g ≫ Y.hom) ⟶ Y)) hg
 
-set_option backward.defeqAttrib.useBackward true in
-/-- The equivalence `Sieve Y ≃ Sieve Y.left` for all `Y : Over X`. -/
-def overEquiv {X : C} (Y : Over X) :
-    Sieve Y ≃ Sieve Y.left where
-  toFun S := Sieve.functorPushforward (Over.forget X) S
-  invFun S' := Sieve.functorPullback (Over.forget X) S'
-  left_inv S := by
-    ext Z g
-    dsimp [Presieve.functorPullback, Presieve.functorPushforward]
-    constructor
-    · rintro ⟨W, a, b, h, w⟩
-      let c : Z ⟶ W := Over.homMk b
-        (by rw [← Over.w g, w, assoc, Over.w a])
-      rw [show g = c ≫ a by ext; exact w]
-      exact S.downward_closed h _
-    · intro h
-      exact ⟨Z, g, 𝟙 _, h, by simp⟩
-  right_inv S := by
-    ext Z g
-    dsimp [Presieve.functorPullback, Presieve.functorPushforward]
-    constructor
-    · rintro ⟨W, a, b, h, rfl⟩
-      exact S.downward_closed h _
-    · intro h
-      exact ⟨Over.mk ((g ≫ Y.hom)), Over.homMk g, 𝟙 _, h, by simp⟩
+/-- The equivalence `Presieve Y ≃ Presieve Y.left` for all `Y : Over X`. -/
+@[simps]
+def overEquiv {X : C} (Y : Over X) : Presieve Y ≃o Presieve Y.left where
+  toFun S := map (Over.forget X) S
+  invFun S' := functorPullback (Over.forget X) S'
+  left_inv := functorPullback_map_overForget
+  right_inv := map_functorPullback_overForget
+  map_rel_iff' := ⟨fun h ↦ by simpa using functorPullback_monotone h, fun h ↦ map_monotone h⟩
 
-@[simp]
-lemma overEquiv_top {X : C} (Y : Over X) :
-    overEquiv Y ⊤ = ⊤ := by
-  ext Z g
-  simp only [top_apply, iff_true]
-  dsimp [overEquiv, Presieve.functorPushforward]
-  exact ⟨Y, 𝟙 Y, g, by simp, by simp⟩
+end Presieve
+
+namespace Sieve
 
 @[simp]
-lemma overEquiv_symm_top {X : C} (Y : Over X) :
-    (overEquiv Y).symm ⊤ = ⊤ :=
-  (overEquiv Y).injective (by simp)
+lemma functorPushforward_overForget_arrows {X : C} {Y : Over X} (S : Sieve Y) :
+    S.arrows.functorPushforward (Over.forget X) = S.arrows.map (Over.forget X) := by
+  refine le_antisymm ?_ (S.arrows.map_le_functorPushforward (Over.forget X))
+  rintro Z - ⟨W, fW, fZ, h, rfl⟩
+  exact Presieve.map_map (S.downward_closed h (Over.homMk fZ : Over.mk (fZ ≫ W.hom) ⟶ W))
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma overEquiv_bot {X : C} (Y : Over X) : overEquiv Y ⊥ = ⊥ := by
-  simp [overEquiv]
+lemma functorPullback_functorPushforward_overForget {X : C} {Y : Over X} (S : Sieve Y) :
+    (S.functorPushforward (Over.forget X)).functorPullback (Over.forget X) = S := by
+  apply arrows_ext
+  simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
-lemma overEquiv_symm_bot {X : C} (Y : Over X) : (overEquiv Y).symm ⊥ = ⊥ := by
-  rw [overEquiv, Equiv.coe_fn_symm_mk, functorPullback_bot]
+lemma functorPushforward_functorPullback_overForget {X : C} {Y : Over X} (S : Sieve Y.left) :
+    (S.functorPullback (Over.forget X)).functorPushforward (Over.forget X) = S := by
+  apply arrows_ext
+  simp [← arrows_generate_map_eq_functorPushforward]
 
-lemma overEquiv_le_overEquiv_iff {X : C} {Y : Over X} (R₁ R₂ : Sieve Y) :
-    R₁.overEquiv Y ≤ R₂.overEquiv Y ↔ R₁ ≤ R₂ := by
-  refine ⟨fun h ↦ ?_, fun h ↦ Sieve.functorPushforward_monotone _ _ h⟩
-  replace h : (overEquiv Y).symm (R₁.overEquiv Y) ≤ (overEquiv Y).symm (R₂.overEquiv Y) :=
-    Sieve.functorPullback_monotone _ _ h
-  simpa using h
+/-- The equivalence `Sieve Y ≃ Sieve Y.left` for all `Y : Over X`. -/
+@[simps -isSimp] -- working with `overEquiv` is useful enough that we don't want `simp` unfolding it
+def overEquiv {X : C} (Y : Over X) : Sieve Y ≃o Sieve Y.left where
+  toFun := functorPushforward (Over.forget X)
+  invFun := functorPullback (Over.forget X)
+  left_inv := functorPullback_functorPushforward_overForget
+  right_inv := functorPushforward_functorPullback_overForget
+  map_rel_iff' := by
+    rw [Equiv.coe_fn_mk]
+    exact ⟨fun h ↦ by simpa using functorPullback_monotone _ _ h,
+      fun h ↦ functorPushforward_monotone _ _ h⟩
+
+@[deprecated (since := "2026-07-08")] alias overEquiv_top := map_top
+@[deprecated (since := "2026-07-08")] alias overEquiv_symm_top := map_top
+@[deprecated (since := "2026-07-08")] alias overEquiv_bot := map_bot
+@[deprecated (since := "2026-07-08")] alias overEquiv_symm_bot := map_bot
+@[deprecated (since := "2026-07-08")] alias overEquiv_le_overEquiv_iff := RelIso.map_rel_iff
 
 set_option backward.defeqAttrib.useBackward true in
 lemma overEquiv_pullback {X : C} {Y₁ Y₂ : Over X} (f : Y₁ ⟶ Y₂) (S : Sieve Y₂) :
@@ -245,7 +249,7 @@ lemma mem_over_iff {X : C} {Y : Over X} (S : Sieve Y) :
 
 lemma overEquiv_symm_mem_over {X : C} (Y : Over X) (S : Sieve Y.left) (hS : S ∈ J Y.left) :
     (Sieve.overEquiv Y).symm S ∈ (J.over X) Y := by
-  simpa only [mem_over_iff, Equiv.apply_symm_apply] using hS
+  simpa only [mem_over_iff, OrderIso.apply_symm_apply] using hS
 
 lemma over_forget_coverPreserving (X : C) :
     CoverPreserving (J.over X) J (Over.forget X) where
@@ -528,7 +532,7 @@ lemma over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
   refine le_antisymm ?_ ?_
   · intro ⟨Y, right, (s : Y ⟶ X)⟩ R hR
     obtain ⟨(R : Sieve Y), rfl⟩ := (Sieve.overEquiv _).symm.surjective R
-    simp +instances only [GrothendieckTopology.mem_over_iff, Equiv.apply_symm_apply,
+    simp +instances only [GrothendieckTopology.mem_over_iff, OrderIso.apply_symm_apply,
       ← Precoverage.toGrothendieck_toCoverage, Coverage.mem_toGrothendieck,
       Over.left] at hR
     induction hR with
@@ -536,7 +540,6 @@ lemma over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
       rw [Sieve.overEquiv_symm_generate]
       exact .of _ _ (by simpa)
     | top =>
-      rw [Sieve.overEquiv_symm_top]
       simp
     | transitive Y R S hR H ih ih' =>
       refine GrothendieckTopology.transitive _ (ih s) _ fun Z g hg ↦ ?_
@@ -547,7 +550,8 @@ lemma over_toGrothendieck_eq_toGrothendieck_comap_forget (X : C) :
     intro Y R hR
     rw [Precoverage.mem_comap_iff] at hR
     rw [GrothendieckTopology.mem_toPrecoverage_iff, GrothendieckTopology.mem_over_iff,
-      Sieve.overEquiv, Equiv.coe_fn_mk, ← Sieve.generate_map_eq_functorPushforward]
+      Sieve.overEquiv, RelIso.coe_fn_mk, Equiv.coe_fn_mk,
+      ← Sieve.generate_map_eq_functorPushforward]
     exact Precoverage.Saturate.of _ _ hR
 
 end
diff --git a/Mathlib/CategoryTheory/Sites/Point/Over.lean b/Mathlib/CategoryTheory/Sites/Point/Over.lean
index a64e4cbffcf603..38514ec9ad53fb 100644
--- a/Mathlib/CategoryTheory/Sites/Point/Over.lean
+++ b/Mathlib/CategoryTheory/Sites/Point/Over.lean
@@ -50,7 +50,7 @@ def over : Point.{w} (J.over X) where
   jointly_surjective := by
     rintro U R hR ⟨u, hu⟩
     obtain ⟨R, rfl⟩ := (Sieve.overEquiv _).symm.surjective R
-    simp only [mem_over_iff, Equiv.apply_symm_apply] at hR
+    simp only [mem_over_iff, OrderIso.apply_symm_apply] at hR
     obtain ⟨Y, f, hf, v, rfl⟩ := Φ.jointly_surjective R hR u
     refine ⟨Over.mk (f ≫ U.hom), Over.homMk f, hf, ⟨v, ?_⟩, rfl⟩
     rw [FunctorToTypes.mem_fromOverSubfunctor_iff] at hu ⊢
@@ -71,7 +71,7 @@ lemma IsConservativeFamilyOfPoints.over
   mk' (fun Y S hS ↦ by
     obtain ⟨Y, f, rfl⟩ := Over.mk_surjective Y
     obtain ⟨S, rfl⟩ := (Sieve.overEquiv _).symm.surjective S
-    rw [mem_over_iff, Equiv.apply_symm_apply]
+    rw [mem_over_iff, OrderIso.apply_symm_apply]
     obtain ⟨ι, Z, g, rfl⟩ := S.exists_eq_ofArrows
     rw [hP.jointly_reflect_ofArrows_mem_of_small]
     intro Φ y
diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
index 45cd429c4147d0..81bf60530d4028 100644
--- a/Mathlib/CategoryTheory/Sites/Sieves.lean
+++ b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -757,8 +757,11 @@ theorem le_generate (R : Presieve X) : R ≤ generate R :=
 theorem generate_sieve (S : Sieve X) : generate S = S :=
   giGenerate.l_u_eq S
 
-lemma generate_mono : Monotone (generate : Presieve X → _) :=
-  (giGenerate (X := X)).gc.monotone_l
+@[gcongr]
+theorem generate_mono : Monotone (generate : Presieve X → Sieve X) := giGenerate.gc.monotone_l
+
+@[gcongr]
+theorem arrows_mono : Monotone (arrows : Sieve X → Presieve X) := giGenerate.gc.monotone_u
 
 /-- If the identity arrow is in a sieve, the sieve is maximal. -/
 theorem id_mem_iff_eq_top : S (𝟙 X) ↔ S = ⊤ :=
@@ -1469,6 +1472,9 @@ lemma Presieve.functorPullback_arrows {X : C} (S : Sieve (F.obj X)) :
     Presieve.functorPullback F S.arrows = Sieve.functorPullback F S :=
   rfl
 
+theorem Presieve.map_le_functorPushforward (S : Presieve X) : S.map F ≤ S.functorPushforward F := by
+  grw [← Sieve.arrows_generate_map_eq_functorPushforward, ← Sieve.le_generate]
+
 lemma Presieve.bind_ofArrows_le_bindOfArrows {ι : Type*} {X : C} (Z : ι → C)
     (f : ∀ i, Z i ⟶ X) (R : ∀ i, Presieve (Z i)) :
     Sieve.bind (Sieve.ofArrows Z f)