Commit 2026-06-06 05:44 1d780199

fix(RingTheory/Valuation): change ValueGroup from taking HomClass to Hom (#36911)

Main description

Following rules described in #mathlib4 > Mathlib's morphism hierarchy @ 💬, this PR

1. refactors MonoidWithZeroHom.valueMonoid, MonoidWithZeroHom.valueGroup, MonoidWithZeroHom.ValueGroup₀, and MonoidWithZeroHom.ValueGroup₀.embedding to take a concrete MonoidWithZeroHom as input instead of a MonoidWithZeroHomClass instance;
2. renames MonoidWithZeroHomClass.toMonoidWithZeroHom to MonoidWithZeroHom.ofClass
3. makes MonoidWithZeroHom.ofClass no longer an instance.

What we gain

As a result, we are able to remove several erw and many set_option backward.isDefEq.respectTransparency false in.

Foreseen problems and its solution

The trade-off is that now definitions taking a MonoidWithZeroHom as input can no longer take a valuation v directly. The fix (foreseen by the same zulip thread) is that we write an explicit coercion .ofClass v replacing v. A simple replacement solves the problem in most of the cases. e.g. ValueGroup₀ (.ofClass (Valued.v (R := R))) instead of ValueGroup₀ (Valued.v (R := R)).

Things not implemented in this PR:

1. MonoidHom.mrange still takes a MonoidHomClass. This should be refactored together with renaming MonoidHomClass.toMonoidHom to MonoidHom.ofClass in the future.