# Zulip Chat Archive

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

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

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

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?

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

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

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

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.

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

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

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

???

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

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

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

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

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

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

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?

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

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`

.

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

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