## Stream: new members

#### 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!

#### Johan Commelin (Aug 17 2020 at 07:58):

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

#### Damiano Testa (Aug 17 2020 at 07:59):

Great!!

Sure, let me fetch it!

#### Damiano Testa (Aug 17 2020 at 08:00):

import data.polynomial.basic
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,


#### 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!

#backticks

#### Damiano Testa (Aug 17 2020 at 08:02):

Kenny Lau said:

#backticks

Thanks! I did not know how to do this!

#### 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 lf : polynomial R →+* Rf := adjoin_root.mk f
end


#### Johan Commelin (Aug 17 2020 at 08:05):

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

#### Damiano Testa (Aug 17 2020 at 08:05):

Ah, this makes it easier to type it!

#### Johan Commelin (Aug 17 2020 at 08:05):

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

#### Johan Commelin (Aug 17 2020 at 08:05):

So you might as well just use adjoin_root.mk directly

#### Johan Commelin (Aug 17 2020 at 08:05):

Maybe open adjoin_root to just type mk

#### Kenny Lau (Aug 17 2020 at 08:06):

@Johan Commelin all comm_rings have has_one...

#### 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!

#### 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.

#### 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.

#### 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.

#### 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.

Ooh, weird

#### 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...

#### 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].

#### Damiano Testa (Aug 17 2020 at 08:10):

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

#### 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!

#### 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.

#### Damiano Testa (Aug 17 2020 at 08:13):

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

#### Johan Commelin (Aug 17 2020 at 08:13):

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

#### Kenny Lau (Aug 17 2020 at 08:14):

it's also called adjoin_root.of f

Aah, right

#### 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)

#### 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)


#### 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!

#### 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

#### 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.

#### 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]


#### Chris Wong (Aug 17 2020 at 08:38):

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

#### 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!

#### 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"

#### 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...

#### 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...

#### Kevin Buzzard (Aug 17 2020 at 08:41):

You should make structures with the

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


syntax

#### 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,...}?

#### 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

#### Kevin Buzzard (Aug 17 2020 at 08:44):

I don't know -- post some code?

#### 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?

#### 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!

#### Kenny Lau (Aug 17 2020 at 08:46):

https://discord.gg/sZf3r3

#### 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)
--                        ^


#### 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:

#### 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...

#### 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!

#### Kenny Lau (Aug 17 2020 at 08:52):

@Damiano Testa let's wait for 5 minutes then

#### 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: Dec 20 2023 at 11:08 UTC