cyclic ring

Stream: Is there code for X?

[Wrenna Robson]

How easy is it to define R[X] / (X^n - 1) for arbitrary rings R and naturals n?

[Kevin Buzzard]

Is R commutative?

[Andrew Yang]

What do you want about it? Is this enough?

example (R : Type*) [ring R] (n : ℕ) := R[X] ⧸ ideal.span ({X ^ n - 1} : set R[X])

[Wrenna Robson]

R is commutative. That looks fairly nice - what I want to do is treat fin n -> R as if it was that (that is to say, transport the addition and multiplication over).

[Eric Rodriguez]

docs#cyclotomic_field for the field case has some fair api

[Gian Cordana Sanjaya]

Wrenna Robson said:

R is commutative. That looks fairly nice - what I want to do is treat fin n -> R as if it was that (that is to say, transport the addition and multiplication over).

Hmm... just out of curiosity, can't we use a group ring, something like R[multiplicative (zmod n)]? Is there a code for group rings?

[Kevin Buzzard]

Yes and yes! Probably they're called monoid algebras or something...

[Riccardo Brasca]

We have docs#monoid_algebra

[Wrenna Robson]

Hmm hmm!

[Junyan Xu]

Wrenna Robson said:

R is commutative. That looks fairly nice - what I want to do is treat fin n -> R as if it was that (that is to say, transport the addition and multiplication over).

Do you really want to transport multiplication over? fin n -> R has the product ring structure with componentwise multiplication, I think.

[Eric Wieser]

add_monoid_algebra R (zmod n) sound like what you want based on the original message

[Junyan Xu]

add_monoid_algebra R (zmod n) sound like what you want based on the original message

Seems great, and the underlying docs#finsupp.to_fun has type defeq to fin n -> R.

[Eric Wieser]

Or if computability is a concern, ⊕ i : zmod n, R (open_locale direct_sum)

[Junyan Xu]

Actually what I said it's not correct. Only when it's add_monoid_algebra R (zmod (n+1)), the type is defeq to fin (n+1) -> R.

[Junyan Xu]

Or if computability is a concern, ⊕ i : zmod n, R (open_locale direct_sum)

That ⊕ needs to be bigger ... \O+
but this doesn't work out of the box:

import algebra.direct_sum.ring
import data.zmod.defs
open_locale direct_sum
example {R n} [comm_ring R] : comm_ring (⨁ i : zmod n, R) := by apply_instance

We need a instance of docs#direct_sum.gcomm_ring for constant A for docs#direct_sum.comm_ring to apply. direct_sum uses dfinsupp, which is more computable finsupp; but I think the correct solution is to make finsupp more computable.

[Eric Wieser]

Oh, that instance is supposed to exist

[Eric Wieser]

docs#comm_semiring.direct_sum_gcomm_semiring already exists, I guess I forgot to add the ring version

[Eric Wieser]

(originally the ring version wasn't needed, but then ring.int_cast appeared and now it is)

[Eric Wieser]

But I agree that a better fix might be to redefine finsupp; I know people keep saying "polynomial being noncomputable is a feature", but I don't see why that means finsupp needs to be noncomputable too

[Wrenna Robson]

So the reason I wanted it on fin n -> R is that I also want the Hamming distance on this thing... but I may have other solutions to that.

[Eric Wieser]

You can cast direct_sum and add_monoid_algebra to a function

[Wrenna Robson]

Aye. Difference being that for Hamming weight the domain has to be finite, wheras that isn't a requirement for a finsupp.

[Wrenna Robson]

What exactly is it about the finsupp construction that makes it non-constructive?

[Eric Wieser]

Sure, but zmod n is finite (n≠0) so that's not relevant here?

[Eric Wieser]

The constructivity is lost in docs#finsupp.has_add which needs to know which coefficients are zero. Rather than requiring decidable_eq on the coefficients which would be annoying, it uses classical decidability

[Eric Wieser]

docs#dfinsupp.has_add uses an approach which does not require knowing which coefficients are zero (by storing the set of elements that might not be zero instead of the ones that are non-zero)

[Wrenna Robson]

Oh, indeed, here it is not relevant.

[Wrenna Robson]

God the finsupp file is massive. It feels like the first step for a refactor is just splitting it up...

[Wrenna Robson]

I was about to ask why has_add needs decidable equality on the coefficients but of course it's because adding it might change the zero set...

[Eric Wieser]

@Yakov Pechersky was also looking at trying such a refactor, it might be good to coordinate

[Wrenna Robson]

It's certainly not something I'd just start without consultation! But if a division of labour is possible I would be interested in helping.