refactor: generalise IsLocalRingHom to monoids (#6045)

This lets `IsLocalRingHom` take two monoids instead of rings. Furthermore, it moves lemmas to be available a bit earlier where they are relevant to other theories, and tries to adapt those theories to use them a bit better.



Co-authored-by: jjdishere <emailboxofjjd@163.com>
Co-authored-by: Jiang Jiedong <107380768+jjdishere@users.noreply.github.com>
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

Mathlib.lean

@@ -3968,7 +3968,6 @@ import Mathlib.RingTheory.LocalRing.Module
 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import Mathlib.RingTheory.LocalRing.ResidueField.Defs
 import Mathlib.RingTheory.LocalRing.RingHom.Basic
-import Mathlib.RingTheory.LocalRing.RingHom.Defs
 import Mathlib.RingTheory.Localization.Algebra
 import Mathlib.RingTheory.Localization.AsSubring
 import Mathlib.RingTheory.Localization.AtPrime

Mathlib/Algebra/Associated/Basic.lean

@@ -248,6 +248,12 @@ theorem Irreducible.dvd_comm [Monoid M] {p q : M} (hp : Irreducible p) (hq : Irr
     p ∣ q ↔ q ∣ p :=
   ⟨hp.dvd_symm hq, hq.dvd_symm hp⟩
 
+theorem Irreducible.of_map {F : Type*} [Monoid M] [Monoid N] [FunLike F M N] [MonoidHomClass F M N]
+    {f : F} [IsLocalRingHom f] {x} (hfx : Irreducible (f x)) : Irreducible x :=
+  ⟨fun hu ↦ hfx.not_unit <| hu.map f,
+   by rintro p q rfl
+      exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)⟩
+
 section
 
 variable [Monoid M]

Mathlib/Algebra/Category/Ring/Instances.lean

@@ -38,7 +38,7 @@ instance Localization.epi' {R : CommRingCat} (M : Submonoid R) :
 
 instance CommRingCat.isLocalRingHom_comp {R S T : CommRingCat} (f : R ⟶ S) (g : S ⟶ T)
     [IsLocalRingHom g] [IsLocalRingHom f] : IsLocalRingHom (f ≫ g) :=
-  _root_.isLocalRingHom_comp _ _
+  RingHom.isLocalRingHom_comp _ _
 
 theorem isLocalRingHom_of_iso {R S : CommRingCat} (f : R ≅ S) : IsLocalRingHom f.hom :=
   { map_nonunit := fun a ha => by

Mathlib/Algebra/Group/Units/Equiv.lean

@@ -192,11 +192,10 @@ def MulEquiv.inv (G : Type*) [DivisionCommMonoid G] : G ≃* G :=
 theorem MulEquiv.inv_symm (G : Type*) [DivisionCommMonoid G] :
     (MulEquiv.inv G).symm = MulEquiv.inv G :=
   rfl
--- Porting note: no `add_equiv.neg_symm` in `mathlib3`
 
-@[to_additive]
-protected
-theorem MulEquiv.map_isUnit_iff {M N} [Monoid M] [Monoid N] [EquivLike F M N] [MonoidHomClass F M N]
-    (f : F) {m : M} : IsUnit (f m) ↔ IsUnit m :=
-  isUnit_map_of_leftInverse (MonoidHom.inverse (f : M →* N) (EquivLike.inv f)
-    (EquivLike.left_inv f) <| EquivLike.right_inv f) (EquivLike.left_inv f)
+instance isLocalRingHom_equiv [Monoid M] [Monoid N] [EquivLike F M N]
+    [MulEquivClass F M N] (f : F) : IsLocalRingHom f where
+  map_nonunit a ha := by
+    convert ha.map (f : M ≃* N).symm
+    rw [MulEquiv.eq_symm_apply]
+    rfl -- note to reviewers: ugly `rfl`

Mathlib/Algebra/Group/Units/Hom.lean

@@ -17,6 +17,18 @@ also contains unrelated results about `Units` that depend on `MonoidHom`.
 * `Units.map`: Turn a homomorphism from `α` to `β` monoids into a homomorphism from `αˣ` to `βˣ`.
 * `MonoidHom.toHomUnits`: Turn a homomorphism from a group `α` to `β` into a homomorphism from
   `α` to `βˣ`.
+* `IsLocalRingHom`: A predicate on monoid maps, requiring that it maps nonunits
+  to nonunits. For local rings, this means that the image of the unique maximal ideal is again
+  contained in the unique maximal ideal. This is developed earlier, and in the generality of
+  monoids, as it allows its use in non-local-ring related contexts, but it does have the
+  strange consequence that it does not require local rings, or even rings.
+
+## TODO
+
+The results that don't mention homomorphisms should be proved (earlier?) in a different file and be
+used to golf the basic `Group` lemmas.
+
+Add a `@[to_additive]` version of `IsLocalRingHom`.
 -/
 
 assert_not_exists MonoidWithZero
@@ -167,6 +179,7 @@ theorem of_leftInverse [MonoidHomClass G N M] {f : F} {x : M} (g : G)
     (hfg : Function.LeftInverse g f) (h : IsUnit (f x)) : IsUnit x := by
   simpa only [hfg x] using h.map g
 
+/-- Prefer `IsLocalRingHom.of_leftInverse`, but we can't get rid of this because of `ToAdditive`. -/
 @[to_additive]
 theorem _root_.isUnit_map_of_leftInverse [MonoidHomClass F M N] [MonoidHomClass G N M]
     {f : F} {x : M} (g : G) (hfg : Function.LeftInverse g f) :
@@ -194,3 +207,49 @@ theorem liftRight_inv_mul (f : M →* N) (h : ∀ x, IsUnit (f x)) (x) :
 
 end Monoid
 end IsUnit
+
+section IsLocalRingHom
+
+variable {G R S T F : Type*}
+
+variable [Monoid R] [Monoid S] [Monoid T] [FunLike F R S]
+
+/-- A local ring homomorphism is a map `f` between monoids such that `a` in the domain
+  is a unit if `f a` is a unit for any `a`. See `LocalRing.local_hom_TFAE` for other equivalent
+  definitions in the local ring case - from where this concept originates, but it is useful in
+  other contexts, so we allow this generalisation in mathlib. -/
+class IsLocalRingHom (f : F) : Prop where
+  /-- A local ring homomorphism `f : R ⟶ S` will send nonunits of `R` to nonunits of `S`. -/
+  map_nonunit : ∀ a, IsUnit (f a) → IsUnit a
+
+@[simp]
+theorem IsUnit.of_map (f : F) [IsLocalRingHom f] (a : R) (h : IsUnit (f a)) : IsUnit a :=
+  IsLocalRingHom.map_nonunit a h
+
+-- TODO : remove alias, change the parenthesis of `f` and `a`
+alias isUnit_of_map_unit := IsUnit.of_map
+
+variable [MonoidHomClass F R S]
+
+@[simp]
+theorem isUnit_map_iff (f : F) [IsLocalRingHom f] (a : R) : IsUnit (f a) ↔ IsUnit a :=
+  ⟨IsLocalRingHom.map_nonunit a, IsUnit.map f⟩
+
+theorem isLocalRingHom_of_leftInverse [FunLike G S R] [MonoidHomClass G S R]
+    {f : F} (g : G) (hfg : Function.LeftInverse g f) : IsLocalRingHom f where
+  map_nonunit a ha := by rwa [isUnit_map_of_leftInverse g hfg] at ha
+
+instance MonoidHom.isLocalRingHom_comp (g : S →* T) (f : R →* S) [IsLocalRingHom g]
+    [IsLocalRingHom f] : IsLocalRingHom (g.comp f) where
+  map_nonunit a := IsLocalRingHom.map_nonunit a ∘ IsLocalRingHom.map_nonunit (f := g) (f a)
+
+-- see note [lower instance priority]
+instance (priority := 100) isLocalRingHom_toMonoidHom (f : F) [IsLocalRingHom f] :
+    IsLocalRingHom (f : R →* S) :=
+  ⟨IsLocalRingHom.map_nonunit (f := f)⟩
+
+theorem MonoidHom.isLocalRingHom_of_comp (f : R →* S) (g : S →* T) [IsLocalRingHom (g.comp f)] :
+    IsLocalRingHom f :=
+  ⟨fun _ ha => (isUnit_map_iff (g.comp f) _).mp (ha.map g)⟩
+
+end IsLocalRingHom

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -87,6 +87,12 @@ noncomputable def inverse : M₀ → M₀ := fun x => if h : IsUnit x then ((h.u
 theorem inverse_unit (u : M₀ˣ) : inverse (u : M₀) = (u⁻¹ : M₀ˣ) := by
   rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]
 
+theorem IsUnit.ringInverse {x : M₀} (h : IsUnit x) : IsUnit (inverse x) :=
+  match h with
+  | ⟨u, hu⟩ => hu ▸ ⟨u⁻¹, (inverse_unit u).symm⟩
+
+theorem inverse_of_isUnit {x : M₀} (h : IsUnit x) : inverse x = ((h.unit⁻¹ : M₀ˣ) : M₀) := dif_pos h
+
 /-- By definition, if `x` is not invertible then `inverse x = 0`. -/
 @[simp]
 theorem inverse_non_unit (x : M₀) (h : ¬IsUnit x) : inverse x = 0 :=

Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

@@ -15,10 +15,35 @@ import Mathlib.Algebra.GroupWithZero.Hom
 
 assert_not_exists DenselyOrdered
 
-variable {α M₀ G₀ M₀' G₀' F F' : Type*}
+variable {α M M₀ G₀ M₀' G₀' F F' : Type*}
+
 variable [MonoidWithZero M₀]
 
+section Monoid
+
+variable [Monoid M] [GroupWithZero G₀]
+
+lemma isLocalRingHom_of_exists_map_ne_one [FunLike F G₀ M] [MonoidHomClass F G₀ M] {f : F}
+    (hf : ∃ x : G₀, f x ≠ 1) : IsLocalRingHom f where
+  map_nonunit a h := by
+    rcases eq_or_ne a 0 with (rfl | h)
+    · obtain ⟨t, ht⟩ := hf
+      refine (ht ?_).elim
+      have := map_mul f t 0
+      rw [← one_mul (f (t * 0)), mul_zero] at this
+      exact (h.mul_right_cancel this).symm
+    · exact ⟨⟨a, a⁻¹, mul_inv_cancel₀ h, inv_mul_cancel₀ h⟩, rfl⟩
+
+instance [GroupWithZero G₀] [FunLike F G₀ M₀] [MonoidWithZeroHomClass F G₀ M₀] [Nontrivial M₀]
+    (f : F) : IsLocalRingHom f :=
+  isLocalRingHom_of_exists_map_ne_one ⟨0, by simp⟩
+
+end Monoid
+
+section GroupWithZero
+
 namespace Commute
+
 variable [GroupWithZero G₀] {a b c d : G₀}
 
 /-- The `MonoidWithZero` version of `div_eq_div_iff_mul_eq_mul`. -/
@@ -107,3 +132,5 @@ end Units
 theorem map_zpow₀ {F G₀ G₀' : Type*} [GroupWithZero G₀] [GroupWithZero G₀'] [FunLike F G₀ G₀']
     [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ) : f (x ^ n) = f x ^ n :=
   map_zpow' f (map_inv₀ f) x n
+
+end GroupWithZero

Mathlib/Algebra/Polynomial/Expand.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 import Mathlib.RingTheory.Polynomial.Basic
-import Mathlib.RingTheory.LocalRing.RingHom.Basic
 
 /-!
 # Expand a polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.
@@ -269,9 +268,8 @@ section IsDomain
 
 variable (R : Type u) [CommRing R] [IsDomain R]
 
-theorem isLocalRingHom_expand {p : ℕ} (hp : 0 < p) :
-    IsLocalRingHom (↑(expand R p) : R[X] →+* R[X]) := by
-  refine ⟨fun f hf1 => ?_⟩; norm_cast at hf1
+theorem isLocalRingHom_expand {p : ℕ} (hp : 0 < p) : IsLocalRingHom (expand R p) := by
+  refine ⟨fun f hf1 => ?_⟩
   have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
   rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
   rw [hf2, isUnit_C] at hf1; rw [expand_eq_C hp] at hf2; rwa [hf2, isUnit_C]
@@ -281,7 +279,7 @@ variable {R}
 theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : R[X]} (hf : Irreducible (expand R p f)) :
     Irreducible f :=
   let _ := isLocalRingHom_expand R hp.bot_lt
-  of_irreducible_map (↑(expand R p)) hf
+  hf.of_map
 
 theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} :
     Irreducible (expand R (p ^ n) f) → Irreducible f :=

Mathlib/Algebra/Ring/Equiv.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Callum Sutton, Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Prod
 import Mathlib.Algebra.Group.Opposite
-import Mathlib.Algebra.Group.Units.Equiv
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.Ring.Hom.Defs
 import Mathlib.Logic.Equiv.Set
@@ -805,9 +804,6 @@ protected theorem map_pow (f : R ≃+* S) (a) : ∀ n : ℕ, f (a ^ n) = f a ^ n
 
 end GroupPower
 
-protected theorem isUnit_iff (f : R ≃+* S) {a} : IsUnit (f a) ↔ IsUnit a :=
-  MulEquiv.map_isUnit_iff f
-
 end RingEquiv
 
 namespace MulEquiv

Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean

@@ -282,6 +282,8 @@ def identityToΓSpec : 𝟭 LocallyRingedSpace.{u} ⟶ Γ.rightOp ⋙ Spec.toLoc
         = toΓSpecFun X x := by rw [ContinuousMap.coe_mk]
       erw [this]
       dsimp [toΓSpecFun]
+      -- TODO: this instance was found automatically before #6045
+      have := @AlgebraicGeometry.LocallyRingedSpace.isLocalRingHomStalkMap X Y
       -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
       erw [← LocalRing.comap_closedPoint (f.stalkMap x), ←
         PrimeSpectrum.comap_comp_apply, ← PrimeSpectrum.comap_comp_apply]