feat(Algebra/Group/Submonoid/Units): units in MonoidHom.eqLocusM (leanprover-community#40171)

This PR adds `MonoidHom.isUnit_eqLocusM_mk_iff`, which is the monoid version of `RingHom.isUnit_eqLocus_mk_iff`.
@eric-wieser

Author: BryceT233

Mathlib/Algebra/Group/Submonoid/Units.lean

@@ -339,3 +339,17 @@ def unitsEquivSelf (H : Subgroup G) : H.units ≃* H :=
   H.unitsEquivUnitsType.trans (toUnits (G := H)).symm
 
 end Subgroup
+
+@[to_additive]
+theorem MonoidHom.isUnit_eqLocusM_mk_iff {N : Type*} [Monoid N] (f g : M →* N) {r : M}
+    (hr : f r = g r) : IsUnit (⟨r, hr⟩ : f.eqLocusM g) ↔ IsUnit r := by
+  refine ⟨fun h ↦ h.map (SubmonoidClass.subtype _), fun h ↦ ?_⟩
+  obtain ⟨s, hs⟩ := isUnit_iff_exists.mp h
+  suffices ∃ a, r * a = 1 ∧ f a = g a ∧ a * r = 1 by
+    simpa [isUnit_iff_exists, ← Subtype.val_inj]
+  refine ⟨s, hs.left, ?_, hs.right⟩
+  rw [← mul_one (f s), ← map_one g, ← hs.left, map_mul, ← mul_assoc, ← hr, ← map_mul,
+    hs.right, map_one, one_mul]
+
+instance {N : Type*} [Monoid N] (f g : M →* N) : IsLocalHom (f.eqLocusM g).subtype where
+  map_nonunit r := f.isUnit_eqLocusM_mk_iff g r.prop |>.2

Mathlib/Algebra/Ring/Subring/Units.lean

@@ -11,6 +11,8 @@ public import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 public import Mathlib.Algebra.Order.Ring.Defs
 public import Mathlib.Algebra.Ring.Subring.Basic
 
+import Mathlib.Algebra.Group.Submonoid.Units
+
 /-!
 
 # Unit subgroups of a ring
@@ -31,14 +33,22 @@ theorem Units.mem_posSubgroup {R : Type*} [Semiring R] [LinearOrder R] [IsStrict
     (u : Rˣ) : u ∈ Units.posSubgroup R ↔ (0 : R) < u :=
   Iff.rfl
 
-theorem RingHom.isUnit_eqLocus_mk_iff {R T : Type*} [Ring R] [Semiring T] (f g : R →+* T)
-    {r : R} (hr : f r = g r) : IsUnit (⟨r, hr⟩ : f.eqLocus g) ↔ IsUnit r := by
-  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-  · simp [isUnit_iff_exists, ← Subtype.val_inj] at h ⊢
-    grind
-  obtain ⟨s, hs⟩ := isUnit_iff_exists.mp h
-  suffices ∃ a, r * a = 1 ∧ f a = g a ∧ a * r = 1 by
-    simpa [isUnit_iff_exists, ← Subtype.val_inj]
-  refine ⟨s, hs.left, ?_, hs.right⟩
-  rw [← mul_one (f s), ← map_one g, ← hs.left, map_mul, ← mul_assoc, ← hr, ← map_mul,
-    hs.right, map_one, one_mul]
+namespace RingHom
+
+variable {R T : Type*} [Semiring T]
+
+theorem isUnit_eqLocusS_mk_iff [Semiring R] (f g : R →+* T) {r : R} (hr : f r = g r) :
+    IsUnit (⟨r, hr⟩ : f.eqLocusS g) ↔ IsUnit r :=
+  MonoidHom.isUnit_eqLocusM_mk_iff ..
+
+theorem isUnit_eqLocus_mk_iff [Ring R] (f g : R →+* T) {r : R} (hr : f r = g r) :
+    IsUnit (⟨r, hr⟩ : f.eqLocus g) ↔ IsUnit r :=
+  MonoidHom.isUnit_eqLocusM_mk_iff ..
+
+instance [Semiring R] (f g : R →+* T) : IsLocalHom (f.eqLocusS g).subtype where
+  map_nonunit r := f.isUnit_eqLocusS_mk_iff g r.prop |>.2
+
+instance [Ring R] (f g : R →+* T) : IsLocalHom (f.eqLocus g).subtype where
+  map_nonunit r := f.isUnit_eqLocus_mk_iff g r.prop |>.2
+
+end RingHom