## Stream: kbb

### Topic: splitting fields

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

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

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

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

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


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


#### Johan Commelin (Sep 17 2018 at 07:29):

Which can undoubtly be golfed

#### Johan Commelin (Sep 17 2018 at 07:30):

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

yes

#### Mario Carneiro (Sep 17 2018 at 07:31):

the next step is the splitting field for one polynomial

#### Mario Carneiro (Sep 17 2018 at 07:33):

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

I think so

#### Johan Commelin (Sep 17 2018 at 07:35):

We know that polynomial K is a PID

#### Johan Commelin (Sep 17 2018 at 07:35):

and every PID is a UFD

#### Johan Commelin (Sep 17 2018 at 07:35):

I think that latter fact is now also in mathlib

we have UFDs?

#### Johan Commelin (Sep 17 2018 at 07:36):

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

#### Johan Commelin (Sep 17 2018 at 07:36):

We'll also need that.

yes

#### Johan Commelin (Sep 17 2018 at 07:36):

Yes, Johannes added UFD's after Orsay

#### Johan Commelin (Sep 17 2018 at 07:36):

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

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

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

#### Johan Commelin (Sep 17 2018 at 07:38):

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

#### Johan Commelin (Sep 17 2018 at 07:38):

Hmm, factoring is hard.

#### Mario Carneiro (Sep 17 2018 at 07:38):

that isn't needed, it follows by homness

???

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

#### Mario Carneiro (Sep 17 2018 at 07:40):

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

#### Mario Carneiro (Sep 17 2018 at 07:40):

we definitely need that

#### Johan Commelin (Sep 17 2018 at 07:43):

I didn't even prove it is a ring hom

#### Johan Commelin (Sep 17 2018 at 07:44):

Working on that now

#### Mario Carneiro (Sep 17 2018 at 07:44):

I think those are the same

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


#### Johan Commelin (Sep 17 2018 at 07:49):

Should the latter be a simp-lemma?

#### Johan Commelin (Sep 17 2018 at 07:49):

At the moment the ⟦a⟧ notation is broken.

#### Johan Commelin (Sep 17 2018 at 07:50):

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

#### Mario Carneiro (Sep 17 2018 at 07:50):

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

#### Mario Carneiro (Sep 17 2018 at 07:51):

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

#### Johan Commelin (Sep 17 2018 at 07:52):

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

#### Johan Commelin (Sep 17 2018 at 07:52):

Splitting field will come later.

#### Johan Commelin (Sep 17 2018 at 07:52):

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

#### Johan Commelin (Sep 17 2018 at 07:53):

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

ah okay

#### Mario Carneiro (Sep 17 2018 at 07:53):

you want to redefine mk for that

#### Mario Carneiro (Sep 17 2018 at 07:54):

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

#### Mario Carneiro (Sep 17 2018 at 07:54):

when you prove it is a ring hom

#### Johan Commelin (Sep 17 2018 at 07:55):

Aah, local attribute [instance] quotient_rel fixes it.

#### Mario Carneiro (Sep 17 2018 at 07:56):

that won't help outside the section

#### Mario Carneiro (Sep 17 2018 at 07:56):

you still want a public mk function

#### Johan Commelin (Sep 17 2018 at 08:00):

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

#### Mario Carneiro (Sep 17 2018 at 08:01):

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

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


#### Chris Hughes (Sep 17 2018 at 08:33):

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

#### Johan Commelin (Sep 17 2018 at 08:34):

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

#### Johan Commelin (Sep 17 2018 at 08:49):

Ok, I pushed a bunch of changes

#### Johan Commelin (Sep 17 2018 at 08:49):

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

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

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

#### Johan Commelin (Sep 17 2018 at 09:04):

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

#### Patrick Massot (Sep 17 2018 at 09:04):

This is Euclidean division

#### Patrick Massot (Sep 17 2018 at 09:04):

I think we have that

#### Chris Hughes (Sep 17 2018 at 09:04):

It's in polynomial.lean

Great

#### Chris Hughes (Sep 17 2018 at 09:04):

dvd_iff_is_root or something

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

#### Johan Commelin (Sep 17 2018 at 09:07):

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

#### Chris Hughes (Sep 17 2018 at 09:08):

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

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

Awesome!

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

#### Patrick Massot (Sep 17 2018 at 09:11):

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

#### Johannes Hölzl (Sep 17 2018 at 09:12):

when is the b-day again?

Friday

#### Johan Commelin (Sep 17 2018 at 09:12):

I'm not competent enough to work on pi

#### Johan Commelin (Sep 17 2018 at 09:12):

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

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

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

#### Johan Commelin (Sep 17 2018 at 12:17):

Or should we just use choice, somehow?

#### Johan Commelin (Sep 17 2018 at 12:17):

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

#### Johannes Hölzl (Sep 17 2018 at 12:18):

Yes, in the worst case I will use choice.

Ok, I see

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


#### Johan Commelin (Sep 17 2018 at 12:53):

How would I unsorry that?

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

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

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

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

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


#### Johan Commelin (Sep 17 2018 at 13:09):

@Johannes Hölzl Thanks, done :lol:

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

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

#### Johan Commelin (Sep 17 2018 at 17:27):

I suspect those issues are related.

#### Johannes Hölzl (Sep 19 2018 at 18:16):

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

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

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

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