NormedAddGroupHom coercion

Stream: mathlib4

[Jireh Loreaux]

Currently, normed_add_group_hom is a structure which does not extend add_hom or add_monoid_hom, and there is no associated normed_add_group_hom_class. I assume that not extending add_monoid_hom is intentional, because it is proven early and an instance of add_monoid_hom_class is given, although it's not clear why it doesn't extend add_hom (guess: historical accident of development).

However, the problem is that a has_coe_to_fun instance is declared using normed_add_group_hom.to_fun instead of using the fun_like instance. Of course, because coercions are now inlined, this wreaks havoc since we really want the FunLike.coe to appear everywhere. Which of the following should I do while porting:

1. move the AddMonoidHomClass instance up ~70 lines and make the CoeFn instance (re)use the FunLike.coe coercion.
2. follow the morphism refactor and make NormedAddGroupHom a structure which extends AddHom and provide an associated NormedAddGroupHomClass.
3. something else

I assume if I go with (2) it would require a backport, but would it be acceptable to do (1) without backporting? This is what I am leaning towards.

[Floris van Doorn]

There are a bunch of hom-classes (in Lean 4) which have no FunLike instances, or some that have a CoeFun instance in addition to a FunLike instance. I think this happens a couple of times in the order folder, and I feel like we should transition all of them to FunLike instances (without manual CoeFun instances), potentially only after the port.
So I'm for option (1), removing the (second) coercion to functions.
I'd think it's fine without backporting, but it might be safer to backport it.

[Anne Baanen]

I agree precisely with Floris' suggestions. We have reordered/redefined the FunLike instance and removed CoeFun before in the port. Option 2 would quite definitely warrant a backport.

[Jireh Loreaux]

okay, I'll go with that and put a TODO stating we should transition to the new morphism classes.