Concretise submonoid

[grunweg]

---

~45 sorries left. Many need actual fixes. Help very welcome!
Helps with #31365.

[github-actions]

PR summary 1201efd6e5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ instance (v : Valuation R Γ₀) : CommMonoidWithZero (MonoidHomClass.toMonoidHom v).mrange
+ map_toMonoidHom_powers
+ toAddMonoidHom_refl'
+ toMonoidHom_refl'
- instance (v : Valuation R Γ₀) : CommMonoidWithZero (MonoidHom.mrange (.ofClass v : R →*₀ _))
- instance {f : A →+* B} (a : A) [Away (f a) Bₚ] : IsLocalization (.map f (.powers a)) Bₚ := by
- map_coe_toMonoidHom
- map_coe_toMulEquiv

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 1201efd6e5
Reference commit a4bb538cf7

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[jjdishere]

I believe some problems are caused by current partial change (still using FooHom.toMonoidHom, not uniformed to MonoidHomClass.toMonoidHom).

[jjdishere]

around half of problems can be solved by an additional MonoidHom.coe_coe.

[grunweg-bot]

I believe some problems are caused by current partial change (still using FooHom.toMonoidHom, not uniformed to MonoidHomClass.toMonoidHom).

That's very possible; I tried to do incremental changes. Do you have an example in mind which definitions (or lemmas) should be changed? Or do you mean that the fix should often be to use MonoidHomClass.toMonoidHom f instead of f.toMonoidHom (when f is e.g. an algebra morphism)? (I've certainly done this too often.)

[jjdishere]

That's very possible; I tried to do incremental changes. Do you have an example in mind which definitions (or lemmas) should be changed? Or do you mean that the fix should often be to use MonoidHomClass.toMonoidHom f instead of f.toMonoidHom (when f is e.g. an algebra morphism)? (I've certainly done this too often.)

It's more like choosing a normal form. Since instance synthesis don't see the two forms IsLocalization (M.map (MonoidHomClass.toMonoidHom f)) S and IsLocalization (M.map f.toMonoidHom) S are equal, we have to stick to one of them for the whole library. I believe the first one is what we want. Most of the theorems with hypothesis/conclusion including f.toMonoidHom should be changed to MonoidHomClass.toMonoidHom f.

I also did a minimal change to make mathlib build. Lots of f.toMonoidHom remains.