Linear maps and module homomorphisms

Stream: maths

[Johan Commelin]

In algebra/module.lean on line 78 there is structure is_linear_map. I have two questions:
(1) Why is this not a class?
(2) Would it make sense to call this is_module_hom? (For me that would be the 'expected' name.)

[Kevin Buzzard]

maps between algebraic structures are a relatively new thing in Lean and I guess people are still trying to decide whether they should be classes or not. is_group_homwas a definition a few weeks ago and is now a class.

[Johan Commelin]

Ok, that's good to know. To make another comment on terminology: I think it is funny that we write [group G] and [is_group_hom f]. I would expect is_group or group_hom for either of those.

[Johan Commelin]

But I guess this is also due to the organic growth...

[Johan Commelin]

Are proposals to "normalise" such conventions welcome? Or is this already in some pipeline?

[Johan Commelin]

On the other hand, I realise now that there is a real difference between homs and groups

[Johan Commelin]

A group gives you extra data, being a group_hom is merely a property

[Johan Commelin]

This is maybe reflected in the terminology