Commit 2021-12-10 13:26 46ac3c41

View on Github →

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).