mathlib

6965ed89 - feat(*): define classes for coercions that are homomorphisms (#17048)

feat(*): define classes for coercions that are homomorphisms (#17048) This PR is part of my [plan to refactor `algebra_map`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60algebra_map.60.20be.20a.20coercion.3F/near/297206409). 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. Co-authored-by: Anne Baanen <t.baanen@vu.nl>