ring_hom

Stream: maths

[Kevin Buzzard]

Whilst making a MWE for this I noticed that we have

structure ring_hom (α : Type*) (β : Type*) [semiring α] [semiring β]
  extends monoid_hom α β, add_monoid_hom α β, monoid_with_zero_hom α β

However monoid_with_zero_hom is defined to extend zero_hom M N (part of add_monoid_hom) and monoid_hom M N, and adds no new fields, so we don't need it at all from a maths point of view. Is there a reason it's there anyway?

[Eric Wieser]

I thought I wrote down why I did this at docs#ring_hom

[Eric Wieser]

From that link:

This extends from both monoid_hom and monoid_with_zero_hom in order to put the fields in a
sensible order, even though monoid_with_zero_hom already extends monoid_hom.

[Kevin Buzzard]

you're justifying why you extend monoid_hom, I was asking the other way around, but either way I don't ubderstand your answer -- surely the sensible order starts with 0?

[Eric Wieser]

If you had extends monoid_with_zero_hom α β, add_monoid_hom α β then the order would be zero, one, mul, add

[Eric Wieser]

Oh, it's so you get ring_hom.to_monoid_with_zero_hom for free

[Eric Wieser]

You're right, I was answering a different question.

[Kevin Buzzard]

The order I learnt them was zero, one, add, mul, which is closer to this than what we have right now ;-) OK so it's just a field order thing? All this is going to have to be refactored before the Lean 4 port anyway, right, because old structures are evil?

[Kevin Buzzard]

Eric Wieser said:

Oh, it's so you get ring_hom.to_monoid_with_zero_hom for free

This was what I was wondering about.

[Eric Wieser]

I think there might be bits of mathlib that rely on the field order, and I didn't want to have to touch them when I added monoid_with_zero_hom

[Kevin Buzzard]

Yes that sounds believable, sometimes people just make complex structures by listing the fields in \< \>

[Kevin Buzzard]

given that elab_as_eliminator is gone and now it's much harder to use recursors directly, one gets the impression that the devs are suggesting that listing the fields is supposed to be idiomatic nowadays (even on a split of an or)

[Eric Wieser]

Either it would need refactoring for lean 4, or we add some meta code to add back old structures. Using new structures sounds like it matters more for typeclass inference

[Eric Wieser]

I think field order is unavoidably public whatever you do; ring_hom.mk is probably not going away