## Stream: maths

### Topic: Linear maps and module homomorphisms

#### Johan Commelin (May 08 2018 at 11:42):

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 (May 08 2018 at 11:50):

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 (May 08 2018 at 11:52):

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 (May 08 2018 at 11:52):

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

#### Johan Commelin (May 08 2018 at 11:53):

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

#### Johan Commelin (May 08 2018 at 11:53):

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

#### Johan Commelin (May 08 2018 at 11:54):

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

#### Johan Commelin (May 08 2018 at 11:54):

This is maybe reflected in the terminology

Last updated: May 10 2021 at 07:15 UTC