generalize IsLocalRingHom to IsLocalMonoidHom

Stream: mathlib4

[Jiang Jiedong]

Hi everyone,

I am trying to add the following lemma into Mathlib.

theorem isUnit_map_iff' [MulEquivClass E M N] (f : E) {a} : IsUnit (f a) ↔ IsUnit a :=

Currently the following lemma is ready in Mathlib

theorem isUnit_map_iff (f : R →+* S) [IsLocalRingHom f] (a) : IsUnit (f a) ↔ IsUnit a :=

These two lemmas have the same result. Should we generalize an abstract structure IsLocalMonoidHom here? Then both MulEquiv, IsLocalRingHom will be instances for this new class. So we can state a unique theorem isUnit_map_iff using IsLocalMonoidHom. Thanks to @Eric Wieser for this suggestion.

[Eric Wieser]

I think we can just rename IsLocalRingHom and make it take a MonoidHomClass

[Jiang Jiedong]

I agree. Although the current definition of IsLocalRingHom requires semiring structures, but it only uses the monoid structure.

Maybe a minor problem is that the terminology will change a lot. Since "local ring maps" is quite a common terminology in algebraic geometry and algebraic number theory. It would be changed to a less familiar phrase "local monoid maps".

Maybe we can rename it to IsLocalHom.

[Eric Wieser]

Indeed, the problem is not a technical one, but on picking the right terminology!

[Johan Commelin]

I like IsLocalHom.

[Yaël Dillies]

Local to a locale, right? :wink: That's a very ambiguous name otherwise

[Jireh Loreaux]

I think there was already a PR to do this a while back? But I think it ran into performance issues. Let me see if I can find it.

[Jireh Loreaux]

#6045

[Jireh Loreaux]

pinging @Eric Rodriguez

[Eric Rodriguez]

yeah it did at the time, and I got very little time to work on it since - I'm not sure I'd be best suited to fix these issues at the moment, I have very little mathlib time these days :(

[Eric Rodriguez]

on the other hand I think it was certainly worth doing then on the mathematical axis and I don't see why it wouldn't be worth doing now