feat(*): define classes for coercions that are homomorphisms (#17048) This PR is part of my plan to refactor algebra_map. It introduces new classes that should connect coercions (↑s) and bundled homomorphisms, e.g. ring_hom, so that e.g. an instance of coe_ring_hom R S states that there is a canonical ring homomorphism ring_hom.coe R S from R to S. These classes are unbundled (they take an instance of has_lift_t R S as a parameter, rather than extending has_lift_t or one of its subclasses) for two reasons:

• We wouldn't have to introduce new classes that handle transitivity (and probably cause diamonds)
• It doesn't matter whether a coercion is written with has_coe or has_lift, you can give it a homomorphism structure in exactly the same way.

Additions

• classes coe_add_hom M N, coe_mul_hom, coe_one_hom, coe_zero_hom state that the coercion map coe : M → N preserves the corresponding operation. They take in a has_lift_t instance so it doesn't matter how precisely the coercion map is defined as long as Lean can find the instance.
• classes coe_monoid_hom M N, coe_add_monoid_hom M N, coe_monoid_with_zero_hom M N, coe_non_unital_ring_hom R S and coe_ring_hom R S are convenient groupings of the above classes
• simp lemmas coe_add, coe_mul, coe_zero, coe_one: basic lemmas stating that coe preserves the corresponding operation.
• simp lemmas coe_pow, coe_nsmul, coe_zpow, coe_zsmul, coe_bit0, coe_bit1, coe_sub, coe_neg: lemmas stating coe preseves the derived structure
• simp lemmas coe_inv, coe_div (for groups), coe_inv₀, coe_div₀ (for groups with zero). An alternative to having this pair of otherwise identical lemmas would be to add coe_inv_hom and coe_div_hom classes.
• class coe_smul_hom M X Y stating that coe : X → Y preseves scalar multiplication by elements of M
• class coe_semilinear_map σ M N stating that coe : M → N is σ-semilinear. coe_linear_map R M N is a synonym of coe_semilinear_map (ring_hom.id R) M N and also gives an instance of coe_smul_hom. I don't think this has any applications yet, it was mostly to test that this design would also work for more complicated classes.
• definitions mul_hom.coe, add_hom.coe, one_hom.coe, zero_hom.coe, monoid_hom.coe, add_monoid_hom.coe, monoid_with_zero_hom.coe, non_unital_ring_hom.coe, ring_hom.coe, semilinear_map.coe and linear_map.coe, given the appropriate coe_hom class, are bundled forms of the coercion map that correspond to the coe_hom classes. In particular ring_hom.coe should become an alternative to algebra_map.
• mul_action_hom.coe, distrib_mul_action_hom.coe and mul_semiring_action_hom.coe are bundled forms of the coercion map corresponding to coe_smul_hom (since they only vary in hypotheses on the non-bundled structure)

Changes

Whenever existing lemmas had a name conflict with the new generic coe_ lemmas, I have made them protected. In many places, the new lemmas are silently used instead of the now protected old lemmas. This caused the vast majority of changed lines. The full list is:

• add_monoid_hom.coe_mul (is about coe_fn)
• linear_map.coe_one and linear_map.coe_mul (are about coe_fn and endomorphisms)
• submodule.coe_zero, submodule.coe_add, submodule.coe_smul (superseded)
• dfinsupp.coe_zero, dfinsupp.coe_add, dfinsupp.coe_nsmul, dfinsupp.coe_neg, dfinsupp.coe_sub, dfinsupp.coe_zsmul, dfinsupp.coe_smul (are about coe_fn)
• finset.coe_one (superseded)
• finsupp.coe_smul, finsupp.coe_zero, finsupp.coe_add, finsupp.coe_neg, finsupp.coe_sub, finsupp.coe_mul (are about coe_fn)
• enat.coe_zero, enat.coe_one, enat.coe_add, enat.coe_sub, enat.coe_mul (superseded except coe_sub)
• nnrat.coe_zero, nnrat.coe_one, nnrat.coe_add, nnrat.coe_mul, nnrat.coe_inv, nnrat.coe_div, nnrat.coe_bit0, nnrat.coe_bit1, nnrat.coe_sub (superseded except coe_sub)
• ereal.coe_zero, ereal.coe_one, ereal.coe_add, ereal.coe_mul, ereal.coe_nsmul, ereal.coe_pow, ereal.coe_bit0, ereal.coe_bit1 (superseded)
• ennreal.coe_zero, ennreal.coe_one, ennreal.coe_add, ennreal.coe_mul, ennreal.coe_bit0, ennreal.coe_bit1, ennreal.coe_pow, ennreal.coe_inv, ennreal.coe_div (superseded)
• equiv.perm.coe_one and equiv.perm.coe_mul (are about coe_fn and endomorphisms)
• submonoid.coe_one, submonoid.coe_mul, submonoid.coe_pow (superseded)
• subsemigroup.coe_mul (superseded)
• special_linear_group.coe_inv, special_linear_group.coe_mul, special_linear_group.coe_pow
• vector_measure.coe_smul, vector_measure.coe_zero, vector_measure.coe_add, vector_measure.coe_neg (are about coe_fn)
• lucas_lehmer.X.coe_mul (superseded)
• power_series.coe_add, power_series.coe_zero, power_series.coe_mul, power_series.coe_one, power_series.coe_bit0, power_series.coe_bit1, power_series.coe_pow (superseded)
• uniform_space.completion.coe_zero, uniform_space.completion.coe_neg, uniform_space.completion.coe_sub, uniform_space.completion.coe_add (superseded)
• continuous_function.coe_mul, continuous_function.coe_one, continuous_function.coe_inv, continuous_function.coe_div continuous_function.coe_pow, continuous_function.coe_zpow (are about `coe_fn)
• bounded_continuous_function.coe_zero, bounded_continuous_function.coe_one, bounded_continuous_function.coe_add, bounded_continuous_function.coe_neg, bounded_continuous_function.coe_sub, bounded_continuous_function.coe_mul, bounded_continuous_function.coe_nsmul, bounded_continuous_function.coe_zsmul, bounded_continuous_function.coe_pow, Many coe_ or cast_ lemmas have been reimplemented using coe_hom classes and are no longer @[simp]. Many homomorphisms subfoo.subtype have been reimplemented by foo_hom.coe. We might consider replacing all of these outright. Finally, some simp calls had to be fixed, e.g. simp [← something.cast_add] could loop due to the new coe_add lemma, so it had to become simp [← something.cast_add, -coe_add].

Further plans

Some obvious further steps that I didn't feel fit in the (already wide) scope of this PR:

• Reviewing for missing instances: currently I only added the obvious instances for the new classes, so we should go through and ensure everything has its instance.
• Reviewing for missing coe lemmas: currently I only added lemmas that existed in the submonoid/subgroup/subring files, so we should go through and ensure everything has its lemma.
• Instances for the transitivity instances coe_trans and lift_trans, so if coe : M → N is a monoid hom and coe : N → O is a monoid hom then coe : M → O is also a monoid hom.
• Classes for when coe_fn is a homomorphism: many of the naming conflicts that required protected are of the form mul_hom.coe_mul : ⇑(f * g) = ⇑f * ⇑g, so the obvious consequence is adding a class coe_fn_mul_hom along these same lines as in this PR.
• Combining with the algebra.to_has_lift_t instance: this is likely to require some subtle fixing so I'd rather merge the big changes first so I don't have to keep those up to date as well.