splitting fields

Stream: kbb

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Which can undoubtly be golfed

[Johan Commelin]

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

[Mario Carneiro]

yes

[Mario Carneiro]

the next step is the splitting field for one polynomial

[Mario Carneiro]

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

[Johan Commelin]

I think so

[Johan Commelin]

We know that polynomial K is a PID

[Johan Commelin]

and every PID is a UFD

[Johan Commelin]

I think that latter fact is now also in mathlib

[Mario Carneiro]

we have UFDs?

[Johan Commelin]

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

[Johan Commelin]

We'll also need that.

[Mario Carneiro]

yes

[Johan Commelin]

Yes, Johannes added UFD's after Orsay

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Hmm, factoring is hard.

[Mario Carneiro]

that isn't needed, it follows by homness

[Johan Commelin]

???

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

we definitely need that

[Johan Commelin]

I didn't even prove it is a ring hom

[Johan Commelin]

Working on that now

[Mario Carneiro]

I think those are the same

[Johan Commelin]

@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

[Johan Commelin]

Should the latter be a simp-lemma?

[Johan Commelin]

At the moment the ⟦a⟧ notation is broken.

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

Splitting field will come later.

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

ah okay

[Mario Carneiro]

you want to redefine mk for that

[Mario Carneiro]

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

[Mario Carneiro]

when you prove it is a ring hom

[Johan Commelin]

Aah, local attribute [instance] quotient_rel fixes it.

[Mario Carneiro]

that won't help outside the section

[Mario Carneiro]

you still want a public mk function

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

Ok, I pushed a bunch of changes

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Patrick Massot]

This is Euclidean division

[Patrick Massot]

I think we have that

[Chris Hughes]

It's in polynomial.lean

[Johan Commelin]

Great

[Chris Hughes]

dvd_iff_is_root or something

[Chris Hughes]

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

[Johan Commelin]

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

[Chris Hughes]

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

[Johannes Hölzl]

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

[Johan Commelin]

Awesome!

[Johan Commelin]

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

[Patrick Massot]

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

[Johannes Hölzl]

when is the b-day again?

[Johan Commelin]

Friday

[Johan Commelin]

I'm not competent enough to work on pi

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

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

[Johan Commelin]

Or should we just use choice, somehow?

[Johan Commelin]

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

[Johannes Hölzl]

Yes, in the worst case I will use choice.

[Johan Commelin]

Ok, I see

[Johan Commelin]

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

[Johan Commelin]

How would I unsorry that?

[Johannes Hölzl]

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

[Johannes Hölzl]

@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

[Johan Commelin]

@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

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

@Johannes Hölzl Thanks, done :lol:

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I suspect those issues are related.

[Johannes Hölzl]

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

[Patrick Massot]

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.

[Johan Commelin]

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

[Johan Commelin]

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