From 2bd8e4cdf8b626ea60ddcc7b6d423c21599b1449 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Sat, 23 May 2026 02:27:49 +0200
Subject: [PATCH 1/3] local epis

---
 Mathlib.lean                                  |   1 +
 Mathlib/CategoryTheory/EssentialImage.lean    |   5 +
 .../MorphismProperty/LocalEpi.lean            | 128 ++++++++++++++++++
 3 files changed, 134 insertions(+)
 create mode 100644 Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index 83b01155b045f9..43ca4b48bd2de8 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3156,6 +3156,7 @@ public import Mathlib.CategoryTheory.MorphismProperty.IsSmall
 public import Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
 public import Mathlib.CategoryTheory.MorphismProperty.Limits
 public import Mathlib.CategoryTheory.MorphismProperty.Local
+public import Mathlib.CategoryTheory.MorphismProperty.LocalEpi
 public import Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
 public import Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
 public import Mathlib.CategoryTheory.MorphismProperty.Quotient
diff --git a/Mathlib/CategoryTheory/EssentialImage.lean b/Mathlib/CategoryTheory/EssentialImage.lean
index 31e33fab22e793..21a44c4643ddfe 100644
--- a/Mathlib/CategoryTheory/EssentialImage.lean
+++ b/Mathlib/CategoryTheory/EssentialImage.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.CategoryTheory.NatIso
 public import Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
 public import Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
+public import Mathlib.Data.Set.Operations
 
 /-!
 # Essential image of a functor
@@ -48,6 +49,10 @@ def essImage (F : C ⥤ D) : ObjectProperty D := fun Y => ∃ X : C, Nonempty (F
 def essImage.witness {Y : D} (h : F.essImage Y) : C :=
   h.choose
 
+lemma isoClosure_eq_essImage : ObjectProperty.isoClosure (· ∈ Set.range F.obj) = F.essImage := by
+  ext
+  exact ⟨fun ⟨_, ⟨Z, rfl⟩, ⟨e⟩⟩ ↦ ⟨Z, ⟨e.symm⟩⟩, fun ⟨Z, ⟨e⟩⟩ ↦ ⟨F.obj Z, ⟨Z, rfl⟩, ⟨e.symm⟩⟩⟩
+
 /-- Extract the isomorphism between `F.obj h.witness` and `Y` itself. -/
 def essImage.getIso {Y : D} (h : F.essImage Y) : F.obj h.witness ≅ Y :=
   Classical.choice h.choose_spec
diff --git a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
new file mode 100644
index 00000000000000..89066e77906939
--- /dev/null
+++ b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.CategoryTheory.MorphismProperty.Limits
+public import Mathlib.CategoryTheory.Localization.Bousfield
+
+/-!
+# Local epimorphisms with respect to an object property
+
+Let `P` be an object property on a category `C`. We say that `f : X ⟶ Y`
+is a local epimorphism wrt. `P` if `f` cancels on the left for morphisms with
+codomain in `P`.
+
+If `C` is the category of presheafs on some category with Grothendieck topology `J` and `P` the
+property of being a sheaf for `J`, then being a local epimorphism wrt. `P` is being
+an epimorphism after sheafification.
+
+## Main declarations
+
+- `CategoryTheory.ObjectProperty.localEpi`: The morphism property of local epimorphisms.
+- `CategoryTheory.ObjectProperty.localEpi_mem_range_iff_epi`: If `F ⊣ G` and `G`
+  is fully faithful, then `f : X ⟶ Y` is a local epimorphism if and only if `F.map f` is an
+  epimorphism.
+-/
+
+@[expose] public section
+
+namespace CategoryTheory
+
+open Limits
+
+variable {C : Type*} [Category* C] {P : ObjectProperty C}
+
+namespace ObjectProperty
+
+/-- A morphism `f` is a local epimorphism wrt. the object property `P`
+if it satisfies left cancellation for morphisms with codomain in `P`. -/
+def localEpi (P : ObjectProperty C) : MorphismProperty C := fun _ _ f ↦
+  ∀ ⦃Z⦄, P Z → Function.Injective fun (g : _ ⟶ Z) ↦ f ≫ g
+
+instance : P.localEpi.IsMultiplicative where
+  id_mem X Z _ := by simpa using Function.injective_id
+  comp_mem f g hf hg T hT _ _ huv := hg hT (hf hT <| by simpa using huv)
+
+lemma localEpi_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f := by
+  intro Z hZ u v huv
+  rwa [← cancel_epi f]
+
+@[simp]
+lemma localEpi_top_apply_iff {X Y : C} {f : X ⟶ Y} :
+    (⊤ : ObjectProperty C).localEpi f ↔ Epi f :=
+  ⟨fun h ↦ ⟨fun _ _ huv ↦ h trivial huv⟩, fun _ ↦ localEpi_of_epi _⟩
+
+lemma localEpi_top_eq_epimorphisms : (⊤ : ObjectProperty C).localEpi = .epimorphisms C := by
+  ext
+  simp
+
+lemma localEpi_antitone : Antitone (localEpi (C := C)) :=
+  fun _ _ hPQ _ _ _ hf _ hZ _ _ huv ↦ hf (hPQ _ hZ) huv
+
+lemma localEpi_isoClosure : P.isoClosure.localEpi = P.localEpi := by
+  refine le_antisymm (localEpi_antitone <| le_isoClosure P) ?_
+  intro X Y f hf Z ⟨T, hT, ⟨e⟩⟩ u v huv
+  rw [← cancel_mono e.hom]
+  apply hf hT
+  simpa
+
+lemma isLocal_le_localEpi : P.isLocal ≤ P.localEpi :=
+  fun _ _ _ hf Z hZ ↦ (hf Z hZ).injective
+
+instance : P.localEpi.RespectsIso :=
+  MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ _ _ ↦ localEpi_of_epi _
+
+instance (W : MorphismProperty C) : P.localEpi.HasOfPrecompProperty W where
+  of_precomp {X Y Z} f g _ hfg T hT u v huv := hfg hT (by simp [huv])
+
+instance : P.localEpi.HasOfPostcompProperty P.isLocal where
+  of_postcomp {X Y Z} f g hg hfg T hT u v huv := by
+    obtain ⟨u, rfl⟩ := (hg _ hT).surjective u
+    obtain ⟨v, rfl⟩ := (hg _ hT).surjective v
+    simp [hfg hT (by simpa using huv)]
+
+instance : P.localEpi.IsStableUnderCobaseChange := by
+  refine .mk' fun X Y S f g _ hg T hT u v huv ↦ ?_
+  refine pushout.hom_ext (hg hT ?_) huv
+  simp [pushout.condition_assoc, huv]
+
+instance : P.localEpi.Respects P.isLocal where
+  precomp _ hf _ hg := MorphismProperty.comp_mem _ _ _ (isLocal_le_localEpi _ hf) hg
+  postcomp _ hf _ hg := MorphismProperty.comp_mem _ _ _ hg (isLocal_le_localEpi _ hf)
+
+variable {D : Type*} [Category* D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
+  [G.Faithful] [G.Full]
+include adj
+
+lemma localEpi_mem_range_iff_epi {X Y : C} (f : X ⟶ Y) :
+    localEpi (· ∈ Set.range G.obj) f ↔ Epi (F.map f) := by
+  rw [← dsimp% (localEpi (· ∈ Set.range G.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),
+    dsimp% adj.unit.naturality f,
+    dsimp% (localEpi (· ∈ Set.range G.obj)).precomp_iff _ _ (isLocal_adj_unit_app adj X)]
+  refine ⟨fun h ↦ ⟨fun {Z} u v huv ↦ ?_⟩, ?_⟩
+  · refine G.map_injective ?_
+    apply h ⟨Z, rfl⟩
+    simp [← Functor.map_comp, huv]
+  · rintro h _ ⟨Z, rfl⟩ u v huv
+    obtain ⟨u, rfl⟩ := G.map_surjective u
+    obtain ⟨v, rfl⟩ := G.map_surjective v
+    simp only [← G.map_comp, G.map_injective_iff, cancel_epi] at huv
+    rw [huv]
+
+lemma localEpi_mem_range_eq_inverseImage_epimorphisms :
+    localEpi (· ∈ Set.range G.obj) = (MorphismProperty.epimorphisms _).inverseImage F := by
+  ext X Y f
+  rw [localEpi_mem_range_iff_epi adj]
+  simp
+
+lemma localEpi_essImage :
+    G.essImage.localEpi = (MorphismProperty.epimorphisms _).inverseImage F := by
+  rw [← Functor.isoClosure_eq_essImage, localEpi_isoClosure,
+    localEpi_mem_range_eq_inverseImage_epimorphisms adj]
+
+end ObjectProperty
+
+end CategoryTheory

From f6f13b1c3ec3a5cb26bdc5a3e36b5094f9389b7f Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Wed, 27 May 2026 23:02:11 +0200
Subject: [PATCH 2/3] add reference

---
 Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
index 89066e77906939..6ec0bed53842d9 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
@@ -25,6 +25,10 @@ an epimorphism after sheafification.
 - `CategoryTheory.ObjectProperty.localEpi_mem_range_iff_epi`: If `F ⊣ G` and `G`
   is fully faithful, then `f : X ⟶ Y` is a local epimorphism if and only if `F.map f` is an
   epimorphism.
+
+## References
+
+The terminology is from [M. Kashiwara, P. Schapira, *Categories and Sheaves*, 16.1][Kashiwara2006].
 -/
 
 @[expose] public section

From bad1f8058c5c656cbb27b9138928fc56591591f2 Mon Sep 17 00:00:00 2001
From: Christian Merten <christian@merten.dev>
Date: Wed, 27 May 2026 23:18:10 +0200
Subject: [PATCH 3/3] rename to allow for dot notation

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

diff --git a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
index 6ec0bed53842d9..935459598ce7d3 100644
--- a/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean
@@ -50,14 +50,14 @@ instance : P.localEpi.IsMultiplicative where
   id_mem X Z _ := by simpa using Function.injective_id
   comp_mem f g hf hg T hT _ _ huv := hg hT (hf hT <| by simpa using huv)
 
-lemma localEpi_of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f := by
+lemma localEpi.of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f := by
   intro Z hZ u v huv
   rwa [← cancel_epi f]
 
 @[simp]
 lemma localEpi_top_apply_iff {X Y : C} {f : X ⟶ Y} :
     (⊤ : ObjectProperty C).localEpi f ↔ Epi f :=
-  ⟨fun h ↦ ⟨fun _ _ huv ↦ h trivial huv⟩, fun _ ↦ localEpi_of_epi _⟩
+  ⟨fun h ↦ ⟨fun _ _ huv ↦ h trivial huv⟩, fun _ ↦ .of_epi _⟩
 
 lemma localEpi_top_eq_epimorphisms : (⊤ : ObjectProperty C).localEpi = .epimorphisms C := by
   ext
@@ -77,7 +77,7 @@ lemma isLocal_le_localEpi : P.isLocal ≤ P.localEpi :=
   fun _ _ _ hf Z hZ ↦ (hf Z hZ).injective
 
 instance : P.localEpi.RespectsIso :=
-  MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ _ _ ↦ localEpi_of_epi _
+  MorphismProperty.respectsIso_of_isStableUnderComposition fun _ _ _ _ ↦ .of_epi _
 
 instance (W : MorphismProperty C) : P.localEpi.HasOfPrecompProperty W where
   of_precomp {X Y Z} f g _ hfg T hT u v huv := hfg hT (by simp [huv])