feat(CategoryTheory): effective epi implies strong epi (#31860)

Also:
* Import `EffectiveEpi.Basic` in the file defining `RegularEpi`, and prove the relationship there.
* Fix some names and golf some proofs in `EffectiveEpi.Basic`

Author: dagurtomas

Mathlib/CategoryTheory/EffectiveEpi/Basic.lean

@@ -39,7 +39,7 @@ our notion of `EffectiveEpi` is often called "strict epi" in the literature.
 
 namespace CategoryTheory
 
-open Limits
+open Limits Category
 
 variable {C : Type*} [Category C]
 
@@ -95,13 +95,21 @@ lemma EffectiveEpi.uniq {X Y W : C} (f : Y ⟶ X) [EffectiveEpi f]
     m = EffectiveEpi.desc f e h :=
   (EffectiveEpi.getStruct f).uniq e h _ hm
 
-instance epiOfEffectiveEpi {X Y : C} (f : Y ⟶ X) [EffectiveEpi f] : Epi f := by
-  constructor
-  intro W m₁ m₂ h
-  have : m₂ = EffectiveEpi.desc f (f ≫ m₂)
-    (fun {Z} g₁ g₂ h => by simp only [← Category.assoc, h]) := EffectiveEpi.uniq _ _ _ _ rfl
-  rw [this]
-  exact EffectiveEpi.uniq _ _ _ _ h
+open EffectiveEpi Category
+
+instance epi_of_effectiveEpi {X Y : C} (f : Y ⟶ X) [EffectiveEpi f] : Epi f where
+  left_cancellation m₁ m₂ h := by
+    rw [show m₂ = desc f (f ≫ m₂) (fun _ _ h => by simp [← assoc, h]) from uniq _ _ _ _ rfl]
+    exact uniq _ _ _ _ h
+
+@[deprecated (since := "2025-11-20")] alias epiOfEffectiveEpi := epi_of_effectiveEpi
+
+instance (priority := 100) strongEpi_of_effectiveEpi {X Y : C} (f : X ⟶ Y) [EffectiveEpi f] :
+    StrongEpi f :=
+  StrongEpi.mk' fun A B z hz u v sq ↦
+    have : ∀ {Z : C} (g₁ g₂ : Z ⟶ X), g₁ ≫ f = g₂ ≫ f → g₁ ≫ u = g₂ ≫ u := fun _ _ h ↦ by
+      simpa [← sq.w, cancel_mono_assoc_iff] using h =≫ v
+    CommSq.HasLift.mk' ⟨desc f u this, fac f u this, (cancel_epi f).1 ((by simp [← sq.w]))⟩
 
 /--
 This structure encodes the data required for a family of morphisms to be effective epimorphic.
@@ -171,7 +179,7 @@ lemma EffectiveEpiFamily.hom_ext {B W : C} {α : Type*} (X : α → C) (π : (a
     [EffectiveEpiFamily X π] (m₁ m₂ : B ⟶ W) (h : ∀ a, π a ≫ m₁ = π a ≫ m₂) :
     m₁ = m₂ := by
   have : m₂ = EffectiveEpiFamily.desc X π (fun a => π a ≫ m₂)
-      (fun a₁ a₂ g₁ g₂ h => by simp only [← Category.assoc, h]) := by
+      (fun a₁ a₂ g₁ g₂ h => by simp only [← assoc, h]) := by
     apply EffectiveEpiFamily.uniq; intro; rfl
   rw [this]
   exact EffectiveEpiFamily.uniq _ _ _ _ _ h
@@ -224,7 +232,7 @@ def effectiveEpiFamilyStructOfIsIsoDesc {B : C} {α : Type*} (X : α → C)
     intro a
     have : π a = Sigma.ι X a ≫ (asIso (Sigma.desc π)).hom := by simp only [asIso_hom,
       colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
-    rw [this, Category.assoc]
+    rw [this, assoc]
     simp only [asIso_hom, asIso_inv, IsIso.hom_inv_id_assoc, colimit.ι_desc, Cofan.mk_pt,
       Cofan.mk_ι_app]
   uniq e h m hm := by

Mathlib/CategoryTheory/EffectiveEpi/RegularEpi.lean

@@ -6,62 +6,5 @@ Authors: Dagur Asgeirsson
 module
 
 public import Mathlib.CategoryTheory.Limits.Shapes.RegularMono
-public import Mathlib.CategoryTheory.EffectiveEpi.Basic
-/-!
 
-# The relationship between effective and regular epimorphisms.
-
-This file proves that the notions of regular epi and effective epi are equivalent for morphisms with
-kernel pairs, and that regular epi implies effective epi in general.
--/
-
-@[expose] public section
-
-namespace CategoryTheory
-
-open Limits RegularEpi
-
-variable {C : Type*} [Category C]
-
-/-- The data of an `EffectiveEpi` structure on a `RegularEpi`. -/
-def effectiveEpiStructOfRegularEpi {B X : C} (f : X ⟶ B) [RegularEpi f] :
-    EffectiveEpiStruct f where
-  desc _ h := Cofork.IsColimit.desc isColimit _ (h _ _ w)
-  fac _ _ := Cofork.IsColimit.π_desc' isColimit _ _
-  uniq _ _ _ hg := Cofork.IsColimit.hom_ext isColimit (hg.trans
-    (Cofork.IsColimit.π_desc' _ _ _).symm)
-
-instance {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpi f :=
-  ⟨⟨effectiveEpiStructOfRegularEpi f⟩⟩
-
-/-- A morphism which is a coequalizer for its kernel pair is an effective epi. -/
-theorem effectiveEpiOfKernelPair {B X : C} (f : X ⟶ B) [HasPullback f f]
-    (hc : IsColimit (Cofork.ofπ f pullback.condition)) : EffectiveEpi f :=
-  let _ := regularEpiOfKernelPair f hc
-  inferInstance
-
-/-- An effective epi which has a kernel pair is a regular epi. -/
-noncomputable instance regularEpiOfEffectiveEpi {B X : C} (f : X ⟶ B) [HasPullback f f]
-    [EffectiveEpi f] : RegularEpi f where
-  W := pullback f f
-  left := pullback.fst f f
-  right := pullback.snd f f
-  w := pullback.condition
-  isColimit := {
-    desc := fun s ↦ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
-      simp only [Cofork.app_one_eq_π]
-      rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
-      simp)
-    fac := by
-      intro s j
-      have := EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
-          simp only [Cofork.app_one_eq_π]
-          rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
-          simp)
-      simp only [Functor.const_obj_obj, Cofork.app_one_eq_π] at this
-      cases j with
-      | zero => simp [this]
-      | one => simp [this]
-    uniq := fun _ _ h ↦ EffectiveEpi.uniq f _ _ _ (h WalkingParallelPair.one) }
-
-end CategoryTheory
+deprecated_module (since := "2025-11-20")

Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean

@@ -5,12 +5,10 @@ Authors: Kim Morrison, Bhavik Mehta
 -/
 module
 
+public import Mathlib.CategoryTheory.EffectiveEpi.Basic
 public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
-public import Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
 public import Mathlib.CategoryTheory.Limits.Shapes.Equalizers
-public import Mathlib.CategoryTheory.MorphismProperty.Basic
 public import Mathlib.CategoryTheory.MorphismProperty.Composition
-public import Mathlib.Lean.Expr.Basic
 
 /-!
 # Definitions and basic properties of regular monomorphisms and epimorphisms.
@@ -27,8 +25,12 @@ and constructions
 * `RegularMono f → Mono f`
 as well as the dual definitions/constructions for regular epimorphisms.
 
-Additionally, we give the construction
-* `RegularEpi f ⟶ StrongEpi f`.
+Additionally, we give the constructions
+* `RegularEpi f → EffectiveEpi f`, from which it can be deduced that regular epimorphisms are
+  strong.
+* `regularEpiOfEffectiveEpi`: constructs a `RegularEpi f` instance from `EffectiveEpi f` and
+  `HasPullback f f`.
+
 
 We also define classes `IsRegularMonoCategory` and `IsRegularEpiCategory` for categories in which
 every monomorphism or epimorphism is regular, and deduce that these categories are
@@ -311,6 +313,49 @@ noncomputable def regularEpiOfKernelPair {B X : C} (f : X ⟶ B) [HasPullback f
   w := pullback.condition
   isColimit := hc
 
+/-- The data of an `EffectiveEpi` structure on a `RegularEpi`. -/
+def effectiveEpiStructOfRegularEpi {B X : C} (f : X ⟶ B) [RegularEpi f] :
+    EffectiveEpiStruct f where
+  desc _ h := Cofork.IsColimit.desc RegularEpi.isColimit _ (h _ _ RegularEpi.w)
+  fac _ _ := Cofork.IsColimit.π_desc' RegularEpi.isColimit _ _
+  uniq _ _ _ hg := Cofork.IsColimit.hom_ext RegularEpi.isColimit (hg.trans
+    (Cofork.IsColimit.π_desc' _ _ _).symm)
+
+instance {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpi f :=
+  ⟨⟨effectiveEpiStructOfRegularEpi f⟩⟩
+
+/-- A morphism which is a coequalizer for its kernel pair is an effective epi. -/
+theorem effectiveEpi_of_kernelPair {B X : C} (f : X ⟶ B) [HasPullback f f]
+    (hc : IsColimit (Cofork.ofπ f pullback.condition)) : EffectiveEpi f :=
+  let _ := regularEpiOfKernelPair f hc
+  inferInstance
+
+@[deprecated (since := "2025-11-20")] alias effectiveEpiOfKernelPair := effectiveEpi_of_kernelPair
+
+/-- An effective epi which has a kernel pair is a regular epi. -/
+noncomputable instance regularEpiOfEffectiveEpi {B X : C} (f : X ⟶ B) [HasPullback f f]
+    [EffectiveEpi f] : RegularEpi f where
+  W := pullback f f
+  left := pullback.fst f f
+  right := pullback.snd f f
+  w := pullback.condition
+  isColimit := {
+    desc := fun s ↦ EffectiveEpi.desc f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
+      simp only [Cofork.app_one_eq_π]
+      rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
+      simp)
+    fac := by
+      intro s j
+      have := EffectiveEpi.fac f (s.ι.app WalkingParallelPair.one) fun g₁ g₂ hg ↦ (by
+          simp only [Cofork.app_one_eq_π]
+          rw [← pullback.lift_snd g₁ g₂ hg, Category.assoc, ← Cofork.app_zero_eq_comp_π_right]
+          simp)
+      simp only [Functor.const_obj_obj, Cofork.app_one_eq_π] at this
+      cases j with
+      | zero => simp [this]
+      | one => simp [this]
+    uniq := fun _ _ h ↦ EffectiveEpi.uniq f _ _ _ (h WalkingParallelPair.one) }
+
 /-- Every split epimorphism is a regular epimorphism. -/
 instance (priority := 100) RegularEpi.ofSplitEpi (f : X ⟶ Y) [IsSplitEpi f] : RegularEpi f where
   W := X
@@ -364,19 +409,9 @@ def regularOfIsPushoutFstOfRegular {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h
     RegularEpi k :=
   regularOfIsPushoutSndOfRegular comm.symm (PushoutCocone.flipIsColimit t)
 
+@[deprecated "No replacement" (since := "2025-11-20")]
 instance (priority := 100) strongEpi_of_regularEpi (f : X ⟶ Y) [RegularEpi f] : StrongEpi f :=
-  StrongEpi.mk'
-    (by
-      intro A B z hz u v sq
-      have : (RegularEpi.left : RegularEpi.W f ⟶ X) ≫ u = RegularEpi.right ≫ u := by
-        apply (cancel_mono z).1
-        simp only [Category.assoc, sq.w, RegularEpi.w_assoc]
-      obtain ⟨t, ht⟩ := RegularEpi.desc' f u this
-      exact
-        CommSq.HasLift.mk'
-          ⟨t, ht,
-            (cancel_epi f).1
-              (by simp only [← Category.assoc, ht, ← sq.w])⟩)
+  inferInstance
 
 /-- A regular epimorphism is an isomorphism if it is a monomorphism. -/
 theorem isIso_of_regularEpi_of_mono (f : X ⟶ Y) [RegularEpi f] [Mono f] : IsIso f :=