[Merged by Bors] - feat(*): introduce classes for types of homomorphism

[Vierkantor]

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 refactor(*): backport coe_fn from Lean 4 #7033)
• Define a class fun_like, analogous to set_like, for types of bundled function + proof (done in [Merged by Bors] - feat(data): define a fun_like class of bundled homs (function + proofs) #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
• bundling morphisms #1044
• Avoid restating multiplicatively many foo_hom.map_bar #4985

---

• depends on: [Merged by Bors] - feat(data): define a fun_like class of bundled homs (function + proofs) #10286
• depends on: [Merged by Bors] - chore(*): protect to_fun and map_{add,zero,mul,one,div} #10580

[urkud]

Would it be hard to split fun_like from the diff? If not, could you please PR it separately so that we can have it before the whole PR passes the review? If it's hard, then ignore this comment.

[Vierkantor]

Sure, I can just copy the commit introducing fun_like.lean to its own PR.

[eric-wieser]

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.

This might be worth splitting into a separate PR, if doing so is easy and this hits lots of otherwise untouched files.

[eric-wieser]

Would it be better here to go straight to adding a ring_hom_class? Or would you argue there is no point in such a class, and using these two classes separately is easier?

[Vierkantor]

With the current design we'd need a separate ring_hom_class, since taking the add_monoid_hom_class and monoid_hom_class in separate parameters can have different to_funs.

An alternative is to unbundle the fun_like from the _hom_classes, taking it as an instance parameter rather than extending it:

class zero_hom_class (F : Type*) (M N : out_param $ Type*) [fun_like F M (λ _, N)]
  [has_zero M] [has_zero N] :=
(map_zero : ∀ (f : F), f 0 = 0)

Then we wouldn't need to define the conjunction of the _hom_classes separately, just one per operation. The disadvantage being that the list of instance parameters becomes extremely long:

theorem polynomial.hom_eval₂ {R S T : Type*} [semiring R] (p : polynomial R)
  [comm_semiring S] [comm_semiring T]
  (f : R →+* S) (g : S →+* T) (x : S) :
  ⇑g (polynomial.eval₂ f x p) = polynomial.eval₂ (g.comp f) (⇑g x) p

becomes

theorem polynomial.hom_eval₂ {R S T F G : Type*} [semiring R] (p : polynomial R)
  [comm_semiring S] [comm_semiring T]
  [fun_like F R (λ _, S)] [add_hom_class F R S] [mul_hom_class F R S] [one_hom_class F R S] [zero_hom_class F R S]
  [fun_like G S (λ _, T)] [add_hom_class G S T] [mul_hom_class G S T] [one_hom_class G S T] [zero_hom_class G S T]
  (f : F) (g : G) (x : S) :
  ⇑g (polynomial.eval₂ f x p) = polynomial.eval₂ (g.comp f) (⇑g x) p

instead of my preferred bundled design:

theorem polynomial.hom_eval₂ {R S T F G : Type*} [semiring R] (p : polynomial R)
  [comm_semiring S] [comm_semiring T] [ring_hom_class F R S] [ring_hom_class G S T]
  (f : F) (g : G) (x : S) :
  ⇑g (polynomial.eval₂ f x p) = polynomial.eval₂ (g.comp f) (⇑g x) p

[eric-wieser]

Note that if we just want to shrink the argument list, we can still have a vestigial ring_hom_class that extends the others and use [fun_like G S (λ _, T)] [ring_hom_class G S T]; which maybe has an advantage since there are no longer any diamonds in the data-carrying classes. I think your design is fine though.

In that case, can you replace these two instances with class ring_hom_class extends ... and a single instance : ring_hom_class?

[Vierkantor]

Indeed, I think we'll end up having to unbundle parts of the linear/mul_action hom classes anyway: if it was a subclass of fun_like we'd get a dangerous instance linear_map_class F σ M N → fun_like F M N. But since they're also add_homs, the class would look something more like:

class linear_map_class (F : Type*) {R S : Type*} [semiring R] [semiring S] (σ : R →+* S) (M M₂ : Type*)
  [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module S M₂]
  [add_hom_class F M M₂] := -- alternatively [fun_like F M (λ _, M₂)] [add_hom_class F M M₂] :=
(map_smul' : ∀ (f : F) (r : R) (x : M), f (r • x) = (σ r) • f x)

so unbundling fun_like from the add_hom_class doesn't really bring anything in that case.

[Vierkantor]

I've added a commit defining a ring_hom_class. I expect nothing will break, let's see :P

[Vierkantor]

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.

This might be worth splitting into a separate PR, if doing so is easy and this hits lots of otherwise untouched files.

I'm currently compiling a branch (edit: #10580) with commits d0a17c6 and c4a31b2 cherry-picked. Let's see how much manual fixing it needs...

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(data): define a fun_like class of bundled homs (function + proofs) #10286
• [Merged by Bors] - chore(*): protect to_fun and map_{add,zero,mul,one,div} #10580

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[sgouezel]

I absolutely love this idea. Two questions:

• could you explain this design idea somewhere (probably in some library note -- then one could refer to it when defining one of these helper classes)? Mentioning in particular the O(n * k) against O(n) + O(k) issue
• in the current version, it is rather O(n * k) + O(n) + O(k), as you don't remove any of the preexisting lemmas. Is that in your plans later?

[Vierkantor]

• in the current version, it is rather O(n * k) + O(n) + O(k), as you don't remove any of the preexisting lemmas. Is that in your plans later?

Yes, I tried doing all of this in one go and it extremely quickly got out of hand. So this will happen in a number of separate follow-ups.

[Vierkantor]

could you explain this design idea somewhere (probably in some library note -- then one could refer to it when defining one of these helper classes)? Mentioning in particular the O(n * k) against O(n) + O(k) issue

Almost forgot to respond to this one. I wrote this in the module documentation for fun_like, would you like to have this instead as a library note named something like "morphism classes"?

[jcommelin]

Thanks 🎉

bors merge

[jcommelin]

Should this now in fact be proven for mul_hom_class? Because that's all you need. (Shouldn't hold up this PR. Can be done later.)

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests