semiring polynomials

Stream: maths

[Chris Hughes]

Do we want polynomials over a semiring? If we do, then it's really necessary to have a way of expressing zero_ne_one as a class for semirings. I'm trying to prove some lemmas now for semirings, not because I care about semirings, but they are true in a semiring so I may as well prove it. It's very hard without degree_X.

[Chris Hughes]

I propose

class zero_ne_one_class' {α : Type*} [has_zero α] [has_one α] :=
(zero_ne_one : (0 : α) ≠ 1)

[Kevin Buzzard]

Part of me wants to say "I see $\mathbb{N}[X]$ occasionally" and part of me wants to say "I have been a mathematician for 30 years and had never once heard of the concept of a semiring before I came here". However the same applies to uniform spaces.

[Johan Commelin]

I think toric geometers would like to see them. Is that right?

[Kevin Buzzard]

Maybe that's exactly where I saw N[X]

[Kevin Buzzard]

I have a totally ordered abelian group under * and I've been adding a bottom element 0 to it. That's another example of a structure with 0 and a 1, although in that case 0 ne 1 is guaranteed. I can't offhand think of anything else with a 0 and a 1 that isn't a semiring

[Mario Carneiro]

I'm not sure what the issue is. Is zero_ne_one_class only defined for rings or something?

[Mario Carneiro]

The proposal seems very reasonable (provided it is put in Prop instead of Type)

[Kevin Buzzard]

I had guessed that was the issue, from the context, but I might be wrong

[Mario Carneiro]

Do we have the submodules degree t <= n? Last time we talked about this it seemed like this was the way to go - it's much nicer constructively and you don't have to do all this cases stuff

[Kevin Buzzard]

+1 for those submodules -- they can be used to give a really nice proof of Hilbert Basis. I assume this is the proof Kenny used.

[Kevin Buzzard]

You avoid having to assume that the ring is not the zero ring.

[Kevin Buzzard]

Multiplication by X is a map from deg<=n to deg<=n+1 whether or not the degree of X is 1

[Neil Strickland]

In stable homotopy theory we definitely want to deal with semirings, such as the Burnside semiring or the representation semiring of a finite group.

[Scott Morrison]

We have a student here at ANU who does Galois theory for semirings...

[Scott Morrison]

And studying fusion categories it's nice to think of the Grothendieck ring as a (based) semiring.

[Reid Barton]

Do we want polynomials over a semiring? If we do, then it's really necessary to have a way of expressing zero_ne_one as a class for semirings. I'm trying to prove some lemmas now for semirings, not because I care about semirings, but they are true in a semiring so I may as well prove it. It's very hard without degree_X.

What makes this different for rings and semirings?

[Reid Barton]

I see zero_ne_one_class extends has_zero and has_one--I don't understand how that doesn't make nonzero rings really awkward to work with

[Reid Barton]

or does class nonzero_comm_ring (α : Type*) extends zero_ne_one_class α, comm_ring α merge the common fields?

[Chris Hughes]

extends does merge the common fields.

[Kenny Lau]

as long as you have some old structure command or whatnot

[Reid Barton]

Then we could also make a parallel nonzero_comm_semiring right?

[Chris Hughes]

Yes,but maybe we want an ordered nonzero semiring or something like that. There's too many combinations.

[Kevin Buzzard]

Will Lean 4 abandon the old structure command so I can finally understand what one can and can't do with structures and then be able to rant about how they're not fit for purpose when doing mathematics?