Zulip Chat Archive

Stream: maths

Topic: Linear maps and module homomorphisms


view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 08 2018 at 11:52):

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

view this post on Zulip Johan Commelin (May 08 2018 at 11:53):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 08 2018 at 11:54):

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

view this post on Zulip Johan Commelin (May 08 2018 at 11:54):

This is maybe reflected in the terminology


Last updated: May 10 2021 at 07:15 UTC