adjoin_root

Stream: new members

[Damiano Testa]

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]

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

[Johan Commelin]

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

[Damiano Testa]

Great!!

Sure, let me fetch it!

[Damiano Testa]

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,

[Damiano Testa]

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!

[Kenny Lau]

#backticks

[Damiano Testa]

Kenny Lau said:

#backticks

Thanks! I did not know how to do this!

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

Ah, this makes it easier to type it!

[Johan Commelin]

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

[Johan Commelin]

So you might as well just use adjoin_root.mk directly

[Johan Commelin]

Maybe open adjoin_root to just type mk

[Kenny Lau]

@Johan Commelin all comm_rings have has_one...

[Damiano Testa]

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]

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]

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]

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

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.

[Johan Commelin]

Ooh, weird

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Johan Commelin]

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

[Kenny Lau]

it's also called adjoin_root.of f

[Johan Commelin]

Aah, right

[Damiano Testa]

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

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

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]

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

[Damiano Testa]

Also very helpful, thanks!

[Johan Commelin]

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

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]

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

[Damiano Testa]

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]

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]

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]

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]

You should make structures with the

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

syntax

[Damiano Testa]

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

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

[Kenny Lau]

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

[Kevin Buzzard]

I don't know -- post some code?

[Damiano Testa]

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]

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]

https://discord.gg/sZf3r3

[Johan Commelin]

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

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

[Damiano Testa]

Kenny Lau said:

https://discord.gg/sZf3r3

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

[Damiano Testa]

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]

@Damiano Testa let's wait for 5 minutes then

[Damiano Testa]

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!