Zulip Chat Archive

Stream: maths

Topic: semiring homomorphisms

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?

Mario Carneiro (May 08 2018 at 05:41):

You need to preserve zero for a semiring homomorphism

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

Johan Commelin (May 08 2018 at 05:44):

Aah, yes. That is not automatic

Johan Commelin (May 08 2018 at 05:45):

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

Mario Carneiro (May 08 2018 at 05:46):

if you like

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...

Johan Commelin (May 08 2018 at 05:47):

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

Mario Carneiro (May 08 2018 at 05:47):

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

Johan Commelin (May 08 2018 at 05:48):

Ok, I will find some place in that file

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

Mario Carneiro (May 08 2018 at 05:48):

I think this will change in lean 4 though

Johan Commelin (May 08 2018 at 05:50):

Ok

Johan Commelin (May 08 2018 at 05:52):

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

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?

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?

Mario Carneiro (May 08 2018 at 06:10):

let's just say that is a point of discussion

Mario Carneiro (May 08 2018 at 06:10):

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

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

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

Johan Commelin (May 08 2018 at 06:12):

Ok, I see

Johan Commelin (May 08 2018 at 06:13):

Am I correct that parametricity could help here?

Mario Carneiro (May 08 2018 at 06:14):

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

Mario Carneiro (May 08 2018 at 06:14):

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

Last updated: Dec 20 2023 at 11:08 UTC