Splitting fields

Stream: maths

[Chris Hughes]

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]

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

[Rob Lewis]

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]

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

[Chris Hughes]

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

[Rob Lewis]

Oh, yeah, sorry. I misread that.

[Rob Lewis]

Where is adjoin_root defined?

[Rob Lewis]

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

[Rob Lewis]

Think I'm having trouble reading today.

[Johan Commelin]

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

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]

using a big sigma or a structure

[Chris Hughes]

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

[Johan Commelin]

@Chris Hughes I think that this thread should know about this thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/simple.20field.20theory

[Chris Hughes]

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]

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

[Chris Hughes]

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]

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]

good luck transporting everything to ulift :P

[Mario Carneiro]

what is the problem with unbundling exactly?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Chris Hughes]

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]

What do you mean by stay away from universal definitions?

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Chris Hughes]

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

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Chris Hughes]

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

[Mario Carneiro]

This is a general fact about fields

[Mario Carneiro]

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

[Mario Carneiro]

(the isomorphism is not constructive in the reverse direction)

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

like the subfield generated by polynomials in alpha

[Mario Carneiro]

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

[Chris Hughes]

I see.

[Mario Carneiro]

and so your lemma applies and the polynomial splits there

[Mario Carneiro]

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]

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]

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

[Chris Hughes]

That sounds easier.

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

You can do similar stuff with crazy well founded definitions

[Mario Carneiro]

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

[Chris Hughes]

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]

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

[Mario Carneiro]

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]

Will resetI cause problems with that?

[Mario Carneiro]

I don't think so

[Mario Carneiro]

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]

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]

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]

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

[Chris Hughes]

I proved the irreducible factor lemma for a noetherian domain.

[Kenny Lau]

see @Mario Carneiro this is problematic

[Chris Hughes]

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

[Mario Carneiro]

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

[Mario Carneiro]

what's problematic?

[Kenny Lau]

that factor_set is hard to use

[Mario Carneiro]

demo? what's factor_set doing here

[Kenny Lau]

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

[Mario Carneiro]

what is factor_set

[Kenny Lau]

associates.factor_set

[Patrick Massot]

Kenny, you shouldn't be so negative

[Mario Carneiro]

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

[Kenny Lau]

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]

@Patrick Massot well played

[Chris Hughes]

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

[Mario Carneiro]

oh it's a ufd thing

[Kenny Lau]

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

[Kenny Lau]

how do we convert from factors to divisibility

[Mario Carneiro]

dvd_eq_le

[Chris Hughes]

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

[Mario Carneiro]

and factors_le

[Kenny Lau]

I see @Mario Carneiro

[Mario Carneiro]

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

[Mario Carneiro]

Anyway I think you could certainly push this

[Mario Carneiro]

next stop algebraic closure?

[Mario Carneiro]

I guess that's another messy induction like this

[Johan Commelin]

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]

@Chris Hughes What are your plans now?

[Johan Commelin]

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

[Chris Hughes]

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

[Johan Commelin]

The one on multiplicities?

[Chris Hughes]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

No, indeed. I was asking if we should copy your roadmap to the github wiki...

[Kenny Lau]

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

[Johan Commelin]

That seems like a good plan.

[Kenny Lau]

@Johan Commelin and my only objection would be predicativity

[Kenny Lau]

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

[Johan Commelin]

https://github.com/leanprover-community/mathlib/wiki/Algebraic-closure-roadmap