From 1b7f11c18bb54df4d220fe08644231f2dadce8bd Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 21:25:26 +0800
Subject: [PATCH 1/9] refactor(CategoryTheory/Sites): Allow non-fully-faithful
 dense subsites.

---
 .../CategoryTheory/Sites/DenseSubsite.lean    | 250 +++++++++++++-----
 Mathlib/CategoryTheory/Sites/Discrete.lean    |   4 +-
 .../CategoryTheory/Sites/InducedTopology.lean | 130 ++++-----
 3 files changed, 248 insertions(+), 136 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index 34106116dc1a8a..ec63a38f860257 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -7,6 +7,8 @@ import Mathlib.CategoryTheory.Sites.Sheaf
 import Mathlib.CategoryTheory.Sites.CoverLifting
 import Mathlib.CategoryTheory.Sites.CoverPreserving
 import Mathlib.CategoryTheory.Adjunction.FullyFaithful
+import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
+
 /-!
 # Dense subsites
 
@@ -123,15 +125,15 @@ theorem ext (ℱ : SheafOfTypes K) (X : D) {s t : ℱ.val.obj (op X)}
 
 variable {G}
 
-theorem functorPullback_pushforward_covering [Full G] {X : C}
+theorem functorPullback_pushforward_covering [G.IsLocallyFull K] {X : C}
     (T : K (G.obj X)) : (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X) := by
-  refine K.superset_covering ?_ (K.bind_covering T.property
-    fun Y f _ => G.is_cover_of_isCoverDense K Y)
-  rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', ⟨rfl⟩⟩, rfl⟩
-  use W; use G.preimage (f' ≫ f); use g
-  constructor
-  · simpa using T.val.downward_closed hf f'
-  · simp
+  refine K.transitive T.2 _ fun Y iYX hiYX ↦ ?_
+  apply K.transitive (G.is_cover_of_isCoverDense _ _) _
+  rintro W _ ⟨Z, iWZ, iZY, rfl⟩
+  rw [Sieve.pullback_comp]; apply K.pullback_stable; clear W iWZ
+  apply K.superset_covering ?_ (G.functorPushforward_hasLift_mem _ (iZY ≫ iYX))
+  rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩
+  exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩
 
 /-- (Implementation). Given a hom between the pullbacks of two sheaves, we can whisker it with
 `coyoneda` to obtain a hom between the pullbacks of the sheaves of maps from `X`.
@@ -154,12 +156,24 @@ theorem sheaf_eq_amalgamation (ℱ : Sheaf K A) {X : A} {U : D} {T : Sieve U} (h
     t = (ℱ.cond X T hT).amalgamate x hx :=
   (ℱ.cond X T hT).isSeparatedFor x t _ h ((ℱ.cond X T hT).isAmalgamation hx)
 
-variable [Full G]
+variable [G.IsLocallyFull K]
 
 namespace Types
 
 variable {ℱ : Dᵒᵖ ⥤ Type v} {ℱ' : SheafOfTypes.{v} K} (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val)
 
+theorem naturality_apply {X Y : C} (i : G.obj X ⟶ G.obj Y) (x) :
+    ℱ'.1.map i.op (α.app _ x) = α.app _ (ℱ.map i.op x) := by
+  have {X Y} (i : X ⟶ Y) (x) :
+      ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
+    exact congr_fun (α.naturality i.op).symm x
+  refine IsLocallyFull.ext G _ i fun V iVX iVY e ↦ ?_
+  simp only [comp_obj, types_comp_apply, ← FunctorToTypes.map_comp_apply, ← op_comp, ← e, this]
+
+@[reassoc]
+theorem naturality {X Y : C} (i : G.obj X ⟶ G.obj Y) :
+    α.app _ ≫ ℱ'.1.map i.op = ℱ.map i.op ≫ α.app _ := types_ext _ _ (naturality_apply α i)
+
 /--
 (Implementation). Given a section of `ℱ` on `X`, we can obtain a family of elements valued in `ℱ'`
 that is defined on a cover generated by the images of `G`. -/
@@ -180,20 +194,23 @@ noncomputable def pushforwardFamily {X} (x : ℱ.obj (op X)) :
 /-- (Implementation). The `pushforwardFamily` defined is compatible. -/
 theorem pushforwardFamily_compatible {X} (x : ℱ.obj (op X)) :
     (pushforwardFamily α x).Compatible := by
-  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ e
-  apply IsCoverDense.ext G
-  intro Y f
-  simp only [pushforwardFamily, ← FunctorToTypes.map_comp_apply, ← op_comp]
-  change (ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _) _ = (ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _) _
-  rw [← G.map_preimage (f ≫ g₁ ≫ _)]
-  rw [← G.map_preimage (f ≫ g₂ ≫ _)]
-  erw [← α.naturality (G.preimage _).op]
-  erw [← α.naturality (G.preimage _).op]
-  refine congr_fun ?_ x
-  simp only [Functor.comp_map, ← Category.assoc, Functor.op_map, Quiver.Hom.unop_op,
-    ← ℱ.map_comp, ← op_comp, G.map_preimage]
-  congr 3
-  simp [e]
+  have {X Y} (i : X ⟶ Y) (x) :
+      ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
+    exact congr_fun (α.naturality i.op).symm x
+  suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
+      (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
+      ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
+    rintro Y₁ Y₂ Z iZY₁ iZY₂ f₁ f₂ h₁ h₂ e
+    simp only [pushforwardFamily, ← FunctorToTypes.map_comp_apply, ← op_comp]
+    generalize Nonempty.some h₁ = l₁
+    generalize Nonempty.some h₂ = l₂
+    obtain ⟨W₁, iYW₁, iWX₁, rfl⟩ := l₁
+    obtain ⟨W₂, iYW₂, iWX₂, rfl⟩ := l₂
+    exact this _ _ _ _ (by simpa only [Category.assoc] using e)
+  introv e
+  refine ext G _ _ fun V iVZ ↦ ?_
+  simp only [← op_comp, ← FunctorToTypes.map_comp_apply, ← Functor.map_comp, naturality_apply,
+    Category.assoc, e]
 
 /-- (Implementation). The morphism `ℱ(X) ⟶ ℱ'(X)` given by gluing the `pushforwardFamily`. -/
 noncomputable def appHom (X : D) : ℱ.obj (op X) ⟶ ℱ'.val.obj (op X) := fun x =>
@@ -203,20 +220,10 @@ noncomputable def appHom (X : D) : ℱ.obj (op X) ⟶ ℱ'.val.obj (op X) := fun
 @[simp]
 theorem pushforwardFamily_apply {X} (x : ℱ.obj (op X)) {Y : C} (f : G.obj Y ⟶ X) :
     pushforwardFamily α x f (Presieve.in_coverByImage G f) = α.app (op Y) (ℱ.map f.op x) := by
-  unfold pushforwardFamily
-  -- Porting note: congr_fun was more powerful in Lean 3; I had to explicitly supply
-  -- the type of the first input here even though it's obvious (there is a unique occurrence
-  -- of x on each side of the equality)
-  refine congr_fun (?_ :
-    (fun t => ℱ'.val.map ((Nonempty.some (_ : coverByImage G X f)).lift.op)
-      (α.app (op (Nonempty.some (_ : coverByImage G X f)).1)
-        (ℱ.map ((Nonempty.some (_ : coverByImage G X f)).map.op) t))) =
-    (fun t => α.app (op Y) (ℱ.map (f.op) t))) x
-  rw [← G.map_preimage (Nonempty.some _ : Presieve.CoverByImageStructure _ _).lift]
-  change ℱ.map _ ≫ α.app (op _) ≫ ℱ'.val.map _ = ℱ.map f.op ≫ α.app (op Y)
-  erw [← α.naturality (G.preimage _).op]
-  simp only [← Functor.map_comp, ← Category.assoc, Functor.comp_map, G.map_preimage, G.op_map,
-    Quiver.Hom.unop_op, ← op_comp, Presieve.CoverByImageStructure.fac]
+  simp only [pushforwardFamily_def, op_obj]
+  generalize Nonempty.some (Presieve.in_coverByImage G f) = l
+  obtain ⟨W, iYW, iWX, rfl⟩ := l
+  simp only [← op_comp, ← FunctorToTypes.map_comp_apply, naturality_apply]
 
 @[simp]
 theorem appHom_restrict {X : D} {Y : C} (f : op X ⟶ op (G.obj Y)) (x) :
@@ -399,10 +406,9 @@ theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
   congr 1
   simp only [Category.assoc]
   congr 1
-  rw [← G.map_preimage hf.some.map]
-  symm
-  apply α.naturality (G.preimage hf.some.map).op
-  -- porting note; Lean 3 needed a random `inferInstance` for cleanup here; not necessary in lean 4
+  have := naturality_apply (G := G) (ℱ := ℱ ⋙ coyoneda.obj (op <| (G.op ⋙ ℱ).obj X))
+    (ℱ' := ⟨_, ℱ'.2 ((G.op ⋙ ℱ).obj X)⟩) (whiskerRight α (coyoneda.obj _)) hf.some.map (𝟙 _)
+  simpa using this
 
 variable (G)
 
@@ -449,19 +455,20 @@ theorem iso_of_restrict_iso {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIs
 variable (G K)
 
 /-- A fully faithful cover-dense functor preserves compatible families. -/
-lemma compatiblePreserving [Faithful G] : CompatiblePreserving K G := by
+lemma compatiblePreserving [G.IsLocallyFaithful K] : CompatiblePreserving K G := by
   constructor
   intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ eq
   apply Functor.IsCoverDense.ext G
   intro W i
-  simp only [← FunctorToTypes.map_comp_apply, ← op_comp]
-  rw [← G.map_preimage (i ≫ f₁)]
-  rw [← G.map_preimage (i ≫ f₂)]
-  apply hx (G.preimage (i ≫ f₁)) ((G.preimage (i ≫ f₂))) hg₁ hg₂
-  apply G.map_injective
-  simp [eq]
-
-lemma isContinuous [Faithful G] (Hp : CoverPreserving J K G) : G.IsContinuous J K :=
+  refine IsLocallyFull.ext G _ (i ≫ f₁) fun V₁ iVW iV₁Y₁ e₁ ↦ ?_
+  refine IsLocallyFull.ext G _ (G.map iVW ≫ i ≫ f₂) fun V₂ iV₂V₁ iV₂Y₂ e₂ ↦ ?_
+  refine IsLocallyFaithful.ext G _ (iV₂V₁ ≫ iV₁Y₁ ≫ g₁) (iV₂Y₂ ≫ g₂) (by simp [e₁, e₂, eq]) ?_
+  intro V₃ iV₃ e₄
+  simp only [← op_comp, ← FunctorToTypes.map_comp_apply, ← e₁, ← e₂, ← Functor.map_comp]
+  apply hx
+  simpa using e₄
+
+lemma isContinuous [G.IsLocallyFaithful K] (Hp : CoverPreserving J K G) : G.IsContinuous J K :=
   isContinuous_of_coverPreserving (compatiblePreserving K G) Hp
 
 instance full_sheafPushforwardContinuous [G.IsContinuous J K] :
@@ -482,33 +489,156 @@ end IsCoverDense
 /-- If `G : C ⥤ D` is cover dense and full, then the
 map `(P ⟶ Q) → (G.op ⋙ P ⟶ G.op ⋙ Q)` is bijective when `Q` is a sheaf`. -/
 lemma whiskerLeft_obj_map_bijective_of_isCoverDense (G : C ⥤ D)
-    [G.IsCoverDense K] [G.Full] {A : Type*} [Category A]
+    [G.IsCoverDense K] [G.IsLocallyFull K] {A : Type*} [Category A]
     (P Q : Dᵒᵖ ⥤ A) (hQ : Presheaf.IsSheaf K Q) :
     Function.Bijective (((whiskeringLeft Cᵒᵖ Dᵒᵖ A).obj G.op).map : (P ⟶ Q) → _) :=
   (IsCoverDense.restrictHomEquivHom (ℱ' := ⟨Q, hQ⟩)).symm.bijective
 
+variable {A : Type*} [Category A]
+variable (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : C ⥤ D)
+
+/-- The functor `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)`
+if `G` is cover-dense, locally fully-faithful,
+and `S` is a cover of `C` if and only if the image of `S` in `D` is a cover. -/
+class IsDenseSubsite : Prop where
+  isCoverDense' : G.IsCoverDense K
+  isLocallyFull' : G.IsLocallyFull K
+  isLocallyFaithful' : G.IsLocallyFaithful K
+  functorPushforward_mem_iff : ∀ {X : C} {S : Sieve X}, S.functorPushforward G ∈ K _ ↔ S ∈ J _
+
+namespace IsDenseSubsite
+
+variable [G.IsDenseSubsite J K]
+
+lemma isCoverDense : G.IsCoverDense K := isCoverDense' J
+lemma isLocallyFull : G.IsLocallyFull K := isLocallyFull' J
+lemma isLocallyFaithful : G.IsLocallyFaithful K := isLocallyFaithful' J
+
+lemma coverPreserving [G.IsDenseSubsite J K] : CoverPreserving J K G :=
+  ⟨functorPushforward_mem_iff.mpr⟩
+
+instance (priority := 900) [G.IsDenseSubsite J K] : G.IsContinuous J K :=
+  letI := IsDenseSubsite.isCoverDense J K G
+  letI := IsDenseSubsite.isLocallyFull J K G
+  letI := IsDenseSubsite.isLocallyFaithful J K G
+  IsCoverDense.isContinuous J K G (IsDenseSubsite.coverPreserving J K G)
+
+instance (priority := 900) [G.IsDenseSubsite J K] : G.IsCocontinuous J K where
+  cover_lift hS :=
+    letI := IsDenseSubsite.isCoverDense J K G
+    letI := IsDenseSubsite.isLocallyFull J K G
+    IsDenseSubsite.functorPushforward_mem_iff.mp
+      (IsCoverDense.functorPullback_pushforward_covering ⟨_, hS⟩)
+
+instance full_sheafPushforwardContinuous [G.IsDenseSubsite J K] :
+    Full (G.sheafPushforwardContinuous A J K) :=
+  letI := IsDenseSubsite.isCoverDense J K G
+  letI := IsDenseSubsite.isLocallyFull J K G
+  inferInstance
+
+instance faithful_sheafPushforwardContinuous [G.IsDenseSubsite J K] :
+    Faithful (G.sheafPushforwardContinuous A J K) :=
+  letI := IsDenseSubsite.isCoverDense J K G
+  letI := IsDenseSubsite.isLocallyFull J K G
+  inferInstance
+
+lemma hasLift_mem [G.IsDenseSubsite J K] {U V} (f : G.obj U ⟶ G.obj V) :
+    Sieve.hasLift G f ∈ J _ :=
+  letI := IsDenseSubsite.isLocallyFull J K G
+  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_hasLift_mem K f)
+
+lemma equalizer_mem [G.IsDenseSubsite J K] {U V} (f₁ f₂ : U ⟶ V) (e : G.map f₁ = G.map f₂) :
+    Sieve.equalizer f₁ f₂ ∈ J _ :=
+  letI := IsDenseSubsite.isLocallyFaithful J K G
+  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_equalizer_mem K f₁ f₂ e)
+
+end IsDenseSubsite
+
 end Functor
 
 end CategoryTheory
 
 namespace CategoryTheory.Functor.IsCoverDense
 
-open CategoryTheory
+open CategoryTheory Opposite
 
 universe w'
 variable {C D : Type*} [Category C] [Category D]
-variable (G : C ⥤ D) [Full G] [Faithful G]
+variable (G : C ⥤ D)
 variable (J : GrothendieckTopology C) (K : GrothendieckTopology D)
 variable {A : Type w} [Category.{w'} A] [∀ X, Limits.HasLimitsOfShape (StructuredArrow X G.op) A]
-variable [G.IsCoverDense K] [G.IsContinuous J K] [G.IsCocontinuous J K]
+variable [G.IsDenseSubsite J K]
+
+lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
+    IsIso ((yoneda.map ((G.op.ranCounit.app Y.val).app (op U))).app (op X)) := by
+  rw [isIso_iff_bijective]
+  constructor
+  · intro f₁ f₂ e
+    apply (isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).hom_ext
+    rintro ⟨⟨⟨⟩⟩, ⟨W⟩, g⟩
+    obtain ⟨g, rfl⟩ : ∃ g' : G.obj W ⟶ G.obj U, g = g'.op := ⟨g.unop, rfl⟩
+    simp only [id_obj, comp_obj, StructuredArrow.proj_obj, RightExtension.coneAt_pt,
+      RightExtension.mk_left, RightExtension.coneAt_π_app, const_obj_obj, op_obj,
+      whiskeringLeft_obj_obj, RightExtension.mk_hom]
+    apply (Y.2 X _ (IsDenseSubsite.hasLift_mem J K G g)).isSeparatedFor.ext
+    rintro V iVW ⟨iVU, e'⟩
+    have := congr($e ≫ Y.1.map iVU.op)
+    simp only [comp_obj, yoneda_map_app, Category.assoc, coyoneda_obj_obj, comp_map,
+      coyoneda_obj_map, ← NatTrans.naturality, op_obj, op_map, Quiver.Hom.unop_op, ← map_comp_assoc,
+      ← op_comp, ← e'] at this ⊢
+    erw [← NatTrans.naturality] at this
+    exact this
+  · intro f
+    have (X Y Z) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : Sieve.hasLift G g f) : Exists _ := hf
+    choose l hl using this
+    let c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.val) := by
+      refine ⟨X, ⟨fun g ↦ ?_, ?_⟩⟩
+      · refine Y.2.amalgamate ⟨_, IsDenseSubsite.hasLift_mem J K G g.hom.unop⟩
+          (fun I ↦ f ≫ Y.1.map (l _ _ _ _ _ I.hf).op) fun I₁ I₂ r ↦ ?_
+        apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (r.g₁ ≫ l _ _ _ _ _ I₁.hf)
+          (r.g₂ ≫ l _ _ _ _ _ I₂.hf) ?_)).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
+        · simp only [const_obj_obj, op_obj, map_comp, hl]
+          simp only [← map_comp_assoc, r.w]
+        · simp [← map_comp, ← op_comp, hiUV]
+      · rintro ⟨⟨⟨⟩⟩, ⟨W₁⟩, g₁⟩ ⟨⟨⟨⟩⟩, ⟨W₂⟩, g₂⟩ ⟨⟨⟨⟨⟩⟩⟩, i, hi⟩
+        dsimp at g₁ g₂ i hi
+        obtain rfl : g₂ = g₁ ≫ (G.map i.unop).op := by simpa only [Category.id_comp] using hi
+        obtain ⟨g, rfl⟩ : ∃ g' : G.obj W₁ ⟶ G.obj U, g₁ = g'.op := ⟨g₁.unop, rfl⟩
+        obtain ⟨i, rfl⟩ : ∃ i' : W₂ ⟶ W₁, i = i'.op := ⟨i.unop, rfl⟩
+        simp only [const_obj_obj, id_obj, comp_obj, StructuredArrow.proj_obj, const_obj_map, op_obj,
+          unop_comp, Quiver.Hom.unop_op, Category.id_comp, comp_map, StructuredArrow.proj_map]
+        apply Y.2.hom_ext ⟨_, IsDenseSubsite.hasLift_mem J K G (G.map i ≫ g)⟩
+        intro I
+        simp only [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← Functor.map_comp, ← op_comp]
+        let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.hasLift_mem J K G g⟩ :=
+          ⟨_, I.f ≫ i, ⟨l _ _ _ _ _ I.hf, by simp [hl]⟩⟩
+        refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm
+        apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
+          (l _ _ _ _ _ I'.hf) (by simp [hl]))).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
+        simp [← Functor.map_comp, ← op_comp, hiUV]
+    refine ⟨(isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).lift c, ?_⟩
+    · have := (isPointwiseRightKanExtensionRanCounit G.op Y.1 (.op (G.obj U))).fac c (.mk (𝟙 _))
+      simp only [id_obj, comp_obj, StructuredArrow.proj_obj, StructuredArrow.mk_right,
+        RightExtension.coneAt_pt, RightExtension.mk_left, RightExtension.coneAt_π_app,
+        const_obj_obj, op_obj, StructuredArrow.mk_hom_eq_self, map_id, whiskeringLeft_obj_obj,
+        RightExtension.mk_hom, Category.id_comp, StructuredArrow.mk_left, unop_id] at this
+      simp only [id_obj, yoneda_map_app, this]
+      apply Y.2.hom_ext ⟨_, IsDenseSubsite.hasLift_mem J K G (𝟙 (G.obj U))⟩ _ _ fun I ↦ ?_
+      apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
+        I.f (by simp [hl]))).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
+      simp [← Functor.map_comp, ← op_comp, hiUV]
 
 instance (Y : Sheaf J A) : IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y) := by
-    haveI : IsIso ((sheafToPresheaf J A).map
-        ((G.sheafAdjunctionCocontinuous A J K).counit.app Y)) := by
-      dsimp
-      rw [sheafAdjunctionCocontinuous_counit_app_val]
-      infer_instance
-    apply ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
+  apply (config := { allowSynthFailures := true })
+  ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
+  apply (config := { allowSynthFailures := true }) NatIso.isIso_of_isIso_app
+  intro ⟨U⟩
+  apply (config := { allowSynthFailures := true }) ReflectsIsomorphisms.reflects yoneda
+  apply (config := { allowSynthFailures := true }) NatIso.isIso_of_isIso_app
+  intro ⟨X⟩
+  simp only [comp_obj, sheafToPresheaf_obj, sheafPushforwardContinuous_obj_val_obj, yoneda_obj_obj,
+    id_obj, sheafToPresheaf_map, sheafAdjunctionCocontinuous_counit_app_val, ranAdjunction_counit]
+  exact isIso_ranCounit_app_of_isDenseSubsite G J K Y U X
 
 variable (A)
 
diff --git a/Mathlib/CategoryTheory/Sites/Discrete.lean b/Mathlib/CategoryTheory/Sites/Discrete.lean
index 978e0410f3691b..01def9d01d1c3b 100644
--- a/Mathlib/CategoryTheory/Sites/Discrete.lean
+++ b/Mathlib/CategoryTheory/Sites/Discrete.lean
@@ -76,9 +76,9 @@ lemma isDiscrete_iff_isIso_counit_app {L : A ⥤ Sheaf J A} (adj : L ⊣ (sheafS
 section Equivalence
 
 variable {D : Type*} [Category D] (K : GrothendieckTopology D) [HasWeakSheafify K A]
-variable (G : C ⥤ D) [G.Full] [G.Faithful]
+variable (G : C ⥤ D)
   [∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A]
-  [G.IsCoverDense K] [G.IsContinuous J K] [G.IsCocontinuous J K] (ht' : IsTerminal (G.obj t))
+  [G.IsDenseSubsite J K] (ht' : IsTerminal (G.obj t))
 
 variable [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
 
diff --git a/Mathlib/CategoryTheory/Sites/InducedTopology.lean b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
index 3d71abeb6d788b..e84f80c62209ef 100644
--- a/Mathlib/CategoryTheory/Sites/InducedTopology.lean
+++ b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
@@ -29,37 +29,35 @@ Given a fully faithful cover-dense functor `G : C ⥤ (D, K)` between small site
 
 -/
 
-
 namespace CategoryTheory
 
 universe v u
 
-open Limits Opposite Presieve
-
-section
+open Limits Opposite Presieve CategoryTheory
 
-variable {C : Type*} [Category C] {D : Type*} [Category D] {G : C ⥤ D}
-variable {J : GrothendieckTopology C} {K : GrothendieckTopology D}
+variable {C : Type*} [Category C] {D : Type*} [Category D] (G : C ⥤ D)
+variable {J : GrothendieckTopology C} (K : GrothendieckTopology D)
 variable (A : Type v) [Category.{u} A]
 
+namespace Functor
+
 -- variables (A) [full G] [faithful G]
 /-- We say that a functor `C ⥤ D` into a site is "locally dense" if
 for each covering sieve `T` in `D`, `T ∩ mor(C)` generates a covering sieve in `D`.
 -/
-def LocallyCoverDense (K : GrothendieckTopology D) (G : C ⥤ D) : Prop :=
-  ∀ ⦃X : C⦄ (T : K (G.obj X)), (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X)
-
-namespace LocallyCoverDense
+class LocallyCoverDense : Prop where
+  functorPushforward_functorPullback_mem :
+    ∀ ⦃X : C⦄ (T : K (G.obj X)), (T.val.functorPullback G).functorPushforward G ∈ K (G.obj X)
 
-variable [G.Full] [G.Faithful] (Hld : LocallyCoverDense K G)
+variable [G.LocallyCoverDense K] [G.IsLocallyFull K] [G.IsLocallyFaithful K]
 
-theorem pushforward_cover_iff_cover_pullback {X : C} (S : Sieve X) :
+theorem pushforward_cover_iff_cover_pullback [G.Full] [G.Faithful] {X : C} (S : Sieve X) :
     K _ (S.functorPushforward G) ↔ ∃ T : K (G.obj X), T.val.functorPullback G = S := by
   constructor
   · intro hS
     exact ⟨⟨_, hS⟩, (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S⟩
   · rintro ⟨T, rfl⟩
-    exact Hld T
+    exact LocallyCoverDense.functorPushforward_functorPullback_mem T
 
 /-- If a functor `G : C ⥤ (D, K)` is fully faithful and locally dense,
 then the set `{ T ∩ mor(C) | T ∈ K }` is a grothendieck topology of `C`.
@@ -71,15 +69,23 @@ def inducedTopology : GrothendieckTopology C where
     change K _ _
     rw [Sieve.functorPushforward_top]
     exact K.top_mem _
-  pullback_stable' X Y S f hS := by
-    have : S.pullback f = ((S.functorPushforward G).pullback (G.map f)).functorPullback G := by
-      conv_lhs => rw [← (Sieve.fullyFaithfulFunctorGaloisCoinsertion G X).u_l_eq S]
-      ext
-      change (S.functorPushforward G) _ ↔ (S.functorPushforward G) _
-      rw [G.map_comp]
-    rw [this]
-    change K _ _
-    apply Hld ⟨_, K.pullback_stable (G.map f) hS⟩
+  pullback_stable' X Y S iYX hS := by
+    apply K.transitive (LocallyCoverDense.functorPushforward_functorPullback_mem
+      ⟨_, K.pullback_stable (G.map iYX) hS⟩)
+    rintro Z _ ⟨U, iUY, iZU, ⟨W, iWX, iUW, hiWX, e₁⟩, rfl⟩
+    rw [Sieve.pullback_comp]
+    apply K.pullback_stable
+    clear iZU Z
+    apply K.transitive (G.functorPushforward_hasLift_mem _ iUW)
+    rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
+    rw [Sieve.pullback_comp]
+    apply K.pullback_stable
+    clear iZU₁ Z
+    apply K.superset_covering ?_ (G.functorPushforward_equalizer_mem _
+      (iU₁U ≫ iUY ≫ iYX) (iU₁W ≫ iWX) (by simp [e₁, e₂]))
+    rintro Z _ ⟨U₂, iU₂U₁, iZU₂, e₃ : _ = _, rfl⟩
+    refine ⟨_, iU₂U₁ ≫ iU₁U ≫ iUY, iZU₂, ?_, by simp⟩
+    simpa [e₃] using S.downward_closed hiWX (iU₂U₁ ≫ iU₁W)
   transitive' X S hS S' H' := by
     apply K.transitive hS
     rintro Y _ ⟨Z, g, i, hg, rfl⟩
@@ -91,74 +97,50 @@ def inducedTopology : GrothendieckTopology C where
     simp
 
 /-- `G` is cover-lifting wrt the induced topology. -/
-theorem inducedTopology_isCocontinuous : G.IsCocontinuous Hld.inducedTopology K :=
-  ⟨@fun _ S hS => Hld ⟨S, hS⟩⟩
+instance inducedTopology_isCocontinuous : G.IsCocontinuous (G.inducedTopology K) K :=
+  ⟨@fun _ S hS => LocallyCoverDense.functorPushforward_functorPullback_mem ⟨S, hS⟩⟩
 
 /-- `G` is cover-preserving wrt the induced topology. -/
-theorem inducedTopology_coverPreserving : CoverPreserving Hld.inducedTopology K G :=
+theorem inducedTopology_coverPreserving : CoverPreserving (G.inducedTopology K) K G :=
   ⟨@fun _ _ hS => hS⟩
 
-end LocallyCoverDense
-
-variable (G K)
+instance (priority := 900) locallyCoverDense_of_isCoverDense [G.IsCoverDense K] :
+    G.LocallyCoverDense K where
+  functorPushforward_functorPullback_mem _ _ :=
+    IsCoverDense.functorPullback_pushforward_covering _
 
-theorem Functor.locallyCoverDense_of_isCoverDense [Full G] [G.IsCoverDense K] :
-    LocallyCoverDense K G := by
-  intro X T
-  refine K.superset_covering ?_ (K.bind_covering T.property
-    fun Y f _ => G.is_cover_of_isCoverDense _ Y)
-  rintro Y _ ⟨Z, _, f, hf, ⟨W, g, f', rfl : _ = _⟩, rfl⟩
-  use W; use G.preimage (f' ≫ f); use g
-  constructor
-  · simpa using T.val.downward_closed hf f'
-  · simp
+instance (priority := 900) [G.IsCoverDense K] : G.IsDenseSubsite (G.inducedTopology K) K where
+  isCoverDense' := inferInstance
+  isLocallyFull' := inferInstance
+  isLocallyFaithful' := inferInstance
+  functorPushforward_mem_iff := Iff.rfl
 
-/-- Given a fully faithful cover-dense functor `G : C ⥤ (D, K)`, we may induce a topology on `C`.
--/
-abbrev Functor.inducedTopologyOfIsCoverDense [Full G] [Faithful G] [G.IsCoverDense K] :
-    GrothendieckTopology C :=
-  (G.locallyCoverDense_of_isCoverDense K).inducedTopology
+@[deprecated (since := "2024-07-23")]
+alias inducedTopologyOfIsCoverDense := inducedTopology
 
 variable (J)
 
-theorem over_forget_locallyCoverDense (X : C) : LocallyCoverDense J (Over.forget X) := by
-  intro Y T
-  convert T.property
-  ext Z f
-  constructor
-  · rintro ⟨_, _, g', hg, rfl⟩
-    exact T.val.downward_closed hg g'
-  · intro hf
-    exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩
-
-end
-
-section SmallSite
-
-variable {C : Type v} [SmallCategory C] {D : Type v} [SmallCategory D] {G : C ⥤ D}
-variable {J : GrothendieckTopology C} {K : GrothendieckTopology D}
-variable (A : Type u) [Category.{v} A]
-
-instance [G.Full] [G.Faithful] [G.IsCoverDense K]  :
-    Functor.IsContinuous G (G.inducedTopologyOfIsCoverDense K) K := by
-  apply Functor.IsCoverDense.isContinuous
-  exact (G.locallyCoverDense_of_isCoverDense K).inducedTopology_coverPreserving
-
-instance [G.Full] [G.Faithful] [G.IsCoverDense K]  :
-    Functor.IsCocontinuous G (G.inducedTopologyOfIsCoverDense K) K :=
-  (G.locallyCoverDense_of_isCoverDense K).inducedTopology_isCocontinuous
+instance over_forget_locallyCoverDense (X : C) : (Over.forget X).LocallyCoverDense J where
+  functorPushforward_functorPullback_mem Y T := by
+    convert T.property
+    ext Z f
+    constructor
+    · rintro ⟨_, _, g', hg, rfl⟩
+      exact T.val.downward_closed hg g'
+    · intro hf
+      exact ⟨Over.mk (f ≫ Y.hom), Over.homMk f, 𝟙 _, hf, (Category.id_comp _).symm⟩
 
 /-- Cover-dense functors induces an equivalence of categories of sheaves.
 
 This is known as the comparison lemma. It requires that the sites are small and the value category
 is complete.
 -/
-noncomputable def Functor.sheafInducedTopologyEquivOfIsCoverDense [Full G] [Faithful G]
-    [G.IsCoverDense K] [HasLimits A] :
-    Sheaf (G.inducedTopologyOfIsCoverDense K) A ≌ Sheaf K A :=
+noncomputable def sheafInducedTopologyEquivOfIsCoverDense
+    [G.IsCoverDense K] [∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A] :
+    Sheaf (G.inducedTopology K) A ≌ Sheaf K A :=
   Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting G
-    (G.inducedTopologyOfIsCoverDense K) K A
+    (G.inducedTopology K) K A
 
-end SmallSite
+end Functor
 
 end CategoryTheory

From 9156c316ef21bb9e81a6c8d6a081dfba70572711 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 22:37:22 +0800
Subject: [PATCH 2/9] fix

---
 Mathlib/CategoryTheory/Sites/Equivalence.lean | 123 ++++++++++--------
 .../Sites/LocallyFullyFaithful.lean           | 122 +++++++++++++++++
 2 files changed, 188 insertions(+), 57 deletions(-)
 create mode 100644 Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean

diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean
index 5808937e197f42..f5842af8d091ca 100644
--- a/Mathlib/CategoryTheory/Sites/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Sites/Equivalence.lean
@@ -46,53 +46,48 @@ variable {C : Type u₁} [Category.{v₁} C] (J : GrothendieckTopology C)
 variable {D : Type u₂} [Category.{v₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (G : D ⥤ C)
 variable (A : Type u₃) [Category.{v₃} A]
 
-namespace Equivalence
-
-theorem locallyCoverDense : LocallyCoverDense J e.inverse := by
-  intro X T
-  convert T.prop
-  ext Z f
+variable {J} in
+lemma pullback_mem_iff_of_isIso {X Y : C} {i : X ⟶ Y} [IsIso i] {S : Sieve Y} :
+    S.pullback i ∈ J _ ↔ S ∈ J _ := by
+  refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
+  convert J.pullback_stable (inv i) H
+  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
+
+@[simp]
+lemma Sieve.comp_mem_iff {X Y Z : C} (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) :
+    S (i ≫ f) ↔ S f := by
+  refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
+  convert S.downward_closed H (inv i)
+  simp
+
+lemma Sieve.functorPushforward_functor {X} (S : Sieve X) :
+    S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse := by
+  ext Y iYX
   constructor
-  · rintro ⟨_, _, g', hg, rfl⟩
-    exact T.val.downward_closed hg g'
-  · intro hf
-    refine ⟨e.functor.obj Z, (Adjunction.homEquiv e.toAdjunction _ _).symm f, e.unit.app Z, ?_, ?_⟩
-    · simp only [Adjunction.homEquiv_counit, Functor.id_obj, Equivalence.toAdjunction_counit,
-        Sieve.functorPullback_apply, Presieve.functorPullback_mem, Functor.map_comp,
-        Equivalence.inv_fun_map, Functor.comp_obj, Category.assoc, Equivalence.unit_inverse_comp,
-        Category.comp_id]
-      exact T.val.downward_closed hf _
-    · simp
-
-theorem coverPreserving : CoverPreserving J (e.locallyCoverDense J).inducedTopology e.functor where
-  cover_preserve {U S} h := by
-    change _ ∈ J.sieves (e.inverse.obj (e.functor.obj U))
-    convert J.pullback_stable (e.unitInv.app U) h
-    ext Z f
-    rw [← Sieve.functorPushforward_comp]
-    simp only [Sieve.functorPushforward_apply, Presieve.functorPushforward, exists_and_left, id_obj,
-      comp_obj, Sieve.pullback_apply]
-    constructor
-    · rintro ⟨W, g, hg, x, rfl⟩
-      rw [Category.assoc]
-      apply S.downward_closed
-      simpa using S.downward_closed hg _
-    · intro hf
-      exact ⟨_, e.unitInv.app Z ≫ f ≫ e.unitInv.app U, S.downward_closed hf _,
-        e.unit.app Z ≫ e.unit.app _, by simp⟩
-
-instance : IsCoverDense e.functor (e.locallyCoverDense J).inducedTopology where
-  is_cover U := by
-    change _ ∈ J.sieves _
-    convert J.top_mem (e.inverse.obj U)
-    ext Y f
-    simp only [Sieve.functorPushforward_apply, Presieve.functorPushforward, exists_and_left,
-      Sieve.top_apply, iff_true]
-    exact ⟨e.functor.obj Y, (Adjunction.homEquiv e.toAdjunction _ _).symm f,
-      Presieve.in_coverByImage _ _, e.unit.app _, by simp⟩
+  · rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩
+    simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)
+  · intro H
+    exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩
+
+@[simp]
+lemma Sieve.mem_functorPushforward_functor {X Y} {S : Sieve X} {f : Y ⟶ e.functor.obj X} :
+    S.functorPushforward e.functor f ↔ S (e.inverse.map f ≫ e.unitInv.app X) :=
+  congr($(S.functorPushforward_functor e).arrows f)
 
-instance : IsCoverDense e.inverse J where
+lemma Sieve.functorPushforward_inverse {X} (S : Sieve X) :
+    S.functorPushforward e.inverse = (S.pullback (e.counit.app X)).functorPullback e.functor :=
+  Sieve.functorPushforward_functor e.symm S
+
+@[simp]
+lemma Sieve.mem_functorPushforward_inverse {X Y} {S : Sieve X} {f : Y ⟶ e.inverse.obj X} :
+    S.functorPushforward e.inverse f ↔ S (e.functor.map f ≫ e.counit.app X) :=
+  congr($(S.functorPushforward_inverse e).arrows f)
+
+namespace Equivalence
+
+instance (priority := 900) [G.IsEquivalence] : IsCoverDense G J where
   is_cover U := by
+    let e := (asEquivalence G).symm
     convert J.top_mem U
     ext Y f
     simp only [Sieve.functorPushforward_apply, Presieve.functorPushforward, exists_and_left,
@@ -102,16 +97,30 @@ instance : IsCoverDense e.inverse J where
     replace := Sieve.downward_closed _ this (e.unit.app Y)
     simpa [g] using this
 
+theorem locallyCoverDense : e.inverse.LocallyCoverDense J := inferInstance
+
+instance : e.functor.IsDenseSubsite J (e.inverse.inducedTopology J) := by
+  have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) := by
+    ext X S
+    show _ ↔ _ ∈ J.sieves _
+    erw [← pullback_mem_iff_of_isIso (i := e.unit.app X)]
+    congr!; ext Y f; simp
+  nth_rw 1 [this]
+  infer_instance
+
+theorem coverPreserving : CoverPreserving J (e.inverse.inducedTopology J) e.functor :=
+  IsDenseSubsite.coverPreserving _ _ _
+
 /-- A class saying that the equivalence `e` transports the Grothendieck topology `J` to `K`. -/
 class TransportsGrothendieckTopology : Prop where
   /-- `K` is equal to the induced topology. -/
-  eq_inducedTopology : K = (e.locallyCoverDense J).inducedTopology
+  eq_inducedTopology : K = e.inverse.inducedTopology J
 
-instance : e.TransportsGrothendieckTopology J (e.locallyCoverDense J).inducedTopology := ⟨rfl⟩
+instance : e.TransportsGrothendieckTopology J (e.inverse.inducedTopology J) := ⟨rfl⟩
 
 variable [e.TransportsGrothendieckTopology J K]
 
-theorem eq_inducedTopology_of_transports : K = (e.locallyCoverDense J).inducedTopology :=
+theorem eq_inducedTopology_of_transports : K = e.inverse.inducedTopology J :=
   TransportsGrothendieckTopology.eq_inducedTopology
 
 instance : IsContinuous e.functor J K := by
@@ -120,7 +129,7 @@ instance : IsContinuous e.functor J K := by
 
 instance : IsContinuous e.inverse K J := by
   rw [eq_inducedTopology_of_transports J K e]
-  exact IsCoverDense.isContinuous _ _ _ (e.locallyCoverDense J).inducedTopology_coverPreserving
+  infer_instance
 
 /-- The functor in the equivalence of sheaf categories. -/
 @[simps!]
@@ -215,13 +224,13 @@ end Equivalence
 
 variable [EssentiallySmall.{w} C]
 variable (B : Type*) [Category B] (F : A ⥤ B)
-variable [HasSheafify ((equivSmallModel C).locallyCoverDense J).inducedTopology A]
-variable [((equivSmallModel C).locallyCoverDense J).inducedTopology.HasSheafCompose F]
+variable [HasSheafify ((equivSmallModel C).inverse.inducedTopology J) A]
+variable [((equivSmallModel C).inverse.inducedTopology J).HasSheafCompose F]
 
 /-- Transport to a small model and sheafify there. -/
 noncomputable
 def smallSheafify : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A := (equivSmallModel C).transportAndSheafify J
-  ((equivSmallModel C).locallyCoverDense J).inducedTopology A
+  ((equivSmallModel C).inverse.inducedTopology J) A
 
 /--
 Transporting to a small model and sheafifying there is left adjoint to the underlying presheaf
@@ -232,22 +241,22 @@ def smallSheafificationAdjunction : smallSheafify J A ⊣ sheafToPresheaf J A :=
   (equivSmallModel C).transportSheafificationAdjunction J _ A
 
 noncomputable instance hasSheafifyEssentiallySmallSite : HasSheafify J A :=
-  (equivSmallModel C).hasSheafify J ((equivSmallModel C).locallyCoverDense J).inducedTopology A
+  (equivSmallModel C).hasSheafify J ((equivSmallModel C).inverse.inducedTopology J) A
 
 instance hasSheafComposeEssentiallySmallSite : HasSheafCompose J F :=
-  (equivSmallModel C).hasSheafCompose J ((equivSmallModel C).locallyCoverDense J).inducedTopology F
+  (equivSmallModel C).hasSheafCompose J ((equivSmallModel C).inverse.inducedTopology J) F
 
 instance hasLimitsEssentiallySmallSite
-    [HasLimits <| Sheaf ((equivSmallModel C).locallyCoverDense J).inducedTopology A] :
+    [HasLimits <| Sheaf ((equivSmallModel C).inverse.inducedTopology J) A] :
     HasLimitsOfSize.{max v₃ w, max v₃ w} <| Sheaf J A :=
   Adjunction.has_limits_of_equivalence ((equivSmallModel C).sheafCongr J
-    ((equivSmallModel C).locallyCoverDense J).inducedTopology A).functor
+    ((equivSmallModel C).inverse.inducedTopology J) A).functor
 
 instance hasColimitsEssentiallySmallSite
-    [HasColimits <| Sheaf ((equivSmallModel C).locallyCoverDense J).inducedTopology A] :
+    [HasColimits <| Sheaf ((equivSmallModel C).inverse.inducedTopology J) A] :
     HasColimitsOfSize.{max v₃ w, max v₃ w} <| Sheaf J A :=
   Adjunction.has_colimits_of_equivalence ((equivSmallModel C).sheafCongr J
-    ((equivSmallModel C).locallyCoverDense J).inducedTopology A).functor
+    ((equivSmallModel C).inverse.inducedTopology J) A).functor
 
 namespace GrothendieckTopology
 
diff --git a/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean b/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
new file mode 100644
index 00000000000000..fc04a809840ad5
--- /dev/null
+++ b/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.CategoryTheory.Sites.SheafOfTypes
+
+/-!
+# Dense subsites
+
+We define `IsCoverDense` functors into sites as functors such that there exists a covering sieve
+that factors through images of the functor for each object in `D`.
+
+## Main results
+
+- `CategoryTheory.Functor.IsCoverDense.Types.presheafHom`: If `G : C ⥤ (D, K)` is
+  and cover-dense, then given any presheaf `ℱ` and sheaf `ℱ'` on `D`,
+  and a morphism `α : G ⋙ ℱ ⟶ G ⋙ ℱ'`, we may glue them together to obtain
+  a morphism of presheaves `ℱ ⟶ ℱ'`.
+- `CategoryTheory.Functor.IsCoverDense.sheafIso`: If `ℱ` above is a sheaf and `α` is an iso,
+  then the result is also an iso.
+- `CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso`: If `G : C ⥤ (D, K)` is
+  and cover-dense, then given any sheaves `ℱ, ℱ'` on `D`, and a morphism `α : ℱ ⟶ ℱ'`,
+  then `α` is an iso if `G ⋙ ℱ ⟶ G ⋙ ℱ'` is iso.
+- `CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting`:
+  If `G : (C, J) ⥤ (D, K)` is faithful, cover-lifting, cover-preserving, and cover-dense,
+  then it will induce an equivalence of categories of sheaves valued in a complete category.
+
+## References
+
+* [Elephant]: *Sketches of an Elephant*, ℱ. T. Johnstone: C2.2.
+* https://ncatlab.org/nlab/show/dense+sub-site
+* https://ncatlab.org/nlab/show/comparison+lemma
+
+-/
+
+
+universe w v u
+
+namespace CategoryTheory
+
+variable {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*} [Category E] (G : C ⥤ D)
+variable (J : GrothendieckTopology C) (K : GrothendieckTopology D)
+variable {L : GrothendieckTopology E}
+
+/--
+For a functor `G : C ⥤ D`, and an morphism `f : G.obj U ⟶ G.obj V`,
+`Sieve.hasLift G f` is the sieve of `U`
+consisting of those arrows whose composition with `f` has a lift in `G`.
+-/
+def Sieve.hasLift {U V : C} (f : G.obj U ⟶ G.obj V) : Sieve U where
+  arrows Y i := ∃ l, G.map l = G.map i ≫ f
+  downward_closed := by
+    rintro Y₁ Y₂ i₁ ⟨l, hl⟩ i₂
+    exact ⟨i₂ ≫ l, by simp [hl]⟩
+
+@[simp]
+lemma Sieve.hasLift_map {U V : C} (f : U ⟶ V) : hasLift G (G.map f) = ⊤ := by
+  ext W g; simpa using ⟨g ≫ f, by simp⟩
+
+/--
+For two arrows `f₁ f₂ : U ⟶ V`, the arrows `i` such that `i ≫ f₁ = i ≫ f₂` forms a sieve.
+-/
+@[simps]
+def Sieve.equalizer {U V : C} (f₁ f₂ : U ⟶ V) : Sieve U where
+  arrows Y i := i ≫ f₁ = i ≫ f₂
+  downward_closed := by aesop
+
+@[simp]
+lemma Sieve.equalizer_self {U V : C} (f : U ⟶ V) : equalizer f f = ⊤ := by ext; simp
+
+open Presieve Opposite
+
+namespace Functor
+
+class IsLocallyFull : Prop where
+  functorPushforward_hasLift_mem : ∀ {U V} (f : G.obj U ⟶ G.obj V),
+    (Sieve.hasLift G f).functorPushforward G ∈ K _
+
+class IsLocallyFaithful : Prop where
+  functorPushforward_equalizer_mem : ∀ {U V : C} (f₁ f₂ : U ⟶ V), G.map f₁ = G.map f₂ →
+    (Sieve.equalizer f₁ f₂).functorPushforward G ∈ K _
+
+lemma functorPushforward_hasLift_mem [G.IsLocallyFull K] {U V} (f : G.obj U ⟶ G.obj V) :
+    (Sieve.hasLift G f).functorPushforward G ∈ K _ :=
+  Functor.IsLocallyFull.functorPushforward_hasLift_mem _
+
+lemma functorPushforward_equalizer_mem
+    [G.IsLocallyFaithful K] {U V} (f₁ f₂ : U ⟶ V) (e : G.map f₁ = G.map f₂) :
+      (Sieve.equalizer f₁ f₂).functorPushforward G ∈ K _ :=
+  Functor.IsLocallyFaithful.functorPushforward_equalizer_mem _ _ e
+
+variable {K}
+variable {A : Type*} [Category A] (G : C ⥤ D)
+
+theorem IsLocallyFull.ext [G.IsLocallyFull K]
+    (ℱ : SheafOfTypes K) {X Y : C} (i : G.obj X ⟶ G.obj Y)
+    {s t : ℱ.val.obj (op (G.obj X))}
+    (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X) (f : Z ⟶ Y), G.map f = G.map j ≫ i →
+      ℱ.1.map (G.map j).op s = ℱ.1.map (G.map j).op t) : s = t := by
+  apply (ℱ.cond _ (G.functorPushforward_hasLift_mem K i)).isSeparatedFor.ext
+  rintro Z _ ⟨W, iWX, iZW, ⟨iWY, e⟩, rfl⟩
+  simp [h iWX iWY e]
+
+theorem IsLocallyFaithful.ext [G.IsLocallyFaithful K] (ℱ : SheafOfTypes K)
+    {X Y : C} (i₁ i₂ : X ⟶ Y) (e : G.map i₁ = G.map i₂)
+    {s t : ℱ.val.obj (op (G.obj X))}
+    (h : ∀ ⦃Z : C⦄ (j : Z ⟶ X), j ≫ i₁ = j ≫ i₂ →
+      ℱ.1.map (G.map j).op s = ℱ.1.map (G.map j).op t) : s = t := by
+  apply (ℱ.cond _ (G.functorPushforward_equalizer_mem K i₁ i₂ e)).isSeparatedFor.ext
+  rintro Z _ ⟨W, iWX, iZW, hiWX, rfl⟩
+  simp [h iWX hiWX]
+
+instance (priority := 900) IsLocallyFull.of_full [G.Full] : G.IsLocallyFull K where
+  functorPushforward_hasLift_mem f := by
+    rw [← G.map_preimage f]
+    simp only [Sieve.hasLift_map, Sieve.functorPushforward_top, GrothendieckTopology.top_mem]
+
+instance (priority := 900) IsLocallyFaithful.of_faithful [G.Faithful] : G.IsLocallyFaithful K where
+  functorPushforward_equalizer_mem f₁ f₂ e := by obtain rfl := G.map_injective e; simp
+
+end CategoryTheory.Functor

From 01b6aeff63e2bb4b29c69bc0a3b2aafe28208550 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 22:37:35 +0800
Subject: [PATCH 3/9] fix

---
 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib.lean b/Mathlib.lean
index 2cffde07c87f8e..bf426181477309 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1768,6 +1768,7 @@ import Mathlib.CategoryTheory.Sites.LeftExact
 import Mathlib.CategoryTheory.Sites.Limits
 import Mathlib.CategoryTheory.Sites.Localization
 import Mathlib.CategoryTheory.Sites.LocallyBijective
+import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
 import Mathlib.CategoryTheory.Sites.LocallyInjective
 import Mathlib.CategoryTheory.Sites.LocallySurjective
 import Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

From 0edf2de7775890ea1af541424fb78e12f13aadf5 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 22:49:04 +0800
Subject: [PATCH 4/9] fix

---
 .../Sites/Coherent/SheafComparison.lean       | 44 +++++++------------
 .../CategoryTheory/Sites/DenseSubsite.lean    |  6 +--
 .../CategoryTheory/Sites/InducedTopology.lean |  3 --
 3 files changed, 19 insertions(+), 34 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean b/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
index bccb645c7cdd21..ce2536aa401c81 100644
--- a/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
+++ b/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
@@ -55,7 +55,7 @@ instance : F.IsCoverDense (coherentTopology _) := by
 theorem exists_effectiveEpiFamily_iff_mem_induced (X : C) (S : Sieve X) :
     (∃ (α : Type) (_ : Finite α) (Y : α → C) (π : (a : α) → (Y a ⟶ X)),
       EffectiveEpiFamily Y π ∧ (∀ a : α, (S.arrows) (π a)) ) ↔
-    (S ∈ F.inducedTopologyOfIsCoverDense (coherentTopology _) X) := by
+    (S ∈ F.inducedTopology (coherentTopology _) X) := by
   refine ⟨fun ⟨α, _, Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
   · apply (mem_sieves_iff_hasEffectiveEpiFamily (Sieve.functorPushforward _ S)).mpr
     refine ⟨α, inferInstance, fun i => F.obj (Y i),
@@ -77,25 +77,19 @@ theorem exists_effectiveEpiFamily_iff_mem_induced (X : C) (S : Sieve X) :
 
 lemma eq_induced : haveI := F.reflects_precoherent
     coherentTopology C =
-      F.inducedTopologyOfIsCoverDense (coherentTopology _) := by
+      F.inducedTopology (coherentTopology _) := by
   ext X S
   have := F.reflects_precoherent
   rw [← exists_effectiveEpiFamily_iff_mem_induced F X]
   rw [← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]
 
-lemma coverPreserving : haveI := F.reflects_precoherent
-    CoverPreserving (coherentTopology _) (coherentTopology _) F := by
-  rw [eq_induced F]
-  apply LocallyCoverDense.inducedTopology_coverPreserving
-
-instance coverLifting : haveI := F.reflects_precoherent
-    F.IsCocontinuous (coherentTopology _) (coherentTopology _) := by
-  rw [eq_induced F]
-  apply LocallyCoverDense.inducedTopology_isCocontinuous
+instance : haveI := F.reflects_precoherent;
+    F.IsDenseSubsite (coherentTopology C) (coherentTopology D) where
+  functorPushforward_mem_iff := by simp_rw [eq_induced F]; rfl
 
-instance isContinuous : haveI := F.reflects_precoherent
-    F.IsContinuous (coherentTopology _) (coherentTopology _) :=
-  Functor.IsCoverDense.isContinuous _ _ _ (coverPreserving F)
+lemma coverPreserving : haveI := F.reflects_precoherent
+    CoverPreserving (coherentTopology _) (coherentTopology _) F :=
+  IsDenseSubsite.coverPreserving _ _ _
 
 section SheafEquiv
 
@@ -161,7 +155,7 @@ instance : F.IsCoverDense (regularTopology _) := by
 theorem exists_effectiveEpi_iff_mem_induced (X : C) (S : Sieve X) :
     (∃ (Y : C) (π : Y ⟶ X),
       EffectiveEpi π ∧ S.arrows π) ↔
-    (S ∈ F.inducedTopologyOfIsCoverDense (regularTopology _) X) := by
+    (S ∈ F.inducedTopology (regularTopology _) X) := by
   refine ⟨fun ⟨Y, π, ⟨H₁, H₂⟩⟩ ↦ ?_, fun hS ↦ ?_⟩
   · apply (mem_sieves_iff_hasEffectiveEpi (Sieve.functorPushforward _ S)).mpr
     refine ⟨F.obj Y, F.map π, ⟨?_, Sieve.image_mem_functorPushforward F S H₂⟩⟩
@@ -179,25 +173,19 @@ theorem exists_effectiveEpi_iff_mem_induced (X : C) (S : Sieve X) :
 
 lemma eq_induced : haveI := F.reflects_preregular
     regularTopology C =
-      F.inducedTopologyOfIsCoverDense (regularTopology _) := by
+      F.inducedTopology (regularTopology _) := by
   ext X S
   have := F.reflects_preregular
   rw [← exists_effectiveEpi_iff_mem_induced F X]
   rw [← mem_sieves_iff_hasEffectiveEpi S]
 
+instance : haveI := F.reflects_preregular;
+    F.IsDenseSubsite (regularTopology C) (regularTopology D) where
+  functorPushforward_mem_iff := by simp_rw [eq_induced F]; rfl
+
 lemma coverPreserving : haveI := F.reflects_preregular
-    CoverPreserving (regularTopology _) (regularTopology _) F := by
-  rw [eq_induced F]
-  apply LocallyCoverDense.inducedTopology_coverPreserving
-
-instance coverLifting : haveI := F.reflects_preregular
-    F.IsCocontinuous (regularTopology _) (regularTopology _) := by
-  rw [eq_induced F]
-  apply LocallyCoverDense.inducedTopology_isCocontinuous
-
-instance isContinuous : haveI := F.reflects_preregular
-    F.IsContinuous (regularTopology _) (regularTopology _) :=
-  Functor.IsCoverDense.isContinuous _ _ _ (coverPreserving F)
+    CoverPreserving (regularTopology _) (regularTopology _) F :=
+  IsDenseSubsite.coverPreserving _ _ _
 
 section SheafEquiv
 
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index ec63a38f860257..43e672507df5e6 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -501,9 +501,9 @@ variable (J : GrothendieckTopology C) (K : GrothendieckTopology D) (G : C ⥤ D)
 if `G` is cover-dense, locally fully-faithful,
 and `S` is a cover of `C` if and only if the image of `S` in `D` is a cover. -/
 class IsDenseSubsite : Prop where
-  isCoverDense' : G.IsCoverDense K
-  isLocallyFull' : G.IsLocallyFull K
-  isLocallyFaithful' : G.IsLocallyFaithful K
+  isCoverDense' : G.IsCoverDense K := by infer_instance
+  isLocallyFull' : G.IsLocallyFull K := by infer_instance
+  isLocallyFaithful' : G.IsLocallyFaithful K := by infer_instance
   functorPushforward_mem_iff : ∀ {X : C} {S : Sieve X}, S.functorPushforward G ∈ K _ ↔ S ∈ J _
 
 namespace IsDenseSubsite
diff --git a/Mathlib/CategoryTheory/Sites/InducedTopology.lean b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
index e84f80c62209ef..29d12c52be323c 100644
--- a/Mathlib/CategoryTheory/Sites/InducedTopology.lean
+++ b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
@@ -110,9 +110,6 @@ instance (priority := 900) locallyCoverDense_of_isCoverDense [G.IsCoverDense K]
     IsCoverDense.functorPullback_pushforward_covering _
 
 instance (priority := 900) [G.IsCoverDense K] : G.IsDenseSubsite (G.inducedTopology K) K where
-  isCoverDense' := inferInstance
-  isLocallyFull' := inferInstance
-  isLocallyFaithful' := inferInstance
   functorPushforward_mem_iff := Iff.rfl
 
 @[deprecated (since := "2024-07-23")]

From 11a43fc022ec81dd568bc8c11a54dec10c78a5f5 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 23:36:41 +0800
Subject: [PATCH 5/9] fix

---
 .../Sites/Coherent/SheafComparison.lean       |  6 +-
 .../CategoryTheory/Sites/DenseSubsite.lean    | 96 +++++++++++--------
 Mathlib/CategoryTheory/Sites/Discrete.lean    | 14 +--
 .../CategoryTheory/Sites/InducedTopology.lean |  2 +-
 .../Sites/LocallyFullyFaithful.lean           | 42 ++++----
 5 files changed, 87 insertions(+), 73 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean b/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
index ce2536aa401c81..330fcdfb5f49f4 100644
--- a/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
+++ b/Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
@@ -108,7 +108,7 @@ noncomputable
 def equivalence (A : Type u₃) [Category.{v₃} A] [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
     haveI := F.reflects_precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A :=
-  Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
+  Functor.IsDenseSubsite.sheafEquiv F _ _ _
 
 end SheafEquiv
 
@@ -132,7 +132,7 @@ def equivalence' (A : Type u₃) [Category.{v₃} A]
     [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
     haveI := F.reflects_precoherent
     Sheaf (coherentTopology C) A ≌ Sheaf (coherentTopology D) A :=
-  Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
+  Functor.IsDenseSubsite.sheafEquiv F _ _ _
 
 end RegularExtensive
 
@@ -204,7 +204,7 @@ noncomputable
 def equivalence (A : Type u₃) [Category.{v₃} A] [∀ X, HasLimitsOfShape (StructuredArrow X F.op) A] :
     haveI := F.reflects_preregular
     Sheaf (regularTopology C) A ≌ Sheaf (regularTopology D) A :=
-  Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting F _ _ _
+  Functor.IsDenseSubsite.sheafEquiv F _ _ _
 
 end SheafEquiv
 
diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index 43e672507df5e6..f76d163581ba6a 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -15,25 +15,23 @@ import Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
 We define `IsCoverDense` functors into sites as functors such that there exists a covering sieve
 that factors through images of the functor for each object in `D`.
 
-We will primarily consider cover-dense functors that are also full, since this notion is in general
-not well-behaved otherwise. Note that https://ncatlab.org/nlab/show/dense+sub-site indeed has a
-weaker notion of cover-dense that loosens this requirement, but it would not have all the properties
-we would need, and some sheafification would be needed for here and there.
-
 ## Main results
 
-- `CategoryTheory.Functor.IsCoverDense.Types.presheafHom`: If `G : C ⥤ (D, K)` is full
+- `CategoryTheory.Functor.IsCoverDense.Types.presheafHom`: If `G : C ⥤ (D, K)` is locally-full
   and cover-dense, then given any presheaf `ℱ` and sheaf `ℱ'` on `D`,
   and a morphism `α : G ⋙ ℱ ⟶ G ⋙ ℱ'`, we may glue them together to obtain
   a morphism of presheaves `ℱ ⟶ ℱ'`.
 - `CategoryTheory.Functor.IsCoverDense.sheafIso`: If `ℱ` above is a sheaf and `α` is an iso,
   then the result is also an iso.
-- `CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso`: If `G : C ⥤ (D, K)` is full
+- `CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso`: If `G : C ⥤ (D, K)` is locally-full
   and cover-dense, then given any sheaves `ℱ, ℱ'` on `D`, and a morphism `α : ℱ ⟶ ℱ'`,
   then `α` is an iso if `G ⋙ ℱ ⟶ G ⋙ ℱ'` is iso.
-- `CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting`:
-  If `G : (C, J) ⥤ (D, K)` is fully-faithful, cover-lifting, cover-preserving, and cover-dense,
-  then it will induce an equivalence of categories of sheaves valued in a complete category.
+- `CategoryTheory.Functor.IsDenseSubsite`:
+  The functor `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)` if `G` is cover-dense,
+  locally fully-faithful, and `S` is a cover of `C` iff the image of `S` in `D` is a cover.
+- `CategoryTheory.Functor.IsDenseSubsite.sheafEquiv`:
+  If `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)`,
+  it induces an equivalence of category of sheaves valued in a category with suitable limits.
 
 ## References
 
@@ -194,9 +192,6 @@ noncomputable def pushforwardFamily {X} (x : ℱ.obj (op X)) :
 /-- (Implementation). The `pushforwardFamily` defined is compatible. -/
 theorem pushforwardFamily_compatible {X} (x : ℱ.obj (op X)) :
     (pushforwardFamily α x).Compatible := by
-  have {X Y} (i : X ⟶ Y) (x) :
-      ℱ'.1.map (G.map i).op (α.app _ x) = α.app _ (ℱ.map (G.map i).op x) := by
-    exact congr_fun (α.naturality i.op).symm x
   suffices ∀ {Z W₁ W₂} (iWX₁ : G.obj W₁ ⟶ X) (iWX₂ : G.obj W₂ ⟶ X) (iZW₁ : Z ⟶ G.obj W₁)
       (iZW₂ : Z ⟶ G.obj W₂), iZW₁ ≫ iWX₁ = iZW₂ ≫ iWX₂ →
       ℱ'.1.map iZW₁.op (α.app _ (ℱ.map iWX₁.op x)) = ℱ'.1.map iZW₂.op (α.app _ (ℱ.map iWX₂.op x)) by
@@ -257,8 +252,10 @@ noncomputable def appIso {ℱ ℱ' : SheafOfTypes.{v} K} (i : G.op ⋙ ℱ.val 
     intro Y f
     simp
 
-/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of types, where `G` is
-full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural transformation between sheaves.
+/--
+Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of types,
+where `G` is locally-full and cover-dense, and `ℱ'` is a sheaf,
+we may obtain a natural transformation between sheaves.
 -/
 @[simps]
 noncomputable def presheafHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ ⟶ ℱ'.val where
@@ -270,16 +267,20 @@ noncomputable def presheafHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ 
     simp only [appHom_restrict, types_comp_apply, ← FunctorToTypes.map_comp_apply]
     -- Porting note: Lean 3 proof continued with a rewrite but we're done here
 
-/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
-and cover-dense, and `ℱ, ℱ'` are sheaves, we may obtain a natural isomorphism between presheaves.
+/--
+Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types,
+where `G` is locally-full and cover-dense, and `ℱ, ℱ'` are sheaves,
+we may obtain a natural isomorphism between presheaves.
 -/
 @[simps!]
 noncomputable def presheafIso {ℱ ℱ' : SheafOfTypes.{v} K} (i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val) :
     ℱ.val ≅ ℱ'.val :=
   NatIso.ofComponents (fun X => appIso i (unop X)) @(presheafHom i.hom).naturality
 
-/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types, where `G` is full
-and cover-dense, and `ℱ, ℱ'` are sheaves, we may obtain a natural isomorphism between sheaves.
+/--
+Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of types,
+where `G` is locally-full and cover-dense, and `ℱ, ℱ'` are sheaves,
+we may obtain a natural isomorphism between sheaves.
 -/
 @[simps]
 noncomputable def sheafIso {ℱ ℱ' : SheafOfTypes.{v} K} (i : G.op ⋙ ℱ.val ≅ G.op ⋙ ℱ'.val) :
@@ -338,17 +339,19 @@ noncomputable def sheafYonedaHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
     ext X x
     exact congr_fun (((sheafCoyonedaHom α).app X).naturality i) x
 
-/-- Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of arbitrary category,
-where `G` is full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural transformation
-between presheaves.
+/--
+Given a natural transformation `G ⋙ ℱ ⟶ G ⋙ ℱ'` between presheaves of arbitrary category,
+where `G` is locally-full and cover-dense, and `ℱ'` is a sheaf, we may obtain a natural
+transformation between presheaves.
 -/
 noncomputable def sheafHom (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) : ℱ ⟶ ℱ'.val :=
   let α' := sheafYonedaHom α
   { app := fun X => yoneda.preimage (α'.app X)
     naturality := fun X Y f => yoneda.map_injective (by simpa using α'.naturality f) }
 
-/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
-where `G` is full and cover-dense, and `ℱ', ℱ` are sheaves,
+/--
+Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
+where `G` is locally-full and cover-dense, and `ℱ', ℱ` are sheaves,
 we may obtain a natural isomorphism between presheaves.
 -/
 @[simps!]
@@ -370,8 +373,9 @@ noncomputable def presheafIso {ℱ ℱ' : Sheaf K A} (i : G.op ⋙ ℱ.val ≅ G
   haveI : IsIso (sheafHom i.hom) := by apply NatIso.isIso_of_isIso_app
   apply asIso (sheafHom i.hom)
 
-/-- Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
-where `G` is full and cover-dense, and `ℱ', ℱ` are sheaves,
+/--
+Given a natural isomorphism `G ⋙ ℱ ≅ G ⋙ ℱ'` between presheaves of arbitrary category,
+where `G` is locally-full and cover-dense, and `ℱ', ℱ` are sheaves,
 we may obtain a natural isomorphism between presheaves.
 -/
 @[simps]
@@ -385,8 +389,7 @@ noncomputable def sheafIso {ℱ ℱ' : Sheaf K A} (i : G.op ⋙ ℱ.val ≅ G.op
     ext1
     apply (presheafIso i).inv_hom_id
 
-/-- The constructed `sheafHom α` is equal to `α` when restricted onto `C`.
--/
+/-- The constructed `sheafHom α` is equal to `α` when restricted onto `C`. -/
 theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
     whiskerLeft G.op (sheafHom α) = α := by
   ext X
@@ -412,7 +415,8 @@ theorem sheafHom_restrict_eq (α : G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) :
 
 variable (G)
 
-/-- If the pullback map is obtained via whiskering,
+/--
+If the pullback map is obtained via whiskering,
 then the result `sheaf_hom (whisker_left G.op α)` is equal to `α`.
 -/
 theorem sheafHom_eq (α : ℱ ⟶ ℱ'.val) : sheafHom (whiskerLeft G.op α) = α := by
@@ -434,7 +438,8 @@ theorem sheafHom_eq (α : ℱ ⟶ ℱ'.val) : sheafHom (whiskerLeft G.op α) = 
 
 variable {G}
 
-/-- A full and cover-dense functor `G` induces an equivalence between morphisms into a sheaf and
+/--
+A locally-full and cover-dense functor `G` induces an equivalence between morphisms into a sheaf and
 morphisms over the restrictions via `G`.
 -/
 noncomputable def restrictHomEquivHom : (G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) ≃ (ℱ ⟶ ℱ'.val) where
@@ -443,8 +448,8 @@ noncomputable def restrictHomEquivHom : (G.op ⋙ ℱ ⟶ G.op ⋙ ℱ'.val) ≃
   left_inv := sheafHom_restrict_eq
   right_inv := sheafHom_eq _
 
-/-- Given a full and cover-dense functor `G` and a natural transformation of sheaves `α : ℱ ⟶ ℱ'`,
-if the pullback of `α` along `G` is iso, then `α` is also iso.
+/-- Given a locally-full and cover-dense functor `G` and a natural transformation of sheaves
+`α : ℱ ⟶ ℱ'`, if the pullback of `α` along `G` is iso, then `α` is also iso.
 -/
 theorem iso_of_restrict_iso {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIso (whiskerLeft G.op α.val)) :
     IsIso α := by
@@ -454,7 +459,7 @@ theorem iso_of_restrict_iso {ℱ ℱ' : Sheaf K A} (α : ℱ ⟶ ℱ') (i : IsIs
 
 variable (G K)
 
-/-- A fully faithful cover-dense functor preserves compatible families. -/
+/-- A locally-fully-faithful and cover-dense functor preserves compatible families. -/
 lemma compatiblePreserving [G.IsLocallyFaithful K] : CompatiblePreserving K G := by
   constructor
   intro ℱ Z T x hx Y₁ Y₂ X f₁ f₂ g₁ g₂ hg₁ hg₂ eq
@@ -558,7 +563,7 @@ end Functor
 
 end CategoryTheory
 
-namespace CategoryTheory.Functor.IsCoverDense
+namespace CategoryTheory.Functor.IsDenseSubsite
 
 open CategoryTheory Opposite
 
@@ -642,21 +647,30 @@ instance (Y : Sheaf J A) : IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.a
 
 variable (A)
 
-/-- Given a functor between small sites that is cover-dense, cover-preserving, and cover-lifting,
-it induces an equivalence of category of sheaves valued in a complete category.
+/--
+If `G : C ⥤ D` exhibits `(C, J)` as a dense subsite of `(D, K)`,
+it induces an equivalence of category of sheaves valued in a category with suitable limits.
 -/
 @[simps! functor inverse]
-noncomputable def sheafEquivOfCoverPreservingCoverLifting : Sheaf J A ≌ Sheaf K A :=
+noncomputable def sheafEquiv : Sheaf J A ≌ Sheaf K A :=
   (G.sheafAdjunctionCocontinuous A J K).toEquivalence.symm
 
 variable [HasWeakSheafify J A] [HasWeakSheafify K A]
 
 /-- The natural isomorphism exhibiting the compatibility of
-`sheafEquivOfCoverPreservingCoverLifting` with sheafification. -/
+`IsDenseSubsite.sheafEquiv` with sheafification. -/
 noncomputable
-abbrev sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility :
+abbrev sheafEquivSheafificationCompatibility :
     (whiskeringLeft _ _ A).obj G.op ⋙ presheafToSheaf _ _ ≅
-      presheafToSheaf _ _ ⋙ (sheafEquivOfCoverPreservingCoverLifting G J K A).inverse := by
+      presheafToSheaf _ _ ⋙ (sheafEquiv G J K A).inverse := by
   apply Functor.pushforwardContinuousSheafificationCompatibility
 
-end CategoryTheory.Functor.IsCoverDense
+end IsDenseSubsite
+
+@[deprecated (since := "2024-07-23")]
+alias IsCoverDense.sheafEquivOfCoverPreservingCoverLifting := IsDenseSubsite.sheafEquiv
+@[deprecated (since := "2024-07-23")]
+alias IsCoverDense.sheafEquivOfCoverPreservingCoverLiftingSheafificationCompatibility :=
+  IsDenseSubsite.sheafEquivSheafificationCompatibility
+
+end CategoryTheory.Functor
diff --git a/Mathlib/CategoryTheory/Sites/Discrete.lean b/Mathlib/CategoryTheory/Sites/Discrete.lean
index 01def9d01d1c3b..2b59807d4ad46d 100644
--- a/Mathlib/CategoryTheory/Sites/Discrete.lean
+++ b/Mathlib/CategoryTheory/Sites/Discrete.lean
@@ -82,11 +82,11 @@ variable (G : C ⥤ D)
 
 variable [(constantSheaf J A).Faithful] [(constantSheaf J A).Full]
 
-open Functor.IsCoverDense
+open Functor.IsDenseSubsite
 
 noncomputable example :
     let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
     e.inverse ⋙ (sheafSections J A).obj (op t) ≅ (sheafSections K A).obj (op (G.obj t)) :=
   Iso.refl _
 
@@ -99,10 +99,10 @@ property of a sheaf of being a discrete object is invariant under equivalence of
 -/
 noncomputable def equivCommuteConstant :
     let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
     constantSheaf J A ⋙ e.functor ≅ constantSheaf K A :=
   let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
   (Adjunction.leftAdjointUniq ((constantSheafAdj J A ht).comp e.toAdjunction)
     (constantSheafAdj K A ht'))
 
@@ -115,10 +115,10 @@ property of a sheaf of being a discrete object is invariant under equivalence of
 -/
 noncomputable def equivCommuteConstant' :
     let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
     constantSheaf J A ≅ constantSheaf K A ⋙ e.inverse :=
   let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
   isoWhiskerLeft (constantSheaf J A) e.unitIso ≪≫
     isoWhiskerRight (equivCommuteConstant J A ht K G ht') e.inverse
 
@@ -128,7 +128,7 @@ categories.
 -/
 lemma isDiscrete_iff_of_equivalence (F : Sheaf K A) :
     let e : Sheaf J A ≌ Sheaf K A :=
-      sheafEquivOfCoverPreservingCoverLifting G J K A
+      sheafEquiv G J K A
     haveI : (constantSheaf K A).Faithful :=
       Functor.Faithful.of_iso (equivCommuteConstant J A ht K G ht')
     haveI : (constantSheaf K A).Full :=
diff --git a/Mathlib/CategoryTheory/Sites/InducedTopology.lean b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
index 29d12c52be323c..0e3ea9401d2421 100644
--- a/Mathlib/CategoryTheory/Sites/InducedTopology.lean
+++ b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
@@ -135,7 +135,7 @@ is complete.
 noncomputable def sheafInducedTopologyEquivOfIsCoverDense
     [G.IsCoverDense K] [∀ (X : Dᵒᵖ), HasLimitsOfShape (StructuredArrow X G.op) A] :
     Sheaf (G.inducedTopology K) A ≌ Sheaf K A :=
-  Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting G
+  Functor.IsDenseSubsite.sheafEquiv G
     (G.inducedTopology K) K A
 
 end Functor
diff --git a/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean b/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
index fc04a809840ad5..d6967c6eae447e 100644
--- a/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
+++ b/Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean
@@ -1,40 +1,30 @@
 /-
-Copyright (c) 2021 Andrew Yang. All rights reserved.
+Copyright (c) 2024 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Sites.SheafOfTypes
 
 /-!
-# Dense subsites
-
-We define `IsCoverDense` functors into sites as functors such that there exists a covering sieve
-that factors through images of the functor for each object in `D`.
+# Locally fully faithful functors into sites
 
 ## Main results
 
-- `CategoryTheory.Functor.IsCoverDense.Types.presheafHom`: If `G : C ⥤ (D, K)` is
-  and cover-dense, then given any presheaf `ℱ` and sheaf `ℱ'` on `D`,
-  and a morphism `α : G ⋙ ℱ ⟶ G ⋙ ℱ'`, we may glue them together to obtain
-  a morphism of presheaves `ℱ ⟶ ℱ'`.
-- `CategoryTheory.Functor.IsCoverDense.sheafIso`: If `ℱ` above is a sheaf and `α` is an iso,
-  then the result is also an iso.
-- `CategoryTheory.Functor.IsCoverDense.iso_of_restrict_iso`: If `G : C ⥤ (D, K)` is
-  and cover-dense, then given any sheaves `ℱ, ℱ'` on `D`, and a morphism `α : ℱ ⟶ ℱ'`,
-  then `α` is an iso if `G ⋙ ℱ ⟶ G ⋙ ℱ'` is iso.
-- `CategoryTheory.Functor.IsCoverDense.sheafEquivOfCoverPreservingCoverLifting`:
-  If `G : (C, J) ⥤ (D, K)` is faithful, cover-lifting, cover-preserving, and cover-dense,
-  then it will induce an equivalence of categories of sheaves valued in a complete category.
+- `CategoryTheory.Functor.IsLocallyFull`:
+  A functor `G : C ⥤ D` is locally full wrt a topology on `D` if for every `f : G.obj U ⟶ G.obj V`,
+  the set of `G.map fᵢ : G.obj Wᵢ ⟶ G.obj U` such that `G.map fᵢ ≫ f` is
+  in the image of `G` is a coverage of the topology on `D`.
+- `CategoryTheory.Functor.IsLocallyFaithful`:
+  A functor `G : C ⥤ D` is locally faithful wrt a topology on `D` if for every `f₁ f₂ : U ⟶ V` whose
+  image in `D` are equal, the set of `G.map gᵢ : G.obj Wᵢ ⟶ G.obj U` such that `gᵢ ≫ f₁ = gᵢ ≫ f₂`
+  is a coverage of the topology on `D`.
 
 ## References
 
-* [Elephant]: *Sketches of an Elephant*, ℱ. T. Johnstone: C2.2.
-* https://ncatlab.org/nlab/show/dense+sub-site
-* https://ncatlab.org/nlab/show/comparison+lemma
+* https://arxiv.org/pdf/1906.08737
 
 -/
 
-
 universe w v u
 
 namespace CategoryTheory
@@ -73,10 +63,20 @@ open Presieve Opposite
 
 namespace Functor
 
+/--
+A functor `G : C ⥤ D` is locally full wrt a topology on `D` if for every `f : G.obj U ⟶ G.obj V`,
+the set of `G.map fᵢ : G.obj Wᵢ ⟶ G.obj U` such that `G.map fᵢ ≫ f` is
+in the image of `G` is a coverage of the topology on `D`.
+-/
 class IsLocallyFull : Prop where
   functorPushforward_hasLift_mem : ∀ {U V} (f : G.obj U ⟶ G.obj V),
     (Sieve.hasLift G f).functorPushforward G ∈ K _
 
+/--
+A functor `G : C ⥤ D` is locally faithful wrt a topology on `D` if for every `f₁ f₂ : U ⟶ V` whose
+image in `D` are equal, the set of `G.map gᵢ : G.obj Wᵢ ⟶ G.obj U` such that `gᵢ ≫ f₁ = gᵢ ≫ f₂`
+is a coverage of the topology on `D`.
+-/
 class IsLocallyFaithful : Prop where
   functorPushforward_equalizer_mem : ∀ {U V : C} (f₁ f₂ : U ⟶ V), G.map f₁ = G.map f₂ →
     (Sieve.equalizer f₁ f₂).functorPushforward G ∈ K _

From 3a1950830b34b09583cd0db2557d0b5e528a7055 Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Tue, 23 Jul 2024 23:42:50 +0800
Subject: [PATCH 6/9] fix

---
 Mathlib/CategoryTheory/Sites/Equivalence.lean | 39 +------------------
 .../CategoryTheory/Sites/Grothendieck.lean    |  8 ++++
 Mathlib/CategoryTheory/Sites/Sieves.lean      | 32 ++++++++++++++-
 3 files changed, 40 insertions(+), 39 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/Equivalence.lean b/Mathlib/CategoryTheory/Sites/Equivalence.lean
index f5842af8d091ca..07fb08b597fdfa 100644
--- a/Mathlib/CategoryTheory/Sites/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Sites/Equivalence.lean
@@ -46,43 +46,6 @@ variable {C : Type u₁} [Category.{v₁} C] (J : GrothendieckTopology C)
 variable {D : Type u₂} [Category.{v₂} D] (K : GrothendieckTopology D) (e : C ≌ D) (G : D ⥤ C)
 variable (A : Type u₃) [Category.{v₃} A]
 
-variable {J} in
-lemma pullback_mem_iff_of_isIso {X Y : C} {i : X ⟶ Y} [IsIso i] {S : Sieve Y} :
-    S.pullback i ∈ J _ ↔ S ∈ J _ := by
-  refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
-  convert J.pullback_stable (inv i) H
-  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
-
-@[simp]
-lemma Sieve.comp_mem_iff {X Y Z : C} (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) :
-    S (i ≫ f) ↔ S f := by
-  refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
-  convert S.downward_closed H (inv i)
-  simp
-
-lemma Sieve.functorPushforward_functor {X} (S : Sieve X) :
-    S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse := by
-  ext Y iYX
-  constructor
-  · rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩
-    simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)
-  · intro H
-    exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩
-
-@[simp]
-lemma Sieve.mem_functorPushforward_functor {X Y} {S : Sieve X} {f : Y ⟶ e.functor.obj X} :
-    S.functorPushforward e.functor f ↔ S (e.inverse.map f ≫ e.unitInv.app X) :=
-  congr($(S.functorPushforward_functor e).arrows f)
-
-lemma Sieve.functorPushforward_inverse {X} (S : Sieve X) :
-    S.functorPushforward e.inverse = (S.pullback (e.counit.app X)).functorPullback e.functor :=
-  Sieve.functorPushforward_functor e.symm S
-
-@[simp]
-lemma Sieve.mem_functorPushforward_inverse {X Y} {S : Sieve X} {f : Y ⟶ e.inverse.obj X} :
-    S.functorPushforward e.inverse f ↔ S (e.functor.map f ≫ e.counit.app X) :=
-  congr($(S.functorPushforward_inverse e).arrows f)
-
 namespace Equivalence
 
 instance (priority := 900) [G.IsEquivalence] : IsCoverDense G J where
@@ -103,7 +66,7 @@ instance : e.functor.IsDenseSubsite J (e.inverse.inducedTopology J) := by
   have : J = e.functor.inducedTopology (e.inverse.inducedTopology J) := by
     ext X S
     show _ ↔ _ ∈ J.sieves _
-    erw [← pullback_mem_iff_of_isIso (i := e.unit.app X)]
+    erw [← GrothendieckTopology.pullback_mem_iff_of_isIso (i := e.unit.app X)]
     congr!; ext Y f; simp
   nth_rw 1 [this]
   infer_instance
diff --git a/Mathlib/CategoryTheory/Sites/Grothendieck.lean b/Mathlib/CategoryTheory/Sites/Grothendieck.lean
index c0a9e3738620d1..f7773b4fc0fb2a 100644
--- a/Mathlib/CategoryTheory/Sites/Grothendieck.lean
+++ b/Mathlib/CategoryTheory/Sites/Grothendieck.lean
@@ -121,6 +121,14 @@ theorem top_mem (X : C) : ⊤ ∈ J X :=
 theorem pullback_stable (f : Y ⟶ X) (hS : S ∈ J X) : S.pullback f ∈ J Y :=
   J.pullback_stable' f hS
 
+variable {J} in
+@[simp]
+lemma pullback_mem_iff_of_isIso {i : X ⟶ Y} [IsIso i] {S : Sieve Y} :
+    S.pullback i ∈ J _ ↔ S ∈ J _ := by
+  refine ⟨fun H ↦ ?_, J.pullback_stable i⟩
+  convert J.pullback_stable (inv i) H
+  rw [← Sieve.pullback_comp, IsIso.inv_hom_id, Sieve.pullback_id]
+
 theorem transitive (hS : S ∈ J X) (R : Sieve X) (h : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄, S f → R.pullback f ∈ J Y) :
     R ∈ J X :=
   J.transitive' hS R h
diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
index 57796493d5443f..44dfbb4a1026f2 100644
--- a/Mathlib/CategoryTheory/Sites/Sieves.lean
+++ b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -416,6 +416,13 @@ theorem generate_of_singleton_isSplitEpi (f : Y ⟶ X) [IsSplitEpi f] :
 theorem generate_top : generate (⊤ : Presieve X) = ⊤ :=
   generate_of_contains_isSplitEpi (𝟙 _) ⟨⟩
 
+@[simp]
+lemma comp_mem_iff (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) :
+    S (i ≫ f) ↔ S f := by
+  refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩
+  convert S.downward_closed H (inv i)
+  simp
+
 /-- The sieve of `X` generated by family of morphisms `Y i ⟶ X`. -/
 abbrev ofArrows {I : Type*} {X : C} (Y : I → C) (f : ∀ i, Y i ⟶ X) :
     Sieve X :=
@@ -707,7 +714,7 @@ def essSurjFullFunctorGaloisInsertion [F.EssSurj] [F.Full] (X : C) :
   apply (functor_galoisConnection F X).toGaloisInsertion
   intro S Y f hf
   refine ⟨_, F.preimage ((F.objObjPreimageIso Y).hom ≫ f), (F.objObjPreimageIso Y).inv, ?_⟩
-  simpa using S.downward_closed hf _
+  simpa using hf
 
 /-- When `F` is fully faithful, the galois connection is a galois coinsertion. -/
 def fullyFaithfulFunctorGaloisCoinsertion [F.Full] [F.Faithful] (X : C) :
@@ -719,6 +726,29 @@ def fullyFaithfulFunctorGaloisCoinsertion [F.Full] [F.Faithful] (X : C) :
   rw [F.map_injective h₂]
   exact S.downward_closed h₁ _
 
+lemma functorPushforward_functor (S : Sieve X) (e : C ≌ D) :
+    S.functorPushforward e.functor = (S.pullback (e.unitInv.app X)).functorPullback e.inverse := by
+  ext Y iYX
+  constructor
+  · rintro ⟨Z, iZX, iYZ, hiZX, rfl⟩
+    simpa using S.downward_closed hiZX (e.inverse.map iYZ ≫ e.unitInv.app Z)
+  · intro H
+    exact ⟨_, e.inverse.map iYX ≫ e.unitInv.app X, e.counitInv.app Y, by simpa using H, by simp⟩
+
+@[simp]
+lemma mem_functorPushforward_functor {Y : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.functor.obj X} :
+    S.functorPushforward e.functor f ↔ S (e.inverse.map f ≫ e.unitInv.app X) :=
+  congr($(S.functorPushforward_functor e).arrows f)
+
+lemma functorPushforward_inverse {X : D} (S : Sieve X) (e : C ≌ D) :
+    S.functorPushforward e.inverse = (S.pullback (e.counit.app X)).functorPullback e.functor :=
+  Sieve.functorPushforward_functor S e.symm
+
+@[simp]
+lemma mem_functorPushforward_inverse {X : D} {S : Sieve X} {e : C ≌ D} {f : Y ⟶ e.inverse.obj X} :
+    S.functorPushforward e.inverse f ↔ S (e.functor.map f ≫ e.counit.app X) :=
+  congr($(S.functorPushforward_inverse e).arrows f)
+
 end Functor
 
 /-- A sieve induces a presheaf. -/

From d66e92b4bb7afd42abb8d483197a068e5aceeb1a Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Wed, 24 Jul 2024 18:58:01 +0800
Subject: [PATCH 7/9] fix

---
 Mathlib/CategoryTheory/Sites/DenseSubsite.lean    | 4 ++--
 Mathlib/CategoryTheory/Sites/InducedTopology.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index f76d163581ba6a..9b7a61284b13e1 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -129,7 +129,7 @@ theorem functorPullback_pushforward_covering [G.IsLocallyFull K] {X : C}
   apply K.transitive (G.is_cover_of_isCoverDense _ _) _
   rintro W _ ⟨Z, iWZ, iZY, rfl⟩
   rw [Sieve.pullback_comp]; apply K.pullback_stable; clear W iWZ
-  apply K.superset_covering ?_ (G.functorPushforward_hasLift_mem _ (iZY ≫ iYX))
+  apply K.superset_covering ?_ (G.functorPushforward_imageSieve_mem _ (iZY ≫ iYX))
   rintro W _ ⟨V, iVZ, iWV, ⟨iVX, e⟩, rfl⟩
   exact ⟨_, iVX, iWV, by simpa [e] using T.1.downward_closed hiYX (G.map iVZ ≫ iZY), by simp [e]⟩
 
@@ -550,7 +550,7 @@ instance faithful_sheafPushforwardContinuous [G.IsDenseSubsite J K] :
 lemma hasLift_mem [G.IsDenseSubsite J K] {U V} (f : G.obj U ⟶ G.obj V) :
     Sieve.hasLift G f ∈ J _ :=
   letI := IsDenseSubsite.isLocallyFull J K G
-  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_hasLift_mem K f)
+  IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_imageSieve_mem K f)
 
 lemma equalizer_mem [G.IsDenseSubsite J K] {U V} (f₁ f₂ : U ⟶ V) (e : G.map f₁ = G.map f₂) :
     Sieve.equalizer f₁ f₂ ∈ J _ :=
diff --git a/Mathlib/CategoryTheory/Sites/InducedTopology.lean b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
index 0e3ea9401d2421..48981facbaeb7c 100644
--- a/Mathlib/CategoryTheory/Sites/InducedTopology.lean
+++ b/Mathlib/CategoryTheory/Sites/InducedTopology.lean
@@ -76,7 +76,7 @@ def inducedTopology : GrothendieckTopology C where
     rw [Sieve.pullback_comp]
     apply K.pullback_stable
     clear iZU Z
-    apply K.transitive (G.functorPushforward_hasLift_mem _ iUW)
+    apply K.transitive (G.functorPushforward_imageSieve_mem _ iUW)
     rintro Z _ ⟨U₁, iU₁U, iZU₁, ⟨iU₁W, e₂⟩, rfl⟩
     rw [Sieve.pullback_comp]
     apply K.pullback_stable

From eb6cc0e0fe6f8e0c548a3be44ea10d6ca90cdade Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Wed, 24 Jul 2024 18:59:17 +0800
Subject: [PATCH 8/9] more fix

---
 Mathlib/CategoryTheory/Sites/DenseSubsite.lean | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index 9b7a61284b13e1..f328a81b4de281 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -547,8 +547,8 @@ instance faithful_sheafPushforwardContinuous [G.IsDenseSubsite J K] :
   letI := IsDenseSubsite.isLocallyFull J K G
   inferInstance
 
-lemma hasLift_mem [G.IsDenseSubsite J K] {U V} (f : G.obj U ⟶ G.obj V) :
-    Sieve.hasLift G f ∈ J _ :=
+lemma imageSieve_mem [G.IsDenseSubsite J K] {U V} (f : G.obj U ⟶ G.obj V) :
+    G.imageSieve f ∈ J _ :=
   letI := IsDenseSubsite.isLocallyFull J K G
   IsDenseSubsite.functorPushforward_mem_iff.mp (G.functorPushforward_imageSieve_mem K f)
 
@@ -585,7 +585,7 @@ lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
     simp only [id_obj, comp_obj, StructuredArrow.proj_obj, RightExtension.coneAt_pt,
       RightExtension.mk_left, RightExtension.coneAt_π_app, const_obj_obj, op_obj,
       whiskeringLeft_obj_obj, RightExtension.mk_hom]
-    apply (Y.2 X _ (IsDenseSubsite.hasLift_mem J K G g)).isSeparatedFor.ext
+    apply (Y.2 X _ (IsDenseSubsite.imageSieve_mem J K G g)).isSeparatedFor.ext
     rintro V iVW ⟨iVU, e'⟩
     have := congr($e ≫ Y.1.map iVU.op)
     simp only [comp_obj, yoneda_map_app, Category.assoc, coyoneda_obj_obj, comp_map,
@@ -594,11 +594,11 @@ lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
     erw [← NatTrans.naturality] at this
     exact this
   · intro f
-    have (X Y Z) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : Sieve.hasLift G g f) : Exists _ := hf
+    have (X Y Z) (f : X ⟶ Y) (g : G.obj Y ⟶ G.obj Z) (hf : G.imageSieve g f) : Exists _ := hf
     choose l hl using this
     let c : Limits.Cone (StructuredArrow.proj (op (G.obj U)) G.op ⋙ Y.val) := by
       refine ⟨X, ⟨fun g ↦ ?_, ?_⟩⟩
-      · refine Y.2.amalgamate ⟨_, IsDenseSubsite.hasLift_mem J K G g.hom.unop⟩
+      · refine Y.2.amalgamate ⟨_, IsDenseSubsite.imageSieve_mem J K G g.hom.unop⟩
           (fun I ↦ f ≫ Y.1.map (l _ _ _ _ _ I.hf).op) fun I₁ I₂ r ↦ ?_
         apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (r.g₁ ≫ l _ _ _ _ _ I₁.hf)
           (r.g₂ ≫ l _ _ _ _ _ I₂.hf) ?_)).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
@@ -612,10 +612,10 @@ lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
         obtain ⟨i, rfl⟩ : ∃ i' : W₂ ⟶ W₁, i = i'.op := ⟨i.unop, rfl⟩
         simp only [const_obj_obj, id_obj, comp_obj, StructuredArrow.proj_obj, const_obj_map, op_obj,
           unop_comp, Quiver.Hom.unop_op, Category.id_comp, comp_map, StructuredArrow.proj_map]
-        apply Y.2.hom_ext ⟨_, IsDenseSubsite.hasLift_mem J K G (G.map i ≫ g)⟩
+        apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (G.map i ≫ g)⟩
         intro I
         simp only [Presheaf.IsSheaf.amalgamate_map, Category.assoc, ← Functor.map_comp, ← op_comp]
-        let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.hasLift_mem J K G g⟩ :=
+        let I' : GrothendieckTopology.Cover.Arrow ⟨_, IsDenseSubsite.imageSieve_mem J K G g⟩ :=
           ⟨_, I.f ≫ i, ⟨l _ _ _ _ _ I.hf, by simp [hl]⟩⟩
         refine Eq.trans ?_ (Y.2.amalgamate_map _ _ _ I').symm
         apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
@@ -628,7 +628,7 @@ lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
         const_obj_obj, op_obj, StructuredArrow.mk_hom_eq_self, map_id, whiskeringLeft_obj_obj,
         RightExtension.mk_hom, Category.id_comp, StructuredArrow.mk_left, unop_id] at this
       simp only [id_obj, yoneda_map_app, this]
-      apply Y.2.hom_ext ⟨_, IsDenseSubsite.hasLift_mem J K G (𝟙 (G.obj U))⟩ _ _ fun I ↦ ?_
+      apply Y.2.hom_ext ⟨_, IsDenseSubsite.imageSieve_mem J K G (𝟙 (G.obj U))⟩ _ _ fun I ↦ ?_
       apply (Y.2 X _ (IsDenseSubsite.equalizer_mem J K G (l _ _ _ _ _ I.hf)
         I.f (by simp [hl]))).isSeparatedFor.ext fun V iUV (hiUV : _ = _) ↦ ?_
       simp [← Functor.map_comp, ← op_comp, hiUV]

From c5093fe32d946c426abbf9f07d7293c29a1f459c Mon Sep 17 00:00:00 2001
From: Andrew Yang <the.erd.one@gmail.com>
Date: Fri, 26 Jul 2024 04:13:19 +0800
Subject: [PATCH 9/9] address comments

---
 Mathlib/CategoryTheory/Sites/DenseSubsite.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
index f328a81b4de281..70492f07dde804 100644
--- a/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
+++ b/Mathlib/CategoryTheory/Sites/DenseSubsite.lean
@@ -635,11 +635,11 @@ lemma isIso_ranCounit_app_of_isDenseSubsite (Y : Sheaf J A) (U X) :
 
 instance (Y : Sheaf J A) : IsIso ((G.sheafAdjunctionCocontinuous A J K).counit.app Y) := by
   apply (config := { allowSynthFailures := true })
-  ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
-  apply (config := { allowSynthFailures := true }) NatIso.isIso_of_isIso_app
+    ReflectsIsomorphisms.reflects (sheafToPresheaf J A)
+  rw [NatTrans.isIso_iff_isIso_app]
   intro ⟨U⟩
   apply (config := { allowSynthFailures := true }) ReflectsIsomorphisms.reflects yoneda
-  apply (config := { allowSynthFailures := true }) NatIso.isIso_of_isIso_app
+  rw [NatTrans.isIso_iff_isIso_app]
   intro ⟨X⟩
   simp only [comp_obj, sheafToPresheaf_obj, sheafPushforwardContinuous_obj_val_obj, yoneda_obj_obj,
     id_obj, sheafToPresheaf_map, sheafAdjunctionCocontinuous_counit_app_val, ranAdjunction_counit]