feat(*): introduce classes for types of homomorphism (#9888)
This PR is the main proof-of-concept in my plan to use typeclasses to reduce duplication surrounding `hom` classes. Essentially, I want to take each type of bundled homs, such as `monoid_hom`, and add a class `monoid_hom_class` which has an instance for each *type* extending `monoid_hom`. Declarations that now take a parameter of the specific type `monoid_hom M N` can instead take a more general `{F : Type*} [monoid_hom_class F M N] (f : F)`; this means we don't need to duplicate e.g. `monoid_hom.map_prod` to `ring_hom.map_prod`, `mul_equiv.map_prod`, `ring_equiv.map_prod`, or `monoid_hom.map_div` to `ring_hom.map_div`, `mul_equiv.map_div`, `ring_equiv.map_div`, ...
Basically, instead of having `O(n * k)` declarations for `n` types of homs and `k` lemmas, following the plan we only need `O(n + k)`.
## Overview
* Change `has_coe_to_fun` to include the type of the function as a parameter (rather than a field of the structure) (**done** as part of #7033)
* Define a class `fun_like`, analogous to `set_like`, for types of bundled function + proof (**done** in #10286)
* Extend `fun_like` for each `foo_hom` to create a `foo_hom_class` (**done** in this PR for `ring_hom` and its ancestors, **todo** in follow-up for the rest)
* Change parameters of type `foo_hom A B` to take `{F : Type*} [foo_hom_class F A B] (f : F)` instead (**done** in this PR for `map_{add,zero,mul,one,sub,div}`, **todo** in follow-up for remaining declarations)
## API changes
Lemmas matching `*_hom.map_{add,zero,mul,one,sub,div}` are deprecated. Use the new `simp` lemmas called simply `map_add`, `map_zero`, ...
Namespaced lemmas of the form `map_{add,zero,mul,one,sub,div}` are now protected. This includes e.g. `polynomial.map_add` and `multiset.map_add`, which involve `polynomial.map` and `multiset.map` respectively. In fact, it should be possible to turn those `map` definitions into bundled maps, so we don't even need to worry about the name change.
## New classes
* `zero_hom_class`, `one_hom_class` defines `map_zero`, `map_one`
* `add_hom_class`, `mul_hom_class` defines `map_add`, `map_mul`
* `add_monoid_hom_class`, `monoid_hom_class` extends `{zero,one}_hom_class`, `{add,mul}_hom_class`
* `monoid_with_zero_hom_class` extends `monoid_hom_class` and `zero_hom_class`
* `ring_hom_class` extends `monoid_hom_class`, `add_monoid_hom_class` and `monoid_with_zero_hom_class`
## Classes still to be implemented
Some of the core algebraic homomorphisms are still missing their corresponding classes:
* `mul_action_hom_class` defines `map_smul`
* `distrib_mul_action_hom_class`, `mul_semiring_action_hom_class` extends the above
* `linear_map_class` extends `add_hom_class` and defines `map_smulₛₗ`
* `alg_hom_class` extends `ring_hom_class` and defines `commutes`
We could also add an `equiv_like` and its descendants `add_equiv_class`, `mul_equiv_class`, `ring_equiv_class`, `linear_equiv_class`, ...
## Other changes
`coe_fn_coe_base` now has an appropriately low priority, so it doesn't take precedence over `fun_like.has_coe_to_fun`.
## Why are you unbundling the morphisms again?
It's not quite the same thing as unbundling. When using unbundled morphisms, parameters have the form `(f : A → B) (hf : is_foo_hom f)`; bundled morphisms look like `(f : foo_hom A B)` (where `foo_hom A B` is equivalent to `{ f : A → B // is_foo_hom f }`; typically you would use a custom structure instead of `subtype`). This plan puts a predicate on the *type* `foo_hom` rather than the *elements* of the type as you would with unbundled morphisms. I believe this will preserve the advantages of the bundled approach (being able to talk about the identity map, making it work with `simp`), while addressing one of its disadvantages (needing to duplicate all the lemmas whenever extending the type of morphisms).
## Discussion
Main Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclasses.20for.20morphisms
Some other threads referencing this plan:
* https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Morphism.20refactor
* https://leanprover.zulipchat.com/#narrow/stream/263328-triage/topic/issue.20.231044.3A.20bundling.20morphisms
* #1044
* #4985
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
