From e4aa60ef1eb17f67e4fd4f3e7e5d59146b9dafb4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <joel.riou@universite-paris-saclay.fr>
Date: Tue, 27 Jan 2026 21:07:28 +0100
Subject: [PATCH] feat(CategoryTheory): transport a NormalMono structure via an
 isomorphism of arrows

---
 .../Limits/Shapes/Equalizers.lean             |  5 +--
 .../Limits/Shapes/NormalMono/Basic.lean       | 31 +++++++++++++++++++
 2 files changed, 34 insertions(+), 2 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
index a3edd43e51ac49..0e0836fc58da29 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
@@ -298,8 +298,9 @@ theorem parallelPairHom_app_one {X' Y' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y')
 its components. -/
 @[simps!]
 def parallelPair.ext {F G : WalkingParallelPair ⥤ C} (zero : F.obj zero ≅ G.obj zero)
-    (one : F.obj one ≅ G.obj one) (left : F.map left ≫ one.hom = zero.hom ≫ G.map left)
-    (right : F.map right ≫ one.hom = zero.hom ≫ G.map right) : F ≅ G :=
+    (one : F.obj one ≅ G.obj one)
+    (left : F.map left ≫ one.hom = zero.hom ≫ G.map left := by cat_disch)
+    (right : F.map right ≫ one.hom = zero.hom ≫ G.map right := by cat_disch) : F ≅ G :=
   NatIso.ofComponents
     (by
       rintro ⟨j⟩
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
index 20824588c6ded9..18a45ff7964178 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/NormalMono/Basic.lean
@@ -115,6 +115,21 @@ def normalOfIsPullbackFstOfNormal {P Q R S : C} {f : P ⟶ Q} {g : P ⟶ R} {h :
     NormalMono f :=
   normalOfIsPullbackSndOfNormal comm.symm (PullbackCone.flipIsLimit t)
 
+/-- Transport a `NormalMono` structure via an isomorphism of arrows. -/
+def NormalMono.ofArrowIso {X Y : C} {f : X ⟶ Y}
+    (hf : NormalMono f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
+    NormalMono f' where
+  Z := hf.Z
+  g := e.inv.right ≫ hf.g
+  w := by
+    have := Arrow.w e.inv
+    dsimp at this
+    rw [← reassoc_of% this, hf.w, comp_zero]
+  isLimit := by
+    refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isLimit
+    · exact parallelPair.ext (Arrow.rightFunc.mapIso e) (Iso.refl _)
+    · exact Fork.ext (Arrow.leftFunc.mapIso e)
+
 section
 
 variable (C)
@@ -219,6 +234,22 @@ open Opposite
 
 variable [HasZeroMorphisms C]
 
+/-- Transport a `NormalEpi` structure via an isomorphism of arrows. -/
+def NormalEpi.ofArrowIso [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y}
+    (hf : NormalEpi f) {X' Y' : C} {f' : X' ⟶ Y'} (e : Arrow.mk f ≅ Arrow.mk f') :
+    NormalEpi f' where
+  W := hf.W
+  g := hf.g ≫ e.hom.left
+  w := by
+    have := Arrow.w e.hom
+    dsimp at this
+    rw [Category.assoc, this, reassoc_of% hf.w, zero_comp]
+  isColimit := by
+    refine (IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_).1 hf.isColimit
+    · exact parallelPair.ext (Iso.refl _) (Arrow.leftFunc.mapIso e)
+    · exact Cofork.ext (Arrow.rightFunc.mapIso e) (by simp [Cofork.π])
+
+
 /-- A normal mono becomes a normal epi in the opposite category. -/
 def normalEpiOfNormalMonoUnop {X Y : Cᵒᵖ} (f : X ⟶ Y) (m : NormalMono f.unop) : NormalEpi f where
   W := op m.Z