## Stream: maths

### Topic: Splitting fields

#### Chris Hughes (Dec 12 2018 at 16:16):

So I thought I'd revive the splitting fields branch on community mathlib. So far I've just updated it to work with current mathlib. This is my definition of splitting fields. It's a bit unusual to write a recursive function like this returning a Type; is this a good approach? Also my definition of of_field the embedding from the base field gives me the error rec_fn_macro only allowed in meta definitions. What is this?

def splitting_field' : Π {n : ℕ} {α : Type u} [discrete_field α] (f : by exactI polynomial α),
by exactI nat_degree f = n → Type u
| 0 := λ α I f hn, α
| 1 := λ α I f hn, α
| (n + 2) := λ α I f hn, by exactI
have hf : nat_degree (f.map (coe : α → adjoin_root (irr_factor f (by rw hn; exact dec_trivial))) /
(X - C root)) = n + 1, from sorry,
splitting_field' (f.map (coe : α → adjoin_root (irr_factor f (by rw hn; exact dec_trivial))) /
(X - C root)) hf

def of_field' : Π {n : ℕ} {α : Type u} [discrete_field α] (f : by exactI polynomial α)
(hf : by exactI nat_degree f = n), α → by exactI splitting_field' f hf
| 0     := λ α I f hf a, a
| 1     := λ α I f hf a, a
| (n+2) := λ α I f hf a, by exactI of_field' _ _ (↑a : adjoin_root _)


#### Chris Hughes (Dec 12 2018 at 16:32):

Okay I still get the error rec_fn_macro only allowed in meta definitions even if I make it meta

#### Rob Lewis (Dec 12 2018 at 16:34):

Could you rearrange the arguments so that  {α : Type u} [discrete_field α] are left of the colon? If nothing else it will let you get rid of the exactIs.

#### Rob Lewis (Dec 12 2018 at 16:34):

That error sounds like something funny in the equation compiler, so simplifying its job might help.

#### Chris Hughes (Dec 12 2018 at 16:36):

Not without changing my method significantly. I use a different type when I recursively call it.

#### Rob Lewis (Dec 12 2018 at 16:38):

Oh, yeah, sorry. I misread that.

#### Rob Lewis (Dec 12 2018 at 16:40):

Where is adjoin_root defined?

#### Rob Lewis (Dec 12 2018 at 16:40):

In the splitting field branch on community, I take it.

#### Rob Lewis (Dec 12 2018 at 16:41):

Think I'm having trouble reading today.

#### Johan Commelin (Dec 12 2018 at 16:46):

@Chris Hughes I think this is exactly the approach that we had in mind when @Mario Carneiro, you and me were hacking on this in Orsay. Too bad it's giving troubles.

#### Reid Barton (Dec 12 2018 at 16:57):

I'm always tempted to package everything I care about together in a single recursive definition--here the type, its field instance, the map from the base field, the factorization of f

#### Reid Barton (Dec 12 2018 at 16:57):

using a big sigma or a structure

#### Chris Hughes (Dec 12 2018 at 17:38):

I found a work around by using nat.rec_on instead of the equation compiler. Seems like it has something to do with this https://github.com/leanprover/lean/issues/1890

#### Chris Hughes (Dec 14 2018 at 21:27):

I've had a new problem, and it's taken me most of the day to figure out what's going on. I think the trouble is that I have an expression where f : polynomial α is mentioned and also some stuff of type adjoin_root f. When I try to rewrite with f = _ It tries to rewrite all the types that mention f and hangs. I solved it using conv but I thought there might be a better way to do this.

#### Johan Commelin (Dec 15 2018 at 09:59):

Isn't this what conv is meant for? I think there's nothing wrong with using it here.

#### Chris Hughes (Dec 16 2018 at 06:45):

So I've some up against a more serious problem. I've defined something of this type

lemma splitting_field_aux : Π {α : Type u} [discrete_field α] (f : by exactI polynomial α),
by exactI Σ' (β : Type u) [discrete_field β] (i : α → β) [is_field_hom i]
(hs : by exactI splits i f), ∀ {γ : Type u} [discrete_field γ] (j : α → γ)
[is_field_hom j] (hj : by exactI splits j f),
∃ k : β → γ, (∀ x, k (i x) = j x) ∧ is_field_hom k


I bundled everything we needed to know together in one definition because I didn't want to have to deal with eq.rec and non definitional equation lemmas. The only trouble with this approach is that the homomorphism from the splitting field into any field that splits only goes into fields in the same universe. The only way around this that I can see is to unbundle the definition, and deal with nasty equation lemmas. Is there any easier way around this?

#### Johan Commelin (Dec 16 2018 at 06:58):

I'm inclined to say that we shouldn't worry about universes here. If universe issues show up, I hope ulift will help.

#### Kenny Lau (Dec 16 2018 at 06:59):

good luck transporting everything to ulift :P

#### Mario Carneiro (Dec 16 2018 at 06:59):

what is the problem with unbundling exactly?

#### Mario Carneiro (Dec 16 2018 at 07:00):

I guess that would be much more convenient to use if it were unbundled, although maybe you need this for the construction?

#### Mario Carneiro (Dec 16 2018 at 07:01):

I think you should try to stay away from "universal definitions" of universal objects, because they are never universe polymorphic enough

#### Chris Hughes (Dec 16 2018 at 07:01):

Then I'd have to unfold the definition to prove things about it. And the equation lemmas are not definitional, so I'd need eq.rec to turn it into adjoin_root whatever  and eq.rec is hard to use.

#### Chris Hughes (Dec 16 2018 at 07:02):

What do you mean by stay away from universal definitions?

#### Mario Carneiro (Dec 16 2018 at 07:02):

right, we definitely want to avoid that. But I'm still not following. Could you show a bit of how you get to this point?

#### Mario Carneiro (Dec 16 2018 at 07:03):

For example, you can define nat := \forall X, {X -> (X -> X) -> X // naturality property} but it's not a good definition because X only lives in one universe

#### Chris Hughes (Dec 16 2018 at 07:04):

https://github.com/ChrisHughes24/mathlib/blob/5efef7b26f78b5bcbcbc43d4d3ae32be7aa6018b/field_theory/splitting_field.lean

#### Mario Carneiro (Dec 16 2018 at 07:04):

instead you want some kind of "intrinsic" characterization of the object that implies the universal property, in any universe

#### Chris Hughes (Dec 16 2018 at 07:05):

So in this example, maybe the fact that any proper subfield does not split?

#### Chris Hughes (Dec 16 2018 at 07:05):

I'll have to think about whether that approach is much harder.

#### Mario Carneiro (Dec 16 2018 at 07:10):

In this case, it looks like that is indeed the right "smallness" property

#### Mario Carneiro (Dec 16 2018 at 07:11):

another way to express it is to start from the theorem you just proved, and show that splitting in one universe implies splitting in all the rest

#### Mario Carneiro (Dec 16 2018 at 07:11):

by taking a special choice of gamma, namely the subfield isomorphic to the gamma in another universe

#### Chris Hughes (Dec 16 2018 at 07:29):

Proving that such a subfield exists is hard though, unless I'm missing a trick?

#### Mario Carneiro (Dec 16 2018 at 07:29):

This is a general fact about fields

#### Mario Carneiro (Dec 16 2018 at 07:30):

Every field hom is injective, so when you restrict to the range you get an isomorphism

#### Mario Carneiro (Dec 16 2018 at 07:31):

(the isomorphism is not constructive in the reverse direction)

#### Chris Hughes (Dec 16 2018 at 07:35):

I still don't understand. Given a field, which subfield do I choose?

#### Mario Carneiro (Dec 16 2018 at 07:38):

oh wait I had it backwards, you need a field into the large universe

#### Mario Carneiro (Dec 16 2018 at 07:39):

for that you can take a subfield of gamma sufficiently large to contain all the action from beta

#### Mario Carneiro (Dec 16 2018 at 07:39):

like the subfield generated by polynomials in alpha

#### Mario Carneiro (Dec 16 2018 at 07:41):

this subfield will be isomorphic to a quotient of a polynomial ring etc etc which is in Type u

I see.

#### Mario Carneiro (Dec 16 2018 at 07:41):

and so your lemma applies and the polynomial splits there

#### Mario Carneiro (Dec 16 2018 at 07:43):

you should double check with @Kevin Buzzard , I walked him through this a few months ago and I think he did almost exactly the same thing in the perfectoid project

#### Mario Carneiro (Dec 16 2018 at 07:44):

as an alternative, returning to the unbundling problem: I assume the reason it isn't definitional is because you are using wf recursion

#### Mario Carneiro (Dec 16 2018 at 07:45):

If you define one step of the induction as a lemma, then it will be definitional there

#### Chris Hughes (Dec 16 2018 at 07:46):

That sounds easier.

#### Mario Carneiro (Dec 16 2018 at 07:46):

so you have something like F : (A : Type u) (h : P.{u} A), Type u and prop : (A : Type u) (h : P.{u} A), P.{v} (F A)

#### Mario Carneiro (Dec 16 2018 at 07:49):

and then you have an induction proof putting it together, which does F /\ P.{u} F, and a cases proof doing the same thing with conclusion P.{v} F

#### Chris Hughes (Dec 16 2018 at 07:51):

It's also not definitional because I've got an ite on degree f \le 1

#### Mario Carneiro (Dec 16 2018 at 07:51):

Also, before I forget: a very general way of avoiding problems with types defined by complicated rules is to use an inductive type instead

#### Mario Carneiro (Dec 16 2018 at 07:53):

for example, simulating if x < 2 then nat else unit:

inductive my_cases (x : ℕ) : Type
| nat : x < 2 → nat → my_cases
| unit : x >= 2 → unit → my_cases


#### Mario Carneiro (Dec 16 2018 at 07:53):

You can do similar stuff with crazy well founded definitions

#### Mario Carneiro (Dec 16 2018 at 07:54):

in the inductive case you don't even have to worry about well foundedness

#### Chris Hughes (Dec 16 2018 at 08:10):

The other major issue I have is that making it a def gives me the error rec_fn_macro only allowed in meta definitions.

#### Mario Carneiro (Dec 16 2018 at 08:21):

that means there is probably a tactic referencing one of the _match type variables in the context by accident

#### Mario Carneiro (Dec 16 2018 at 08:22):

you can fix this by clearing it when you have used it, or even using it right at the start and clearing it then (or if its random junk then just remove it)

#### Chris Hughes (Dec 16 2018 at 08:35):

Will resetI cause problems with that?

I don't think so

#### Mario Carneiro (Dec 16 2018 at 08:36):

At some version of resetI I recall it deleting the recursive function variable as a side effect, not sure if that's still the case but I think not

#### Kevin Buzzard (Dec 16 2018 at 09:54):

I've only just seen this thread. Chris I'll dig out the universe conversation Mario and I had when I'm at a pc

#### Chris Hughes (Dec 17 2018 at 10:57):

All done and sorry free. @Mario Carneiro are you happy for me to push all of this to the splitting fields branch in community?

def splitting_field (f : polynomial α) := splitting_field.type_aux f rfl

namespace splitting_field

instance field (f : polynomial α) : discrete_field (splitting_field f) :=
by unfold splitting_field; apply_instance

def mk (f : polynomial α) : α → splitting_field f := mk_aux f rfl

instance (f : polynomial α) : is_field_hom (mk f) :=
by unfold mk; apply_instance

lemma splitting_field_splits (f : polynomial α) : splits (mk f) f :=
(splitting_field_aux f rfl).2.2.2.2

def hom {β : Type v} [discrete_field β] (i : α → β) [is_field_hom i] (f : polynomial α)
(hβ : splits i f) : splitting_field f → β :=
classical.some (exists_hom _ f rfl i hβ)

@[instance] lemma hom_is_field_hom {β : Type v} [discrete_field β] (i : α → β) [is_field_hom i]
(f : polynomial α) (hβ : splits i f) : is_field_hom (hom i f hβ) :=
(classical.some_spec (exists_hom _ f rfl i hβ)).2

@[simp] lemma hom_fixes {β : Type v} [discrete_field β] (i : α → β) [is_field_hom i]
(f : polynomial α) (hβ : splits i f) : ∀ x, hom i f hβ (mk f x) = i x :=
(classical.some_spec (exists_hom _ f rfl i hβ)).1

attribute [irreducible] hom splitting_field splitting_field.field splitting_field.mk


#### Kenny Lau (Dec 17 2018 at 10:57):

@Chris Hughes so how did you extract an element from factor_set?

#### Chris Hughes (Dec 17 2018 at 10:58):

I proved the irreducible factor lemma for a noetherian domain.

#### Kenny Lau (Dec 17 2018 at 10:59):

see @Mario Carneiro this is problematic

#### Chris Hughes (Dec 17 2018 at 11:00):

I don't think it's problematic. You shouldn't use UFD for that anyway since it's true in greater generality.

#### Mario Carneiro (Dec 17 2018 at 11:09):

Looks good to me, although I would call hom lift instead

#### Mario Carneiro (Dec 17 2018 at 11:09):

what's problematic?

#### Kenny Lau (Dec 17 2018 at 11:09):

that factor_set is hard to use

#### Mario Carneiro (Dec 17 2018 at 11:11):

demo? what's factor_set doing here

#### Kenny Lau (Dec 17 2018 at 11:11):

well could you prove that the factor set of a non-unit non-zero element is nonempty?

#### Mario Carneiro (Dec 17 2018 at 11:12):

what is factor_set

#### Kenny Lau (Dec 17 2018 at 11:12):

associates.factor_set

#### Patrick Massot (Dec 17 2018 at 11:12):

Kenny, you shouldn't be so negative

#### Mario Carneiro (Dec 17 2018 at 11:12):

it's not in the mathlib version, remind me what it does

#### Kenny Lau (Dec 17 2018 at 11:12):

associates.factors :
Π {α : Type u_1} [_inst_1 : integral_domain α] [_inst_2 : unique_factorization_domain α]
[_inst_3 : decidable_eq (associates α)], associates α → associates.factor_set α


#### Kenny Lau (Dec 17 2018 at 11:13):

@Patrick Massot well played

#### Chris Hughes (Dec 17 2018 at 11:13):

If it was empty the product would be one. Seems like it's probably not that hard.

#### Mario Carneiro (Dec 17 2018 at 11:13):

oh it's a ufd thing

#### Kenny Lau (Dec 17 2018 at 11:13):

how about that any non-zero non-unit is divisible by an irreducible

#### Kenny Lau (Dec 17 2018 at 11:14):

how do we convert from factors to divisibility

#### Mario Carneiro (Dec 17 2018 at 11:14):

dvd_eq_le

#### Chris Hughes (Dec 17 2018 at 11:15):

Prove that a UFD is noetherian, and use the lemma I proved.

#### Mario Carneiro (Dec 17 2018 at 11:15):

and factors_le

#### Kenny Lau (Dec 17 2018 at 11:15):

I see @Mario Carneiro

#### Mario Carneiro (Dec 17 2018 at 11:16):

it's a bit cumbersome to state, but it looks like the lemmas are there

#### Mario Carneiro (Dec 17 2018 at 11:18):

Anyway I think you could certainly push this

#### Mario Carneiro (Dec 17 2018 at 11:18):

next stop algebraic closure?

#### Mario Carneiro (Dec 17 2018 at 11:18):

I guess that's another messy induction like this

#### Johan Commelin (Dec 17 2018 at 12:05):

Before going towards algebraic closure, I would like to have this PR'd. This is going to be a very useful tool in the theory if finite extensions. I think it makes sense to start defining separable and normal extensions now. We're pretty close to finite Galois extensions.

#### Johan Commelin (Dec 17 2018 at 12:07):

@Chris Hughes What are your plans now?

#### Johan Commelin (Dec 17 2018 at 12:31):

@Chris Hughes I merged master into this branch and pushed.

#### Chris Hughes (Dec 17 2018 at 12:38):

This branch does now depend on unmerged PRs that I have made.

#### Johan Commelin (Dec 17 2018 at 12:40):

The one on multiplicities?

#### Chris Hughes (Dec 17 2018 at 12:41):

And some others. I have three open to do with polynomials right now I think.

#### Johan Commelin (Dec 17 2018 at 12:42):

Yes, I see. Ok, let's hope those get merged soon.

#### Johan Commelin (Dec 17 2018 at 12:43):

Do you want to do more with this branch? I mean, it's name is splitting_fields, so maybe new stuff should happen on a new branch?

#### Chris Hughes (Dec 17 2018 at 12:53):

I think new stuff should happen on a new branch. I think it's best to not make PRs too big.

#### Johan Commelin (Dec 17 2018 at 13:18):

So, if I'm not mistaken... the first 10 points of https://github.com/kckennylau/Lean/blob/master/algebraic-closure-roadmap.md have now been done. (Although not everything is in mathlib yet.)

#### Johan Commelin (Dec 17 2018 at 13:23):

Kenny, do you mind if I copy-paste that roadmap to the github wiki of the community repo? Then we can start ticking of things that we've done.

#### Kenny Lau (Dec 17 2018 at 13:24):

might want to replace the whole discriminant business with just GCD? ah the beauty of impredicativity

#### Johan Commelin (Dec 17 2018 at 13:26):

According to wiki, a polynomial is separable if it has just as many roots in its splitting field as its degree. So a square of a separable polynomial is not separable... choices...

#### Kenny Lau (Dec 17 2018 at 13:27):

I don't think we're talking about the same thing

#### Kenny Lau (Dec 17 2018 at 13:36):

and I was asking if you might want to change 11-14 to just 14

#### Johan Commelin (Dec 17 2018 at 13:39):

That seems like a good plan.

#### Kenny Lau (Dec 17 2018 at 13:43):

@Johan Commelin and my only objection would be predicativity

#### Kenny Lau (Dec 17 2018 at 13:44):

which I'm sure less people care about, compared to constructivity...