Zulip Chat Archive

Stream: Is there code for X?

Topic: char_zero instance on polynomials

Damiano Testa (Mar 31 2022 at 13:58):

Dear All,

I cannot find a char_zero instance on R[X], when R itself has char_zero. Is the instance below somewhere, and I simply cannot find it?

Note: this is similar to what happened here, except that there I was asking for char_p.

Thanks!

import ring_theory.polynomial.basic

open_locale polynomial
open polynomial char_p

instance polynomial.char_p' {R : Type*} [semiring R] [char_zero R] : char_p R[X] 0 :=
by apply_instance  --works and finds `polynomial.char_p 0`.

instance polynomial.char_zero {R : Type*} [semiring R] [char_zero R] : char_zero R[X] :=
{ cast_injective := λ x y, nat_cast_inj.mp }

Yaël Dillies (Mar 31 2022 at 14:01):

If you have a look at the instance list at docs#char_zero, you can check that it is indeed missing.

Damiano Testa (Mar 31 2022 at 14:02):

Ok, thanks for confirming! As I have been so unsuccessful at finding existing lemmas/instances, I was worried that I might have missed it.

Damiano Testa (Mar 31 2022 at 14:02):

I will PR it, then!

Damiano Testa (Mar 31 2022 at 14:06):

#13075

Riccardo Brasca (Mar 31 2022 at 14:06):

I am sure it is already there

Riccardo Brasca (Mar 31 2022 at 14:06):

Let me see

Riccardo Brasca (Mar 31 2022 at 14:07):

docs#polynomial.char_p and docs#char_p.char_p_to_char_zero

Damiano Testa (Mar 31 2022 at 14:07):

I tried this, but docs#char_p.char_p_to_char_zero wants a ring.

Riccardo Brasca (Mar 31 2022 at 14:08):

Mmh, I see, and also docs#char_p.char_p_to_char_zero is not an instance

Damiano Testa (Mar 31 2022 at 14:09):

Yes, I think there would be a loop char_p R 0 -> char_zero R -> char_p R 0 -> ....

Damiano Testa (Mar 31 2022 at 14:09):

But here I think that this is safe: R[X] inherits char_zero from R, so the "complexity" increases, right?

Riccardo Brasca (Mar 31 2022 at 14:09):

Well, modifying [ring R] to [semiring R] just before docs#char_p.char_p_to_char_zero didn't break anything, so we at least want it

Riccardo Brasca (Mar 31 2022 at 14:10):

Can you add it to your PR?

Damiano Testa (Mar 31 2022 at 14:10):

Sure!

Riccardo Brasca (Mar 31 2022 at 14:11):

Even non_assoc_semiring R works

Riccardo Brasca (Mar 31 2022 at 14:12):

I don't remember how far we went about this kind of generality :D

Damiano Testa (Mar 31 2022 at 14:12):

hmmm, it does break:

lemma char_p_to_char_zero {R : Type*} [semiring R] [char_p R 0] : char_zero R :=
char_zero_of_inj_zero $
  λ n h0, eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)

char_zero_of_inj_zero wants cancel something

Riccardo Brasca (Mar 31 2022 at 14:13):

Ah sorry, my VS code is too slow

Damiano Testa (Mar 31 2022 at 14:13):

This is the error, in case you are wondering:

Error

Damiano Testa (Mar 31 2022 at 14:14):

Ok, so I will not include this in the PR. :stuck_out_tongue_wink:

Riccardo Brasca (Mar 31 2022 at 14:18):

Ah, I see the difference. For semirings the two may be really different

Damiano Testa (Mar 31 2022 at 14:21):

Yes, if the successor function looks like 0 -> 1 -> 1 -> 1..., then nat.cast is not injective, but no positive multiple of 1 is zero.

Damiano Testa (Mar 31 2022 at 14:21):

(I guess this semiring used to be called, maybe still is called, fin 1).

Reid Barton (Mar 31 2022 at 14:24):

Instead what you should add to the PR is a big warning that char_p 0 is not the same as char_zero

Damiano Testa (Mar 31 2022 at 14:25):

Sure! Maybe even the example above, showing that the two notions can be different.

Damiano Testa (Mar 31 2022 at 14:43):

Ok, I updated the two doc-strings for char_zero and char_p. Feel free to suggest comments!

Yakov Pechersky (Mar 31 2022 at 14:55):

(deleted)

Yakov Pechersky (Mar 31 2022 at 14:56):

(deleted)

Yakov Pechersky (Mar 31 2022 at 14:56):

(deleted)

Yakov Pechersky (Mar 31 2022 at 14:58):

(deleted)

Yakov Pechersky (Mar 31 2022 at 14:59):

I don't think we ever defined semirings with saturating addition.

Damiano Testa (Mar 31 2022 at 15:03):

Ok, I was simply saying "use 0,1{0,1} and define addition by requiring 00 to be 00, and 1+1=11 + 1 = 1". Everything else follows and for this add_monoid/semiring, the two notions of characteristic disagree.

If you want to comment on the warning that I wrote in the PR, I'm happy to take suggestions!

Damiano Testa (Mar 31 2022 at 15:55):

I went ahead and formalized the example above: #13080.

Last updated: Dec 20 2023 at 11:08 UTC