# Zulip Chat Archive

## Stream: maths

### Topic: semiring polynomials

#### Chris Hughes (Feb 10 2019 at 23:12):

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 (Feb 11 2019 at 00:25):

I propose

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

#### Kevin Buzzard (Feb 11 2019 at 07:41):

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 (Feb 11 2019 at 07:48):

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

#### Kevin Buzzard (Feb 11 2019 at 07:50):

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

#### Kevin Buzzard (Feb 11 2019 at 07:52):

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 (Feb 11 2019 at 08:06):

I'm not sure what the issue is. Is `zero_ne_one_class`

only defined for `ring`

s or something?

#### Mario Carneiro (Feb 11 2019 at 08:07):

The proposal seems very reasonable (provided it is put in `Prop`

instead of `Type`

)

#### Kevin Buzzard (Feb 11 2019 at 08:08):

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

#### Mario Carneiro (Feb 11 2019 at 08:09):

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 (Feb 11 2019 at 08:18):

+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 (Feb 11 2019 at 08:18):

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

#### Kevin Buzzard (Feb 11 2019 at 08:18):

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

#### Neil Strickland (Feb 11 2019 at 09:44):

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 (Feb 11 2019 at 21:01):

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

#### Scott Morrison (Feb 11 2019 at 21:02):

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

#### Reid Barton (Feb 12 2019 at 01:21):

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 (Feb 12 2019 at 01:23):

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 (Feb 12 2019 at 01:25):

or does `class nonzero_comm_ring (α : Type*) extends zero_ne_one_class α, comm_ring α`

merge the common fields?

#### Chris Hughes (Feb 12 2019 at 01:51):

`extends`

does merge the common fields.

#### Kenny Lau (Feb 12 2019 at 02:03):

as long as you have some old structure command or whatnot

#### Reid Barton (Feb 12 2019 at 03:47):

Then we could also make a parallel `nonzero_comm_semiring`

right?

#### Chris Hughes (Feb 12 2019 at 07:02):

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

#### Kevin Buzzard (Feb 12 2019 at 07:30):

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?

Last updated: May 06 2021 at 18:20 UTC