Zulip Chat Archive

Stream: kbb

Topic: splitting fields


view this post on Zulip Johan Commelin (Sep 14 2018 at 17:28):

It would be great if we could push the splitting fields branch to the point where we can define the Galois group of a splitting field.

view this post on Zulip Johan Commelin (Sep 14 2018 at 17:29):

So far we can adjoint the root of an irreducible polynomial. There is a sorryd statement of the universal property of adjoining a root.

view this post on Zulip Johan Commelin (Sep 14 2018 at 17:29):

Ooh, the branch I'm talking about is not in this repo, but in the community mathlib.

view this post on Zulip Johan Commelin (Sep 14 2018 at 17:31):

If we combine this with the stuff on Hecke operators, then we'll have the formal abstract of Kevin's paper (modulo one fact that requires a Mjölnir to prove).

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:12):

Little hole in the quotient ring api. I'll leave it to others to :golf:

def quotient_ring.lift {α : Type u} {β : Type v} [comm_ring α] [comm_ring β]
(S : set α) [is_ideal S] (f : α  β) [is_ring_hom f] (H :  {a}, a  S  f a = 0) :
quotient_ring.quotient S  β :=
begin
  refine @quotient.lift _ _ (quotient_ring.quotient_rel S) f _,
  intros a b h,
  apply eq_of_sub_eq_zero,
  rw is_submodule.quotient_rel_eq at h,
  simpa only [is_ring_hom.map_sub f] using H h,
end

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:29):

Here is adjoin_root.lift:

def lift {L} [discrete_field L] (i : K  L) [is_field_hom i]
  (x : L) (h : f.eval₂ i x = 0) : (adjoin_root f)  L :=
begin
  refine @quotient_ring.lift _ _ _ _
    (@span _ _ _ ring.to_module ({f} : set (polynomial K))) (is_ideal.span _)
    (eval₂ i x) _ _,
  intros g H,
  simp [span_singleton] at H,
  cases H with y H,
  dsimp at H,
  rw [ H, eval₂_mul],
  simp [h],
end

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:29):

Which can undoubtly be golfed

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:30):

@Mario Carneiro I think the next step was some really crazy inductive proof, right?

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:31):

yes

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:31):

the next step is the splitting field for one polynomial

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:33):

Do we know that every polynomial over a field has an irreducible factor?

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:35):

I think so

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:35):

We know that polynomial K is a PID

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:35):

and every PID is a UFD

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:35):

I think that latter fact is now also in mathlib

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:35):

we have UFDs?

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:36):

Hmm, I guess there is a standard lemma on lift_mk or something?

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:36):

We'll also need that.

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:36):

yes

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:36):

Yes, Johannes added UFD's after Orsay

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:36):

So we need this lift_mk for quotient rings, and then for adjoin root.

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:36):

the fact you want about lift is composition with the coercion from K, and value at the root

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:38):

is the proof constructive? (i.e. is there a function from a polynomial to its smallest irreducible factor or something)

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:38):

Not only stuff from K, right? Also K[X]

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:38):

Hmm, factoring is hard.

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:38):

that isn't needed, it follows by homness

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:39):

???

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:39):

but I guess the quotient map is equal to the eval map, we want to know that

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:40):

oh, you didn't prove lift is a field hom

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:40):

we definitely need that

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:43):

I didn't even prove it is a ring hom

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:44):

Working on that now

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:44):

I think those are the same

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:49):

@Mario Carneiro I need some help to get the right statements for these API things: this is in the quotient_ring namespace:

def lift (S : set α) [is_ideal S] (f : α  β) [is_ring_hom f] (H :  (a : α), a  S  f a = 0) :
quotient_ring.quotient S  β :=
begin
  refine @quotient.lift _ _ (quotient_ring.quotient_rel S) f _,
  intros a b h,
  apply eq_of_sub_eq_zero,
  rw is_submodule.quotient_rel_eq at h,
  simpa only [is_ring_hom.map_sub f] using H _ h,
end

lemma lift_mk {S : set α} [is_ideal S] {f : α  β} [is_ring_hom f] {H :  (a : α), a  S  f a = 0} {a : α} :
lift S f H a = f a :=
begin

end

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:49):

Should the latter be a simp-lemma?

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:49):

At the moment the ⟦a⟧ notation is broken.

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:50):

This is my first time working with quotients in Lean...

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:50):

I forget the details but I don't think ⟦⟧ is part of the interface

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:51):

The only "public" functions are the map from K, and the root element

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:52):

No, I'm working on quotient rings at the moment.

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:52):

Splitting field will come later.

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:52):

We don't even have lift for quotient rings at the moment.

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:53):

I guess we want that notation for general quotient rings, right?

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:53):

ah okay

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:53):

you want to redefine mk for that

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:54):

that way you can give it the right type and find it with typeclass inference

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:54):

when you prove it is a ring hom

view this post on Zulip Johan Commelin (Sep 17 2018 at 07:55):

Aah, local attribute [instance] quotient_rel fixes it.

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:56):

that won't help outside the section

view this post on Zulip Mario Carneiro (Sep 17 2018 at 07:56):

you still want a public mk function

view this post on Zulip Johan Commelin (Sep 17 2018 at 08:00):

Right. Quotient rings already had that. But they didn't have lift

view this post on Zulip Mario Carneiro (Sep 17 2018 at 08:01):

in that case you should use it in the statement of lift_mk

view this post on Zulip Johan Commelin (Sep 17 2018 at 08:19):

Ok, this is what I now have

namespace quotient_ring -- move this to the right file
open is_submodule
variables {α : Type u} [comm_ring α] {β : Type v} [comm_ring β]

local attribute [instance] quotient_rel

def lift (S : set α) [is_ideal S] (f : α  β) [is_ring_hom f] (H :  (a : α), a  S  f a = 0) :
quotient S  β :=
begin
  refine @quotient.lift _ _ (quotient_rel S) f _,
  intros a b h,
  apply eq_of_sub_eq_zero,
  rw quotient_rel_eq at h,
  simpa only [is_ring_hom.map_sub f] using H _ h,
end

@[simp] lemma lift_mk {S : set α} [is_ideal S] {f : α  β} [is_ring_hom f] {H :  (a : α), a  S  f a = 0} {a : α} :
lift S f H a = f a := rfl

#print quotient_ring.is_ring_hom_mk

instance {S : set α} [is_ideal S] {f : α  β} [is_ring_hom f] {H :  (a : α), a  S  f a = 0} :
is_ring_hom (lift S f H) :=
{ map_one := by show lift S f H 1 = 1; simp [is_ring_hom.map_one f],
  map_add := λ a₁ a₂, quotient.induction_on₂ a₁ a₂ $ λ a₁ a₂, begin
    show lift S f H (mk a₁ + mk a₂) = lift S f H a₁ + lift S f H a₂,
    have := quotient_ring.is_ring_hom_mk S,
    rw  this.map_add,
    show lift S f H (a₁ + a₂) = lift S f H a₁ + lift S f H a₂,
    simp only [lift_mk, is_ring_hom.map_add f],
  end,
  map_mul := λ a₁ a₂, quotient.induction_on₂ a₁ a₂ $ λ a₁ a₂, begin
    show lift S f H (mk a₁ * mk a₂) = lift S f H a₁ * lift S f H a₂,
    have := quotient_ring.is_ring_hom_mk S,
    rw  this.map_mul,
    show lift S f H (a₁ * a₂) = lift S f H a₁ * lift S f H a₂,
    simp only [lift_mk, is_ring_hom.map_mul f],
  end }

end quotient_ring

view this post on Zulip Chris Hughes (Sep 17 2018 at 08:33):

You should be able to use quotient.lift' instead of @quotient.lift ...

view this post on Zulip Johan Commelin (Sep 17 2018 at 08:34):

Yes, I've been golfing them a bit. I didn't use the lift' version though.

view this post on Zulip Johan Commelin (Sep 17 2018 at 08:49):

Ok, I pushed a bunch of changes

view this post on Zulip Johan Commelin (Sep 17 2018 at 08:49):

@Mario Carneiro I think I might want to try the induction proof now...

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:02):

Hmm, so we have UFD's but we don't know that K[X] is an example of a UFD

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:03):

What we need to know is that if we have a polynomial f with a root x, then we can factor f as (X - x) * g, and the degree of g is lower than degree f.

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:04):

@Chris Hughes Did you have stuff like that in your QR project?

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:04):

This is Euclidean division

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:04):

I think we have that

view this post on Zulip Chris Hughes (Sep 17 2018 at 09:04):

It's in polynomial.lean

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:04):

Great

view this post on Zulip Chris Hughes (Sep 17 2018 at 09:04):

dvd_iff_is_root or something

view this post on Zulip Chris Hughes (Sep 17 2018 at 09:07):

Can't find it. We have similar stuff. p %ₘ (X - C a) = C (p.eval a) and dvd_iff_mod_by_monic_eq_zero

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:07):

@Johannes Hölzl Have you thought about PID → UFD in Lean?

view this post on Zulip Chris Hughes (Sep 17 2018 at 09:08):

Euclidean_domain -> UFD might be easier, and that all that's needed.

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 09:10):

I didn't think about it yet, but I surely want it. I guess that's my project for today :-)

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:10):

Awesome!

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:11):

Your version of UFD is not a Prop. Do we also want a version where it is a prop?

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:11):

Johan, what's your plan? Are you still working towards a specific goal before the birthday?

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 09:12):

when is the b-day again?

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:12):

Friday

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:12):

I'm not competent enough to work on pi

view this post on Zulip Johan Commelin (Sep 17 2018 at 09:12):

Maybe I shouldn't distract the experts, and let them work on that.

view this post on Zulip Patrick Massot (Sep 17 2018 at 09:13):

I think what is really needed is Mario and Johannes telling us whether they think anything from the kbb repository could be PR'ed on Friday

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:16):

How would you even show that K[X] is an example of a UFD, with the current definition of UFD? You have to give an algorithm that factors polynomials, right? I'm not sure if those even exist for arbitrary K...

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:17):

Or should we just use choice, somehow?

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:17):

@Johannes Hölzl did you have a particular plan here?

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 12:18):

Yes, in the worst case I will use choice.

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:18):

Ok, I see

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:53):

Here is a little hole in the polynomial api:

namespace polynomial

variables {R : Type u} [comm_semiring R] [decidable_eq R]

@[simp] lemma map_id (f : polynomial R) : map id f = f := sorry

end polynomial

view this post on Zulip Johan Commelin (Sep 17 2018 at 12:53):

How would I unsorry that?

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 12:56):

@Johan Commelin By the way, kbb doesn't build for me: SL2Z_M.finitely_many_orbits is missing

view this post on Zulip Johannes Hölzl (Sep 17 2018 at 13:00):

@Johan Commelin eval₂ is defined using the finsupp.sum operator. The combination of single_eq_C_mul_X and finsupp.sum_single should be enough. With sum_single you can proof that the polynomial f has a sum representation over single and with single_eq_C_mul_X you change the representation to C (id a) * X^n

view this post on Zulip Johan Commelin (Sep 17 2018 at 13:04):

@Johan Commelin By the way, kbb doesn't build for me: SL2Z_M.finitely_many_orbits is missing

Aaah, Kenny changed this. It is now

def finiteness (hm : m  0) : fintype (quotient $ action_rel $ SL2Z_M_ m) :=
@fintype.of_equiv _ _ (reps.fintype m hm) (reps_equiv m hm).symm

on lines 344-345 of SL2Z_generators.lean

view this post on Zulip Johan Commelin (Sep 17 2018 at 13:05):

I think that error was in the Hecke operator file? I'm afraid that file won't really see any improvements. I don't have the time, and probably it is not realistic to work on it before Friday anyway.

view this post on Zulip Johan Commelin (Sep 17 2018 at 13:09):

@[simp] lemma map_id (f : polynomial R) : map id f = f :=
by dsimp [map,eval₂]; conv { to_lhs, congr, skip, funext, rw  single_eq_C_mul_X }; simp

view this post on Zulip Johan Commelin (Sep 17 2018 at 13:09):

@Johannes Hölzl Thanks, done :lol:

view this post on Zulip Johan Commelin (Sep 17 2018 at 17:26):

I think that progress on splitting fields will require a bit of an api for k[x] as UFD. Things like units of R[x] is units of R. Every polynomial in k[x] of degree (not nat_degree!) equal to 0 is a unit, and vice versa. All polynomials of degree 1 are irreducible. Etc...

view this post on Zulip Johan Commelin (Sep 17 2018 at 17:27):

I have not started on any of this. But I also found myself mentally blocked on writing down the definition of a splitting field.

view this post on Zulip Johan Commelin (Sep 17 2018 at 17:27):

I suspect those issues are related.

view this post on Zulip Johannes Hölzl (Sep 19 2018 at 18:16):

I don't know if this is still needed, but PID -> UFD is finished now

view this post on Zulip Patrick Massot (Sep 19 2018 at 18:19):

Nice! I think the hope was to make progress on splitting field, which will probably not happen very soon. But this is good to know anyway.

view this post on Zulip Johan Commelin (Sep 19 2018 at 18:40):

@Johannes Hölzl Cool. Thanks a lot! I think this should help with the splitting fields branch. The next steps there are probably proving that non-zero constants are exactly the units and linear polynomials are irreducible.

view this post on Zulip Johan Commelin (Sep 19 2018 at 18:41):

Once that is know, I think we can start some sort of construction of splitting fields that inducts on the degree of the polynomial.


Last updated: May 18 2021 at 10:14 UTC