Zulip Chat Archive

Stream: new members

Topic: adjoin_root


view this post on Zulip Damiano Testa (Aug 17 2020 at 07:57):

Dear All,

I am trying to use the command adjoin_root. Given a polynomial f in one variable over the commutative ring R with 1, I see from the documentation that it is possible to extract lots of data from adjoin_root (f). For instance, I would like to retrieve

  1. the hypothesis that R[x]/(f) is a commutative ring with 1,
  2. the canonical map lf : R --> R[x]/(f),
  3. the hypothesis that lf is a ring homomorphism,
    ...

I understand that the documentation is saying how to access this information, but I am new to Lean and I do not know how to extract this info. Could anyone help me, please?

Thank you very much!

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:58):

@Damiano Testa Sure, we can make that work (-;

view this post on Zulip Johan Commelin (Aug 17 2020 at 07:58):

Do you already have a bit of code to start with?

view this post on Zulip Damiano Testa (Aug 17 2020 at 07:59):

Great!!

Sure, let me fetch it!

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:00):

import data.polynomial.basic
import ring_theory.adjoin_root
import tactic

open set classical ring monoid

class univ_loc_f (R : Type) [comm_ring R] [has_one R] (f : R) :=
    (Rf : Type)
    (ring : comm_ring Rf)
    (has1 : has_one Rf)
    (lf : R  Rf)
    (lfh : is_ring_hom lf)
    (inve : is_unit (lf f))
    (vers :  (S : Type) [comm_ring S] [has_one S] ,
         (h : R  S) [is_ring_hom h] [is_unit (h f)] ,
         (fac : Rf  S) [is_ring_hom fac] ,  r : R , h r = fac (lf r))
    (uni :  (S : Type) [comm_ring S] [has_one S] ,
         (h : R  S) [is_ring_hom h] [is_unit (h f)] ,
         (fac1 fac2 : Rf  S) [is_ring_hom fac1] [is_ring_hom fac2] ,  r : R , h r = fac1 (lf r)  h r = fac2 (lf r)  fac1=fac2)


def loc_f (R : Type) [comm_ring R] [has_one R] (f : R) : univ_loc_f R f :=
begin
    let fx := polynomial.monomial 1 f,
    let fx1 : polynomial R := fx-1,
    let Rf := adjoin_root fx1,

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:01):

at this stage in the definition loc_f, I would like to start introducing the hypothesis to check that indeed a localization in the sense above exists. But I am stuck!

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:01):

#backticks

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:02):

Kenny Lau said:

#backticks

Thanks! I did not know how to do this!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:04):

open polynomial -- jmc added this

def loc_f (R : Type) [comm_ring R] [has_one R] (f : R) : univ_loc_f R f :=
begin
  let f : polynomial R := X - 1,
  let Rf := adjoin_root f,
  let lf : polynomial R →+* Rf := adjoin_root.mk f
end

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:05):

Because of open polynomial you can simply write X for the polynomial variable

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:05):

Ah, this makes it easier to type it!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:05):

lf is the canonical map, and it is already a ring hom

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:05):

So you might as well just use adjoin_root.mk directly

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:05):

Maybe open adjoin_root to just type mk

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:06):

@Johan Commelin all comm_rings have has_one...

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:06):

Ok, I am going to try it now and see if I can now finish the proof and figure out all the remaining hypotheses!

Thank you very much!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:07):

Ooh, it would be mk f not just mk... you have to remind it about the polynomial of which you are adjoining a root. So maybe the let is not so bad.

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:08):

thanks! I prefer to have the names of all the data that I introduce as hypotheses, so that I can reuse them as I need to.

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:08):

@Damiano Testa, Kenny raised an important point. (I hadn't looked at your code closely.)
If you write [comm_ring R] [has_one R], then R will end up having two elements called 1. The first comes from comm_ring (because in mathlib all rings are unital) and the other from has_one. And you can't prove that they will be the same or different, because nothing relates the two.

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:09):

Ah, I see! I had added this, since at some other time, after stating that something was a commutative ring, then I had an error saying that 1 was missing in a commutative ring.

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:10):

Ooh, weird

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:10):

This might very well have been a mistake on my part, in that I did not know how to use the 1 in the ring, even if it already was there...

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:10):

Also, you are encouraged to use R →+* S for ring homs, instead of [is_ring_hom f].

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:10):

I will remove it and see how far I can go along

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:11):

Johan Commelin said:

Also, you are encouraged to use R →+* S for ring homs, instead of [is_ring_hom f].

I am glad to use this notation: I had no idea that it existed!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:13):

@Damiano Testa Oops, adjoin_root.mk f is the quotient map from polynomial R, not the "inclusion" R →+* Rf.

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:13):

Yes, I was going to try to fix this! Ahahaha

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:13):

let lf : R →+* Rf := algebra_map R Rf

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:14):

it's also called adjoin_root.of f

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:14):

Aah, right

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:15):

(Also, in my code, f is not the polynomial whose root I was to extract, but rather is the polynomial f*x-1. Which means that I also do not know how to multiply f in R with X in polynomial R)

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:17):

@Damiano Testa I think I would use the following structure definition:

structure univ_loc_f (R : Type) [comm_ring R] (f : R) :=
(Rf : Type)
[ring : comm_ring Rf]
(lf : R →+* Rf)
(inve : is_unit (lf f))
(vers :  (S : Type) [comm_ring S],
   (h : R →+* S) (hf : is_unit (h f)),
   (fac : Rf →+* S),  r : R , h r = fac (lf r))
(uni :  (S : Type) [comm_ring S],
   (h : R →+* S) (hf : is_unit (h f)),
   (fac1 fac2 : Rf →+* S),  r : R , h r = fac1 (lf r)  h r = fac2 (lf r)  fac1 = fac2)

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:18):

Thank you! You are much faster than I am: I was exactly going through a similar process!

I will continue with my own version and in the end, I will check it against your solution: proceeding in this way, I feel that I learn more!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:19):

Damiano Testa said:

(Also, in my code, f is not the polynomial whose root I was to extract, but rather is the polynomial f*x-1. Which means that I also do not know how to multiply f in R with X in polynomial R)

polynomial.C is the ring hom that maps r : R to the constant polynomial C r

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:20):

Also very helpful, thanks!

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:34):

@Damiano Testa I've found a mistake on the final line of the structure definition. But I'll keep my mouth shut in case you want to figure it out yourself.

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:36):

I will try to find the mistake. For the moment, I have a question: why did you change the parenthesis in hypothesis ring from round to square?

(Rf : Type)```
was
```(ring : comm_ring Rf)```
you changed it to
```[ring : comm_ring Rf]```

view this post on Zulip Chris Wong (Aug 17 2020 at 08:38):

The [] means type class resolution, i.e. Lean will find a comm_ring automatically

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:39):

Chris Wong said:

The [] means type class resolution, i.e. Lean will find a comm_ring automatically

Ah, how convenient! Thanks! One fewer hypothesis to prove!

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 08:39):

comm_ring is a typeclass so we use square brackets to let Lean deal with it -- the square bracket system, a.k.a. the type class inference system, then deals with all the fiddly theorems of the form "a commutative ring is an abelian group under addition so this lemma proved for abelian groups also holds for rings"

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:40):

Ok, I changed the round brackets to square brackets, but now I can no longer use the fconstructor command to introduce the various bits of the structure...

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:41):

Johan Commelin said:

Damiano Testa I've found a mistake on the final line of the structure definition. But I'll keep my mouth shut in case you want to figure it out yourself.

I could not find the mistake, but I have a bad feeling about the equal sign in fac1=fac2...

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 08:41):

You should make structures with the

{ field1 := value1,
  field2 := value2,
  ... }

syntax

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:43):

Ok, so this means that I introduce everything and at the end I type

exact { field1 := value1,...}?

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:44):

@Damiano Testa if you could join the discord server maybe I can livestream how to fix your code

view this post on Zulip Kevin Buzzard (Aug 17 2020 at 08:44):

I don't know -- post some code?

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:45):

Kenny Lau said:

Damiano Testa if you could join the discord server maybe I can livestream how to fix your code

Happy to do this, but what is the discord server?

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:46):

Kevin Buzzard said:

I don't know -- post some code?

I will give it a shot and I will get back, in case I fail!

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:46):

https://discord.gg/sZf3r3

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:50):

@Damiano Testa The mistake is that you are missing parentheses:

   (fac1 fac2 : Rf →+* S), ( r : R , h r = fac1 (lf r)  h r = fac2 (lf r))  fac1 = fac2)
  --                        ^

view this post on Zulip Johan Commelin (Aug 17 2020 at 08:51):

Without them, you would have to prove the implication for all r, which isn't what you want :smiley:

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:52):

Kenny Lau said:

https://discord.gg/sZf3r3

My account needs to be 5 mins old to be able to post...

view this post on Zulip Damiano Testa (Aug 17 2020 at 08:52):

Johan Commelin said:

Without them, you would have to prove the implication for all r, which isn't what you want :smiley:

Ah, thanks for catching this!

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:52):

@Damiano Testa let's wait for 5 minutes then

view this post on Zulip Damiano Testa (Aug 17 2020 at 09:43):

Kevin Buzzard said:

I don't know -- post some code?

Dear Kevin,

thank you for your offer! I had a chat with Kenny Lau and he cleared a lot of doubts that I had! I will try to make some further progress and will get back to the chat, once I have been stuck for a while!

Thank you all for your help!


Last updated: May 09 2021 at 20:11 UTC