Zulip Chat Archive

Stream: maths

Topic: semiring homomorphisms


view this post on Zulip Johan Commelin (May 08 2018 at 05:39):

There is a class for ring homomorphisms: https://github.com/leanprover/mathlib/blob/7d1ab388bb097db5d631d11892e8f110e1f2e9cd/algebra/ring.lean#L60
But there is no class for semiring homomorphisms. Does it make sense to change broaden this class into semiring homomorphisms?

view this post on Zulip Mario Carneiro (May 08 2018 at 05:41):

You need to preserve zero for a semiring homomorphism

view this post on Zulip Mario Carneiro (May 08 2018 at 05:41):

in fact, I guess it's just the same as a monoid homomorphism which is also an additive monoid homo

view this post on Zulip Johan Commelin (May 08 2018 at 05:44):

Aah, yes. That is not automatic

view this post on Zulip Johan Commelin (May 08 2018 at 05:45):

Ok, so, shall I add a new class for semiring homs?

view this post on Zulip Mario Carneiro (May 08 2018 at 05:46):

if you like

view this post on Zulip Johan Commelin (May 08 2018 at 05:47):

What is a natural place for it? I am a bit surprised that the definition of a semiring is in core...

view this post on Zulip Johan Commelin (May 08 2018 at 05:47):

Otherwise it would be natural to add it after the definition of semiring

view this post on Zulip Mario Carneiro (May 08 2018 at 05:47):

the mathlib file for ring-like stuff is algebra/ring.lean

view this post on Zulip Johan Commelin (May 08 2018 at 05:48):

Ok, I will find some place in that file

view this post on Zulip Mario Carneiro (May 08 2018 at 05:48):

semiring is defined in core because nat is a semiring and that defines all the operations on nat

view this post on Zulip Mario Carneiro (May 08 2018 at 05:48):

I think this will change in lean 4 though

view this post on Zulip Johan Commelin (May 08 2018 at 05:50):

Ok

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

Aah, and it seems like monoid_homs are also not yet there

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

Does this have anything to do with the "algebraic hierarchy" that I sometimes hear people talking about?

view this post on Zulip Johan Commelin (May 08 2018 at 06:09):

At the moment there is a class for homomorphisms between two groups but if one (or both) of my groups are additive, there is no class for homomorphisms. Does this mean we need 4 classes to cover all the possibilities?

view this post on Zulip Mario Carneiro (May 08 2018 at 06:10):

let's just say that is a point of discussion

view this post on Zulip Mario Carneiro (May 08 2018 at 06:10):

One option is to use multiplicative to interpret an additive group as a multiplicative group

view this post on Zulip Mario Carneiro (May 08 2018 at 06:11):

We have not made any significant effort to have a full complement of morphisms between the various available structures in mathlib

view this post on Zulip Mario Carneiro (May 08 2018 at 06:12):

the ones that exist have basically been added ad-hoc as people needed them, and I'm fine with that

view this post on Zulip Johan Commelin (May 08 2018 at 06:12):

Ok, I see

view this post on Zulip Johan Commelin (May 08 2018 at 06:13):

Am I correct that parametricity could help here?

view this post on Zulip Mario Carneiro (May 08 2018 at 06:14):

Well, transport_to_additive can be seen as a special case of parametricity

view this post on Zulip Mario Carneiro (May 08 2018 at 06:14):

but there is also a lot of renaming to be done by the tactic


Last updated: May 10 2021 at 07:15 UTC