Zulip Chat Archive

Stream: maths

Topic: Splitting fields


view this post on Zulip 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 _)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:34):

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

view this post on Zulip Chris Hughes (Dec 12 2018 at 16:36):

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

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:38):

Oh, yeah, sorry. I misread that.

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:40):

Where is adjoin_root defined?

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:40):

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

view this post on Zulip Rob Lewis (Dec 12 2018 at 16:41):

Think I'm having trouble reading today.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Dec 12 2018 at 16:57):

using a big sigma or a structure

view this post on Zulip 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

view this post on Zulip Johan Commelin (Dec 12 2018 at 18:32):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 16 2018 at 06:59):

good luck transporting everything to ulift :P

view this post on Zulip Mario Carneiro (Dec 16 2018 at 06:59):

what is the problem with unbundling exactly?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:02):

What do you mean by stay away from universal definitions?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:04):

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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:05):

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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:05):

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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:10):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:29):

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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:29):

This is a general fact about fields

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:30):

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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:31):

(the isomorphism is not constructive in the reverse direction)

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:35):

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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:38):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:39):

like the subfield generated by polynomials in alpha

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:41):

I see.

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:41):

and so your lemma applies and the polynomial splits there

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:46):

That sounds easier.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Chris Hughes (Dec 16 2018 at 07:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:53):

You can do similar stuff with crazy well founded definitions

view this post on Zulip Mario Carneiro (Dec 16 2018 at 07:54):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Dec 16 2018 at 08:35):

Will resetI cause problems with that?

view this post on Zulip Mario Carneiro (Dec 16 2018 at 08:35):

I don't think so

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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 α)
  ( : splits i f) : splitting_field f  β :=
classical.some (exists_hom _ f rfl i )

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

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

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 10:57):

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

view this post on Zulip Chris Hughes (Dec 17 2018 at 10:58):

I proved the irreducible factor lemma for a noetherian domain.

view this post on Zulip Kenny Lau (Dec 17 2018 at 10:59):

see @Mario Carneiro this is problematic

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:09):

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

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:09):

what's problematic?

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:09):

that factor_set is hard to use

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:11):

demo? what's factor_set doing here

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:12):

what is factor_set

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:12):

associates.factor_set

view this post on Zulip Patrick Massot (Dec 17 2018 at 11:12):

Kenny, you shouldn't be so negative

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:12):

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

view this post on Zulip 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 α

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:13):

@Patrick Massot well played

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:13):

oh it's a ufd thing

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:13):

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:14):

how do we convert from factors to divisibility

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:14):

dvd_eq_le

view this post on Zulip Chris Hughes (Dec 17 2018 at 11:15):

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

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:15):

and factors_le

view this post on Zulip Kenny Lau (Dec 17 2018 at 11:15):

I see @Mario Carneiro

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:16):

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

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:18):

Anyway I think you could certainly push this

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:18):

next stop algebraic closure?

view this post on Zulip Mario Carneiro (Dec 17 2018 at 11:18):

I guess that's another messy induction like this

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Dec 17 2018 at 12:07):

@Chris Hughes What are your plans now?

view this post on Zulip Johan Commelin (Dec 17 2018 at 12:31):

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

view this post on Zulip Chris Hughes (Dec 17 2018 at 12:38):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 12:40):

The one on multiplicities?

view this post on Zulip Chris Hughes (Dec 17 2018 at 12:41):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 12:42):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Dec 17 2018 at 13:24):

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

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Dec 17 2018 at 13:27):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 13:27):

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

view this post on Zulip Kenny Lau (Dec 17 2018 at 13:36):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 13:39):

That seems like a good plan.

view this post on Zulip Kenny Lau (Dec 17 2018 at 13:43):

@Johan Commelin and my only objection would be predicativity

view this post on Zulip Kenny Lau (Dec 17 2018 at 13:44):

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

view this post on Zulip Johan Commelin (Dec 17 2018 at 14:58):

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


Last updated: May 06 2021 at 18:20 UTC