Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: Project ideas


Patrick Lutz (Jul 17 2020 at 22:00):

As we discussed today, one option for the rest of the seminar is to try to complete some larger project together, perhaps with the goal of formalizing some catchy-sounding theorems. This thread is for discussion of project ideas: theorems that we could try to prove, ideas about how to organize it, etc.

Patrick Lutz (Jul 17 2020 at 22:00):

(deleted)

Jalex Stark (Jul 17 2020 at 22:15):

contribute to sphere eversion? pick off something from freek's list? from the undergrad_todo list?

Kevin Buzzard (Jul 17 2020 at 22:35):

Try and figure out why algebraic closures still aren't done? Prove that a short exact sequence of complexes induces a long exact sequence of cohomology in an abelian category?

Kevin Buzzard (Jul 17 2020 at 22:35):

Define fundamental group of a topological space?

Kevin Buzzard (Jul 17 2020 at 22:36):

Higher homotopy groups even?

Kevin Buzzard (Jul 17 2020 at 22:37):

Make a basic API for locally ringed spaces?

Kevin Buzzard (Jul 17 2020 at 22:37):

Define Picard groups?

Kevin Buzzard (Jul 17 2020 at 22:37):

Ext and Tor?

Patrick Lutz (Jul 18 2020 at 00:27):

Sorry, I got interrupted when writing the original message. I meant to explain a bit more

Patrick Lutz (Jul 18 2020 at 00:28):

Some of the possible topics we discussed were:

Patrick Lutz (Jul 18 2020 at 00:28):

1) Fourier analysis. Goal: prove theorem about rate of decay of fourier series of CnC^n functions

Patrick Lutz (Jul 18 2020 at 00:29):

2) Fundamental Group. Goal: prove Galois connection between subgroups and covering spaces

Patrick Lutz (Jul 18 2020 at 00:29):

3) Fundamental theorem of calculus

Patrick Lutz (Jul 18 2020 at 00:29):

4) Galois Theory. Goal: prove Galois connection

Patrick Lutz (Jul 18 2020 at 00:29):

(4) seemed like the most popular option brought up so far

Patrick Lutz (Jul 18 2020 at 00:30):

but it would obviously involve figuring out how to do algebraic closures

Patrick Lutz (Jul 18 2020 at 00:30):

(or I guess assuming algebraic closures exist as an axiom and working from there)

Patrick Lutz (Jul 18 2020 at 00:32):

However, we haven't made any definite decisions. So this thread is for discussion of what topics sound most interesting, how feasible they are, what would be involved in completing different projects, and how to organize the project

Patrick Lutz (Jul 18 2020 at 00:32):

Thanks for the suggestions @Jalex Stark and @Kevin Buzzard! :)

Patrick Lutz (Jul 18 2020 at 00:33):

Since there seems to be the most interest in Galois theory, do either of you know anything about why algebraic closure is not in mathlib? Is it especially hard to do for some reason?

Patrick Lutz (Jul 18 2020 at 00:34):

And do either of you have any advice about how to organize this kind of project?

Thomas Browning (Jul 18 2020 at 01:06):

(a) does Galois theory need the existence of algebraic closures? (b) one option would be to have algebraic closures start off as an axiom and get proved as a side project

Jalex Stark (Jul 18 2020 at 01:09):

I think successful past projects have started with a detailed exposition in latex or markdown

Kevin Buzzard (Jul 18 2020 at 06:12):

We have some Galois theory, written by Imperial undergrads, in some ImperialCollegeLpndon repo on GitHub.

Kevin Buzzard (Jul 18 2020 at 06:12):

The fundamental theorem is still not in Lean

Kevin Buzzard (Jul 18 2020 at 06:13):

If you do work on Galois theory your aim should not just be to prove FTG but to finish the job and get it into mathlib

Kevin Buzzard (Jul 18 2020 at 06:14):

https://github.com/ImperialCollegeLondon/P11-Galois-Theory

Kevin Buzzard (Jul 18 2020 at 06:14):

You're more than welcome to use that material or add to it. The job is still far from done

Kevin Buzzard (Jul 18 2020 at 06:15):

Kenny Lau has had some interesting ideas about how to deal with KLMK\subseteq L\subseteq M

Kevin Buzzard (Jul 18 2020 at 06:16):

He was live streaming a proof of the tower law on Discord last week

Patrick Lutz (Jul 19 2020 at 17:18):

@Kevin Buzzard How much work are Imperial undergrads currently doing on this repository? It looks like the last commit was 24 days ago, but you mentioned Kenny Lau live streaming something last week.

Kevin Buzzard (Jul 19 2020 at 17:19):

Oh, work comes and goes

Patrick Lutz (Jul 19 2020 at 17:19):

Also, if we want to contribute to this project, would it be better for us to push directly to the master branch of the repo, make another branch, or fork the entire repo?

Kevin Buzzard (Jul 19 2020 at 17:19):

@Kenny Lau what do you think?

Kevin Buzzard (Jul 19 2020 at 17:19):

I think it's about time we got some Galois theory in Lean

Kenny Lau (Jul 19 2020 at 17:20):

sure

Kevin Buzzard (Jul 19 2020 at 17:20):

and I am spread quite thin at the minute, I'm trying to supervise a bunch of summer projects

Patrick Lutz (Jul 19 2020 at 17:20):

Also, is there any kind of written stuff about the organization of the project, what the different files mean, etc?

Patrick Lutz (Jul 19 2020 at 17:20):

It looks like there's quite a few files with just one or two small theorems in them. Is there some reason for that?

Patrick Lutz (Jul 19 2020 at 17:21):

Do all of the projects (https://github.com/ImperialCollegeLondon/P11-Galois-Theory/projects) represent things that still need to be done?

Kenny Lau (Jul 19 2020 at 17:22):

yeah mainly

Patrick Lutz (Jul 19 2020 at 17:24):

I assume files like cardinal.lean are intended to be added to the similar-named files in mathlib. Is there any reason not to just turn these into mathlib PRs and remove them from the Galois theory repo?

Patrick Lutz (Jul 19 2020 at 17:40):

@Kenny Lau In your opinion, what's the best way to understand what's been done so far in the Galois theory project? Like, what are the best files to look at first to get a sense of how it's organized? And what are the next things to do to make progress on the project?

Kenny Lau (Jul 20 2020 at 04:56):

what's happening is that I'm slowly making new PR's to mathlib

Kenny Lau (Jul 20 2020 at 04:59):

for example, https://github.com/leanprover-community/mathlib/pull/3355 has just been merged

Kenny Lau (Jul 20 2020 at 04:59):

(tower law)

Patrick Lutz (Jul 22 2020 at 03:49):

We've started an overleaf document to write up the definitions and theorems that need to be formalized to get the fundamental theorem of galois theory in lean. For now, ask Thomas Browning to get access to the document

Patrick Lutz (Jul 22 2020 at 03:50):

Also, @Kenny Lau is it okay if we coordinate with you about this project further in this thread going forward (like, in the next few weeks)?

Kenny Lau (Jul 22 2020 at 05:11):

go ahead

Jordan Brown (Jul 24 2020 at 01:07):

Are we including particular applications of Galois theory to number fields? Does mathlib already have Gauss' Lemma and the Eisenstein criterion? If not I think we should include them too, though not strictly necessary for the Galois correspondence.

Jalex Stark (Jul 24 2020 at 01:17):

https://leanprover-community.github.io/mathlib_docs/ring_theory/eisenstein_criterion.html

Jalex Stark (Jul 24 2020 at 01:17):

I found this by putting eisenstein in the search bar here https://leanprover-community.github.io/mathlib_docs/

Scott Morrison (Jul 27 2020 at 06:02):

Anyone interested-in-Galois-theory want to have a look at #3568? It's always great to have people helping out with the pull-request review process!

Thomas Browning (Jul 27 2020 at 15:17):

Unfortunately, I'm not super familiar with how these pull requests work. But it will be good to have is_separable in mathlib.

Kevin Buzzard (Jul 27 2020 at 15:25):

Scott is just suggesting that people look at the code in the link, to see if they have any comments of the form "why not prove this lemma as well" or "this docstring has a typo" or anything

Patrick Lutz (Jul 29 2020 at 00:41):

Is there anything in mathlib/the imperial repo/our repo showing that if EE is a finite extension of FF then every element of EE is integral over FF?

Patrick Lutz (Jul 29 2020 at 00:55):

I'm going to try to prove the case of the primitive element theorem of an extension by adjoining two elements today. In case anyone else is working on it. (If someone is, I'm happy to collaborate). Although maybe it will take me more time to finish it

Kevin Buzzard (Jul 29 2020 at 07:10):

I think there's a lot about integrality in mathlib

Kenny Lau (Jul 29 2020 at 07:34):

https://github.com/leanprover-community/mathlib/blob/7cd1e268ef09e4f24c18b63079ee61f917ce7836/src/ring_theory/integral_closure.lean#L133-L134

theorem is_integral_of_mem_of_fg (S : subalgebra R A)
  (HS : (S : submodule R A).fg) (x : A) (hx : x  S) : is_integral R x :=

Patrick Lutz (Jul 29 2020 at 23:25):

Patrick Lutz said:

I'm going to try to prove the case of the primitive element theorem of an extension by adjoining two elements today. In case anyone else is working on it. (If someone is, I'm happy to collaborate). Although maybe it will take me more time to finish it

Lol, this is probably going to take a while actually. But we now have the primitive element theorem for finite fields.

Patrick Lutz (Jul 30 2020 at 21:10):

@Jordan Brown I think we should change the statement of the theorem in root_construction.lean to first define the isomorphism between F[x]/f(x)F[x]/f(x) and F[α]F[\alpha] (where ff is the minimal polynomial of α\alpha) and then prove the properties of this isomorphism, for instance that it takes xx to α\alpha.

Patrick Lutz (Jul 30 2020 at 21:10):

See the changes that I've made to the file for reference

Patrick Lutz (Jul 30 2020 at 21:19):

Also, something is messed up with the statement of primitive_element_inf_aux in primitive_element.lean. The statement being proved by induction is not strong enough to carry out the induction. We should be quantifying over the field FF after quantifying over nn instead of before. But when I try to do this I run into the problem that Lean no longer knows how to do the type inferences correctly, which is quite annoying. For more details, see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Problems.20with.20induction.20and.20type.20inference where I try to turn this into a question that doesn't mention galois theory/etc.

Patrick Lutz (Jul 30 2020 at 21:32):

Also, I'm starting to think that we should combine all of adjoin_set.lean, adjoin_simple.lean and root_construction.lean into a single adjoin.lean file just to keep things simpler.

Thomas Browning (Jul 30 2020 at 22:23):

I'd be happy to combine them, although keeping them separate (for now) has two potential advantages: files don't get too long, and merge conflicts are more rare

Patrick Lutz (Jul 30 2020 at 22:31):

Okay, let's leave them separate for now but consider combining them once they're a bit more complete

Thomas Browning (Jul 31 2020 at 00:26):

I've made a change to how the results in adjoin_set and adjoin_simple are stated. The E is now implicit. I think this makes sense since E can always be deduced from what you're adjoining. Now you would write "adjoin_simple F a" rather than "adjoin_simple F E a."

Thomas Browning (Jul 31 2020 at 21:21):

I've moved stuff to adjoin.lean, so use that rather than adjoin_set.lean or adjoin_simple.lean

Kenny Lau (Aug 01 2020 at 06:52):

#3654 @Kevin Buzzard @Johan Commelin @Chris Hughes

Jordan Brown (Aug 04 2020 at 00:26):

Does mathlib have a way to restrict group actions to a subgroup? It seems like it should be there, but I cannot find such a construction.

Thomas Browning (Aug 04 2020 at 00:33):

Not sure, but you will need to assume that the subgroup is stable under the group action

Jordan Brown (Aug 04 2020 at 00:36):

What do you mean? I am talking about restricting the acting group, not the set being acted upon

Thomas Browning (Aug 04 2020 at 00:41):

oh right, I see what you mean

Thomas Browning (Aug 04 2020 at 00:43):

/-- An action of `α` on `β` and a monoid homomorphism `γ → α` induce an action of `γ` on `β`. -/
def comp_hom [monoid γ] (g : γ  α) [is_monoid_hom g] :
  mul_action γ β :=
{ smul := λ x b, (g x)  b,
  one_smul := by simp [is_monoid_hom.map_one g, mul_action.one_smul],
  mul_smul := by simp [is_monoid_hom.map_mul g, mul_action.mul_smul] }

Thomas Browning (Aug 04 2020 at 00:43):

That might be enough for you, because you can apply it to H->G

Patrick Lutz (Aug 05 2020 at 02:41):

@Thomas Browning How easy is it to transfer facts about adjoining elements to a subfield FF of a field EE, thought of as an algebra map from FF to EE, to the subfield of EE given by the image of this algebra map? Basically, how easy is it to fill in the sorries in primitive_element_inf?

Thomas Browning (Aug 05 2020 at 03:55):

Not super easy. It might be worth constructing an isomorphism, and proving that those properties are preserved by isomorphism.

Thomas Browning (Aug 05 2020 at 03:57):

I'll prove the isomorphism in adjoin.lean, since it might come up later as well

Patrick Lutz (Aug 05 2020 at 04:00):

By the way, if you have time it might be nice to write comments documenting what the different stuff in adjoin.lean is doing.

Patrick Lutz (Aug 05 2020 at 04:00):

but it's not a big deal

Thomas Browning (Aug 05 2020 at 04:00):

sure. actually, I just realized that this isomorphim doesn't belong in adjoin.lean at all since it doesn't involve adjoining. Where should it go?

Thomas Browning (Aug 05 2020 at 04:01):

make a new file for properties of subfields?

Patrick Lutz (Aug 05 2020 at 04:01):

Sure. Or if you want it can go in primitive_element.lean for now. Either way is fine with me

Patrick Lutz (Aug 05 2020 at 04:02):

Also, I added two lemma statements about the degree of EE over F[α]F[\alpha]. Right now they're in primitive_element.lean but if you think we should, they could be moved to adjoin.lean

Patrick Lutz (Aug 05 2020 at 04:03):

Also, I'm curious if you have an opinion on how hard they are to prove. One of them says that if EE is a finite extension of FF then EE is also a finite extension of F[α]F[\alpha] and the other says that if α\alpha is not in FF then the degree strictly decreases.

Patrick Lutz (Aug 05 2020 at 04:04):

One annoying part is that here FF is again a subset of EE. Though maybe not so bad here, especially for the first of the lemmas

Thomas Browning (Aug 05 2020 at 04:06):

well, those are true about any subfields, and I don't expect them to be hard to prove (since we have the power law).

Patrick Lutz (Aug 05 2020 at 04:08):

Thomas Browning said:

well, those are true about any subfields, and I don't expect them to be hard to prove (since we have the power law).

Yeah, okay I think you're right that it shouldn't make it any more difficult here.

Patrick Lutz (Aug 05 2020 at 04:09):

Actually, maybe I should remove that assumption from the lemma statements

Patrick Lutz (Aug 05 2020 at 04:09):

Just for the first of the two lemmas I mean

Patrick Lutz (Aug 05 2020 at 04:09):

The second doesn't totally make sense without it

Patrick Lutz (Aug 05 2020 at 04:10):

unless you replace αF\alpha \notin F with α\alpha \notin set.range (algebra.map F E)

Thomas Browning (Aug 05 2020 at 04:10):

the second can also be rephrased as saying that if F and F' are two subfields, and F is a proper subset of F' then the dimension decreases

Patrick Lutz (Aug 05 2020 at 04:11):

True. Would any of those be useful to have later? Right now those lemmas are only needed to prove the primitive element theorem.

Thomas Browning (Aug 05 2020 at 04:14):

maybe, but I would guess not for this project

Kevin Buzzard (Aug 05 2020 at 07:36):

Just to let you know that mathlib has subsemirings (bundled) and subrings (unbundled) but we plan on bundling subrings soon (there's a branch bundled-subrings or bundled_subrings) and then I guess the idea would be to bundle subfields, although some people might say that it's better to have subfields as a predicate on subrings

Patrick Lutz (Aug 05 2020 at 17:29):

Kevin Buzzard said:

Just to let you know that mathlib has subsemirings (bundled) and subrings (unbundled) but we plan on bundling subrings soon (there's a branch bundled-subrings or bundled_subrings) and then I guess the idea would be to bundle subfields, although some people might say that it's better to have subfields as a predicate on subrings

Yeah, we noticed that subgroups were just bundled. I think bundling subfields would be nice, having them as a predicate is also probably fine.

Thomas Browning (Aug 05 2020 at 22:05):

Patrick Lutz said:

Thomas Browning How easy is it to transfer facts about adjoining elements to a subfield FF of a field EE, thought of as an algebra map from FF to EE, to the subfield of EE given by the image of this algebra map? Basically, how easy is it to fill in the sorries in primitive_element_inf?

One sorry down

Patrick Lutz (Aug 05 2020 at 22:37):

By the way, if f is a polynomial over F and E is an algebra over F, does mathlib already have a definition of the set of roots of f in E? It's easy to define using polynomial.eval\2 but I'm wondering if it's already done somewhere

Thomas Browning (Aug 05 2020 at 22:45):

I'm not sure

Patrick Lutz (Aug 05 2020 at 23:00):

Also, do we have anything saying that if STS \subseteq T then adjoin F S is a subset of adjoin F T?

Thomas Browning (Aug 05 2020 at 23:06):

No, but I just added it: adjoin.mono

Patrick Lutz (Aug 05 2020 at 23:12):

Actually, I realized I might not need it. But it might be good to have anyway

Thomas Browning (Aug 06 2020 at 02:46):

Finished the last sorry in "primitive_element_inf", and I might try to take care of the sorry in "primitive_element_inf_aux"

Patrick Lutz (Aug 06 2020 at 02:48):

Thomas Browning said:

Finished the last sorry in "primitive_element_inf", and I might try to take care of the sorry in "primitive_element_inf_aux"

You mean the one about EE being a separable extension of F[α]F[\alpha] (I think that's the only one left in that proof)? If so, I made a statement that would suffice in separable.lean

Thomas Browning (Aug 06 2020 at 06:07):

proved it

Patrick Lutz (Aug 06 2020 at 16:45):

Thomas Browning said:

proved it

Nice! Soon the only parts of the primitive element theorem that are left will be the hard parts

Jalex Stark (Aug 06 2020 at 18:02):

does "hard parts" mean "parts with mathematical content"?

Patrick Lutz (Aug 06 2020 at 18:03):

Jalex Stark said:

does "hard parts" mean "parts with mathematical content"?

More or less.

Patrick Lutz (Aug 06 2020 at 18:05):

Basically the two sorries in primitive_element_two_inf and primitive_element_two_aux in the code here

Patrick Lutz (Aug 06 2020 at 19:37):

@Thomas Browning @Jordan Brown Should we introduce some notation for adjoin and adjoin_simple? It might be nice to be able to write F[\a] rather than adjoin_simple F \a

Jordan Brown (Aug 06 2020 at 19:51):

That does sound like a good idea, I'm still not totally sure about how to correctly introduce notation but I think that trying to introduce notation that conforms to normal mathematical usage will make everything much easier to understand

Patrick Lutz (Aug 06 2020 at 21:13):

Okay, I've tried adding notation. You should now be able to write F[\a] for adjoin_simple F \a and F[\a, \b] for adjoin F {\a, \b}. Let me know if the notation ever doesn't work correctly

Patrick Lutz (Aug 06 2020 at 21:15):

Also, @Thomas Browning can you take a look at the stuff I added to adjoin.lean here to make sure it's not redundant/there aren't any other problems with it

Thomas Browning (Aug 06 2020 at 21:42):

looks good to me

Patrick Lutz (Aug 06 2020 at 21:51):

I've tried changing stuff to use the new notation. One thing that is slightly annoying is that you often still need to write (F[a]) in situations where you'd rather just write F[a] (e.g. when it is an argument to some other theorem). I imagine that this has to do with how strong the binding power is in the declaration of the notation but I don't know how this stuff works or how to change it effectively.

Patrick Lutz (Aug 06 2020 at 23:21):

Does it sound reasonable to define F[a, b] as F[a][b] rather than as F[{a, b}]? I think that notation would be a lot easier to define

Patrick Lutz (Aug 06 2020 at 23:23):

oh, it's kind of cool that now VSCode displays the type of things using the notation F[a]

Patrick Lutz (Aug 06 2020 at 23:49):

It looks like it's not that hard to get notation that does the following: F[a, b, c, d] turns into adjoin_simple (adjoin_simple (adjoin_simple (adjoin_simple F a) b) c) d and so on, for any number of arguments. But I can't figure out how to set up notation so that F[a, b, c, d] turns into adjoin F {a, b, c, d}

Patrick Lutz (Aug 06 2020 at 23:50):

Also it might be nice to have notation for adjoin F S. But if I just define F[S] to be adjoin F S and F[a] to be adjoin_simple F a then lean complains to me that it can't figure out which one to use in which situation.

Kenny Lau (Aug 07 2020 at 00:27):

Kenny Lau said:

#3654 Kevin Buzzard Johan Commelin Chris Hughes

merged

Thomas Browning (Aug 07 2020 at 00:50):

Patrick Lutz said:

It looks like it's not that hard to get notation that does the following: F[a, b, c, d] turns into adjoin_simple (adjoin_simple (adjoin_simple (adjoin_simple F a) b) c) d and so on, for any number of arguments. But I can't figure out how to set up notation so that F[a, b, c, d] turns into adjoin F {a, b, c, d}

You could do something hacky where you manually define notation for each possible number of elements

Patrick Lutz (Aug 07 2020 at 16:34):

The PRs #3720 and #3717 which were just made should help make some of our proofs shorter once they are merged. I think we should consider temporarily copying the code from those PRs into our project and removing it once the changes are merged

Patrick Lutz (Aug 07 2020 at 16:57):

I've added some stuff from those PRs to our code, which we can take out once they are merged.

Patrick Lutz (Aug 08 2020 at 02:15):

We now have slightly better notation. You should now be able to write just F[a] instead of having to write (F[a]) all the time because I have increased the binding power of [ in that notation to be std.prec.max_plus (i.e. I've turned the amp to 11)

Patrick Lutz (Aug 08 2020 at 02:16):

I think I can also probably figure out how to make F[a, b, c] mean adjoin F {a, b, c} but I'm not quite there yet.

Thomas Browning (Aug 08 2020 at 07:08):

I think that when proving the PET, we don't need to consider the splitting field of f*g, but just the splitting field of g (since all of the roots of the gcd lie in the splitting field of g).

Patrick Lutz (Aug 08 2020 at 07:10):

Thomas Browning said:

I think that when proving the PET, we don't need to consider the splitting field of f*g, but just the splitting field of g (since all of the roots of the gcd lie in the splitting field of g).

Yeah, I think you're right.

Patrick Lutz (Aug 08 2020 at 07:12):

By the way, I thought I was close to proving adjoin_dim_lt but I think I need to understand smul_tower better actually. I can't seem to escape wanting to know that if you change the base field to an isomorphic one then the dimension stays the same.

Thomas Browning (Aug 08 2020 at 07:13):

The result is reduced to showing that dimension of F[alpha]/F is greater than 1, so why do you need to deal with changing the base field?

Thomas Browning (Aug 08 2020 at 07:15):

It seems to me like the crux of the matter is dealing with a basis of cardinality 1.

Patrick Lutz (Aug 08 2020 at 07:15):

I want to use findim_lt from #3720

Patrick Lutz (Aug 08 2020 at 07:16):

If you use reasoning about the basis directly then it shouldn't be a problem

Thomas Browning (Aug 08 2020 at 07:16):

oh I see

Patrick Lutz (Aug 08 2020 at 07:16):

But I was trying to be clever and use the fact that the dimension of F over itself is 1

Patrick Lutz (Aug 08 2020 at 07:17):

Maybe I should just do it the other way. But I wanted to avoid dealing with fintype

Patrick Lutz (Aug 08 2020 at 07:21):

Actually, I think I may have just been misunderstanding submodule

Patrick Lutz (Aug 08 2020 at 07:21):

maybe it's not so bad

Patrick Lutz (Aug 08 2020 at 07:43):

Okay, maybe actually it is lol

Kevin Buzzard (Aug 08 2020 at 16:06):

Instead of copying the code, just make your local mathlib dependency the branch

Patrick Lutz (Aug 08 2020 at 18:09):

@Kevin Buzzard That's good advice for the future. For now, the PR has been merged so I'll just delete the extra stuff.

Patrick Lutz (Aug 09 2020 at 02:35):

adjoin_findim_lt is done

Patrick Lutz (Aug 09 2020 at 02:35):

It turned out that mathlib had some lemmas for dealing with linearly indepdent singletons and for singletons which span the whole space.

Patrick Lutz (Aug 09 2020 at 03:07):

Patrick Lutz said:

adjoin_findim_lt is done

I actually meant adjoin_dim_lt

Patrick Lutz (Aug 09 2020 at 03:45):

I'm thinking about changing the definition for the roots in EE of a polynomial ff over FF to be roots f E rather than the current roots F E f. Does that seem reasonable?

Thomas Browning (Aug 09 2020 at 04:51):

Seems reasonable to me

Patrick Lutz (Aug 09 2020 at 05:51):

We're at 150 commits btw

Patrick Lutz (Aug 09 2020 at 16:30):

Okay, I changed the definition of roots. You should now write roots f E for the roots of the polynomial f in the field E

Kevin Buzzard (Aug 09 2020 at 19:11):

I was just watching Kenny live stream the definition of algebraic closure on the Discord

Patrick Lutz (Aug 09 2020 at 19:12):

Kevin Buzzard said:

I was just watching Kenny live stream the definition of algebraic closure on the Discord

What is the discord?

Kevin Buzzard (Aug 09 2020 at 19:13):

There's a Xena project discord server. Kenny is live streaming Galois theory with some other Imperial undergraduates

Kenny Lau (Aug 09 2020 at 19:14):

https://discord.gg/cNGnzX

Kevin Buzzard (Aug 09 2020 at 19:14):

I'm not at a computer right now so can't generate an invite

Kevin Buzzard (Aug 09 2020 at 19:14):

I'm going to turn this invite off in a few days

Kenny Lau (Aug 09 2020 at 19:15):

this invite link expires in 1 day

Kenny Lau (Aug 09 2020 at 19:15):

just like any other

Kevin Buzzard (Aug 09 2020 at 19:16):

Oh ok the link on my Twitter never expired but I just removed it from my bio

Patrick Lutz (Aug 10 2020 at 08:54):

We have finished proving the primitive element theorem!

Patrick Lutz (Aug 10 2020 at 08:55):

https://github.com/pglutz/galois_theory/blob/5b8a97dd884568aa76d0cb40a99df7b8ab92cb29/src/primitive_element.lean#L622

Kevin Buzzard (Aug 10 2020 at 12:36):

Nice! You should get it into mathlib! This is like saying you proved a theorem on paper but couldn't be bothered to write it up properly. In a year's time you have lost the piece of paper, and your code doesn't compile any more with mathlib master

Kevin Buzzard (Aug 10 2020 at 12:37):

Mathlib master gets fixed when breaking changes to mathlib are made

Kevin Buzzard (Aug 10 2020 at 12:37):

And lean 4 mathlib will initially use automation to transfer lean 3 statements over

Kevin Buzzard (Aug 10 2020 at 12:37):

So your proof is guaranteed to live

Kevin Buzzard (Aug 10 2020 at 12:38):

I'm sure this was your plan anyway but years of experience of my own mistakes in this matter have made me very vocal in making sure that others don't make the same mistakes as I do

Patrick Lutz (Aug 10 2020 at 15:11):

Do you have any advice about how we should go about getting it into mathlib? We were planning to make a series of smaller PRs

Thomas Browning (Aug 10 2020 at 15:13):

Basically, there are some smaller lemmas which might have good homes in mathlib, but apart from that there are two big files (adjoin.lean and primitive_element.lean) which would probably need to stay as their own files. (Just general info for someone answering your question Patrick).

Jalex Stark (Aug 10 2020 at 16:10):

The goal with splitting up PRs is to make them easier to review

Patrick Massot (Aug 10 2020 at 18:21):

Kevin Buzzard said:

I'm sure this was your plan anyway but years of experience of my own mistakes in this matter have made me very vocal in making sure that others don't make the same mistakes as I do

As a collaborator on some of Kevin's mistakes, I can only add my voice to his: PR before it's too late or you'll only have regrets and dead code.

Kevin Buzzard (Aug 10 2020 at 22:21):

PR's of the form "here are some random additions to random mathlib files" are fine, and if they are short then they are often not hard to review. PR's of the form "here is one big new standalone file" are probably also preferred to monster PR's which achieve one big goal by making lots of changes to lots of files.

Patrick Lutz (Aug 11 2020 at 04:55):

@Thomas Browning @Jordan Brown @Rahul Dalal As I mentioned last week, I can't go to our regular meeting tomorrow. We can either reschedule to later in the day or I can skip the meeting.

Thomas Browning (Aug 11 2020 at 05:03):

Later works for me (I just have office hours 7pm-8pm)

Patrick Lutz (Aug 11 2020 at 05:12):

How about 5 pm?

Rahul Dalal (Aug 11 2020 at 19:37):

I think I might also not be able to make it. I am very behind where I wanted to be on some stuff I really need to finish today. Sorry for the very late notice. I was hoping to be done by now.

Jordan Brown (Aug 13 2020 at 20:03):

Does the adjoin file have anything in it that explicitly states that F[alpha] is a vector space over F? We have that it is an algebra, but I cannot find a statement that it is a vector space and library_search hasn't given me any way to convert something from an algebra over a field to a vector space

Kenny Lau (Aug 13 2020 at 20:19):

import ring_theory.adjoin

variables (F : Type*) [field F] {A : Type*} [ring A] [algebra F A] (s : set A)

#check (by apply_instance : vector_space F (algebra.adjoin F s))

Kenny Lau (Aug 13 2020 at 20:19):

vector_space is a class

Kenny Lau (Aug 13 2020 at 20:19):

you don't refer to the instances by name

Kenny Lau (Aug 13 2020 at 20:20):

Lean just figures them out using typeclass inference

Thomas Browning (Aug 13 2020 at 20:44):

that's ring_theory.adjoin, but the same holds for the field adjoin. Lean should be able to figure it out automatically.

Thomas Browning (Aug 14 2020 at 19:32):

What time were we going to meet today? 4pm?

Patrick Lutz (Aug 14 2020 at 19:39):

that was your suggestion. I'm not sure we ever decided on a time

Patrick Lutz (Aug 14 2020 at 19:40):

somewhere between 3-5 is best for me

Patrick Lutz (Aug 14 2020 at 19:40):

(as the starting time for the meeting)

Patrick Lutz (Aug 14 2020 at 19:40):

though I'm not sure how much we have to talk about

Thomas Browning (Aug 14 2020 at 21:51):

I'm still in the middle of grading my final exam, so maybe it's best to hold off until Tuesday at the usual time?

Patrick Lutz (Aug 14 2020 at 22:06):

sounds good

Jordan Brown (Aug 16 2020 at 17:19):

Lean seems to not recognize adjoin_root.mk, even though I imported ring_theory.adjoin_root; is there something else I need to import?

Thomas Browning (Aug 16 2020 at 19:02):

I think it's just adjoin_root (polynomial)

Kevin Buzzard (Aug 16 2020 at 19:20):

Jordan Brown said:

Lean seems to not recognize adjoin_root.mk, even though I imported ring_theory.adjoin_root; is there something else I need to import?

Explicit error message or it didn't happen.

Kevin Buzzard (Aug 16 2020 at 19:21):

docs#adjoin_root.mk

Jordan Brown (Aug 17 2020 at 03:04):

Thomas, I think that just gives the resulting ring; I want to use the quotient homomorphism to the ring

Jordan Brown (Aug 17 2020 at 03:05):

The error message is "invalid 'begin-end' expression, ',' expected", which makes me think that it just does not recognize adjoin_root.mk at all

Thomas Browning (Aug 17 2020 at 03:12):

post the code that gives the message?

Jordan Brown (Aug 17 2020 at 03:45):

''' import subfield_stuff
import group_theory.subgroup
import field_theory.minimal_polynomial
import linear_algebra.dimension
import linear_algebra.finite_dimensional
import ring_theory.adjoin_root
import data.zmod.basic
import data.polynomial.basic
import adjoin

variables (F : Type) [field F] {E : Type} [field E] [algebra F E] (S : set E)(α : E) (h : is_integral F α)

lemma adjunction_degree_finite : finite_dimensional F (adjoin_root (minimal_polynomial h)) :=
begin
let minimal:=minimal_polynomial h,
let degree:=polynomial.nat_degree minimal,
let x:polynomial F:= polynomial.X,
let S:= {n: ℕ| n<degree},
let η := λ n:S, adjoin_root.​mk (x^(n:ℕ)),
sorry
end'''

Jordan Brown (Aug 17 2020 at 03:47):

(I intend to just add it to adjoin itself eventually, but that should not affect this particular issue)

Kenny Lau (Aug 17 2020 at 05:45):

#backticks

Kevin Buzzard (Aug 17 2020 at 07:56):

That error means you've made a syntax error, not that lean doesn't recognise some definition or theorem

Kevin Buzzard (Aug 17 2020 at 07:58):

But code posted without backticks is hard to read because all the _ and * get initerpreted as syntax highlighting

Thomas Browning (Aug 17 2020 at 16:48):

@Jordan Brown Are you sure that you want to be using adjoin_root.mk (x^n) here? adjoin_root.mk (x^n) seems like it would give the ring homomorphism F[x] -> F[x]/(x^n) which I don't think is what you want. Also, one issue might be that lean can't figure out the field/ring that you are working over when you write let η := λ n:S, adjoin_root.​mk (x^(n:ℕ))

Jordan Brown (Aug 18 2020 at 00:53):

Ah yes, it seems like it works if I specify the polynomial I am taking the quotient of before applying the function to x^n

Jordan Brown (Aug 18 2020 at 00:54):

And thanks for the reminders about backticks, I seem to always forget how to use them correctly

Thomas Browning (Aug 19 2020 at 00:30):

Ok, I've removed the subfield assumption from primitive_element_two_inf_key

Thomas Browning (Aug 19 2020 at 00:30):

@Patrick Lutz What's next in the quest for subfield removal?

Patrick Lutz (Aug 19 2020 at 01:36):

Thomas Browning said:

Patrick Lutz What's next in the quest for subfield removal?

I'll push the stuff from the other branch. Also, I had another idea about this. Maybe instead of (or in addition to) having stuff about the isomorphism between F and its image we could (1) show that ulift F is an isomorphism and (2) show that everything in the statement of the primitive element theorem is invariant under isomorphism

Patrick Lutz (Aug 19 2020 at 01:54):

@Thomas Browning Okay, I've pushed the stuff I did

Patrick Lutz (Aug 19 2020 at 01:54):

I think it still needs some cleaning up though

Patrick Lutz (Aug 19 2020 at 01:54):

and if it's okay with you, I would prefer to make adjoin_simple_is_separable it's own lemma

Patrick Lutz (Aug 19 2020 at 01:54):

maybe in the adjoin.lean file

Thomas Browning (Aug 19 2020 at 02:11):

sure, go for it

Patrick Lutz (Aug 19 2020 at 03:42):

hmmm, I think replacing my_roots with (f.map (algebra_map F E)).roots may actually be a little annoying. But maybe just because I don't really understand how to use finsets.

Patrick Lutz (Aug 19 2020 at 03:44):

It looks like if s and t are finsets I'm not allowed to do things like s × t → α: Lean complains that it expected s and t to have type Type u but instead they have type finset E

Thomas Browning (Aug 19 2020 at 04:11):

could you replace my_roots with ↑(polynomial.map ϕ f).roots to preserve the type?

Patrick Lutz (Aug 19 2020 at 04:12):

Lean doesn't seem to understand the type coercion there

Patrick Lutz (Aug 19 2020 at 04:12):

I've asked a question about this on the new members stream though

Patrick Lutz (Aug 19 2020 at 04:12):

so I'll see what they say

Patrick Lutz (Aug 19 2020 at 06:57):

@Thomas Browning I have removed all references to my_roots from primitive_element_two_aux (which I've renamed to primitive_element_two_aux' to make the code still compile). If you also change primitive_element_two_inf_key then we can remove my_roots completely.

Thomas Browning (Aug 19 2020 at 17:18):

I think I've finished taking out my_roots

Patrick Lutz (Aug 19 2020 at 18:54):

I propose that we move submodule_restrict_field, adjoin_findim_of_findim, adjoin_findim_of_findim_base, algebra_findim_lt, adjoin_dim_lt and adjoin_inf_of_inf from primitive_element.lean to adjoin.lean

Thomas Browning (Aug 19 2020 at 19:11):

Sounds good.

Patrick Lutz (Aug 19 2020 at 19:47):

I wonder if we should totally get rid of adjoin_simple and just adjoin. We don't have to write adjoin F {a} everywhere because we can keep the notation F[a].

Patrick Lutz (Aug 19 2020 at 19:47):

And we could probably get rid of a bunch of duplicate lemmas

Patrick Lutz (Aug 19 2020 at 19:48):

It's a little annoying that we have two versions of so many things: one for adjoin and one for adjoin_simple

Patrick Lutz (Aug 19 2020 at 19:56):

although I guess sometimes it's nice to be able to avoid writing {a} when invoking a theorem.

Thomas Browning (Aug 19 2020 at 20:21):

I guess that's fair since there is subfield.closure if you want a more general version

Thomas Browning (Aug 21 2020 at 16:28):

One question though, how do you plan on handling adjoining two elements? Just as (F[a])[b] ?

Johan Commelin (Aug 21 2020 at 16:36):

You can adjoin {a,b} as well

Johan Commelin (Aug 21 2020 at 16:36):

And the two are not defeq (-;

Thomas Browning (Aug 21 2020 at 16:55):

Oh nevermind. I thought that Patrick was advocating keeping just adjoin_simple, rather than keeping just adjoin. I totally understand now.

Thomas Browning (Aug 22 2020 at 20:24):

@Patrick Lutz I'm going to be away camping during the next few days, so I won't be able to attend the Tuesday meeting

Patrick Lutz (Aug 23 2020 at 02:00):

@Thomas Browning Okay, let's just skip Tuesday this week then.

Thomas Browning (Aug 23 2020 at 02:06):

Sure. By the way, I've pushed an initial chunk to mathlib at #3913
Do you have permissions to make changes while I'm gone?

Jalex Stark (Aug 23 2020 at 04:14):

everyone who asks for mathlib permissions gets permission to push to every non-master branch of mathlib. pushing to the relevant branch is how you update a PR.

Thomas Browning (Aug 23 2020 at 04:22):

Ah, makes sense. That's good to hear.

Thomas Browning (Aug 28 2020 at 22:52):

Ok, I've refactored primitive_element so that the "same-universe version" doesn't require subfield_stuff

Thomas Browning (Aug 28 2020 at 22:53):

Also, @Patrick Lutz , it looks like Lint failed again on the new notation

Thomas Browning (Aug 29 2020 at 01:22):

Actually, I'm not entirely sure why the linter is given an error. The error message is super weird.

Thomas Browning (Aug 29 2020 at 02:09):

Also, there isn't any error when I put #lint at the end of the file in my VScode

Patrick Lutz (Aug 29 2020 at 02:13):

@Thomas Browning Yeah, I don't get the lint error at all.

Patrick Lutz (Aug 29 2020 at 02:13):

@Kevin Buzzard do you have any idea what could cause this? We're getting a linter error in this pull request: #3913

Patrick Lutz (Aug 29 2020 at 02:20):

It looks like it has something to do with set.insert

Kevin Buzzard (Aug 29 2020 at 07:09):

I don't know anything about the linter and I'm on mobile and can't figure out how to see the output. I would just ask the experts

Kevin Buzzard (Aug 29 2020 at 16:55):

hah I've now looked at the output. Yeah, you broke the linter :-) You get an achievement! Definitely beyond my pay grade!

Patrick Lutz (Aug 30 2020 at 17:50):

@Thomas Browning @Jordan Brown I made a comment on github saying that I think to address the problems with notation we should pick one of the brackets here to use for field extensions. It's not a great solution and I would be happy to hear alternatives. I would like to avoid something bizarre like F[ (a) ] or F-(a)-. I might be willing to accept F(⟨α⟩) though.

Patrick Lutz (Aug 30 2020 at 17:51):

I kind of miss just being able to type F[a]

Thomas Browning (Aug 30 2020 at 18:05):

I think your idea makes the most sense. Some sort of curved bracket would be fine?

Kevin Buzzard (Aug 30 2020 at 18:16):

You could find some exotic unicode square bracket if you want to use F[a]. You can't use [ and ], they are already over-used by CS aspects of Lean :-(

Thomas Browning (Aug 30 2020 at 19:12):

Ok, I've pushed some new brackets

Kyle Miller (Aug 30 2020 at 19:20):

This might be a bit out there, but you might consider something like

instance : has_coe_to_fun (field F) :=
⟨_, adjoin

Then you could write F {a} (or F{a}) for adjoin F {a}

Patrick Lutz (Aug 30 2020 at 19:57):

Kyle Miller said:

This might be a bit out there, but you might consider something like

instance : has_coe_to_fun (field F) :=
⟨_, adjoin

Then you could write F {a} (or F{a}) for adjoin F {a}

I'm a little worried this could create problems down the line if a field and a set occur as arguments to a theorem and Lean tries to interpret them as a field extension.

Kyle Miller (Aug 30 2020 at 20:00):

That shouldn't be a problem, but the opposite problem might: if you intended to pass a field extension as an argument, but it'll be interpreted as a field and a set as two separate arguments unless you use parentheses: foo (F{a})

Patrick Lutz (Aug 30 2020 at 20:02):

Kevin Buzzard said:

You could find some exotic unicode square bracket if you want to use F[a]. You can't use [ and ], they are already over-used by CS aspects of Lean :-(

Surprisingly, F[a] didn't cause any problems (with either compiling mathlib or the linter). It was only discarded because it conflicts with the standard math notation where F(a) should mean adjoining a to F as a field and F[a] should mean adjoining a to F as a ring. The Lean problems actually only came from the notations F(a) and F[(a)]

Patrick Lutz (Aug 30 2020 at 20:02):

Kyle Miller said:

That shouldn't be a problem, but the opposite problem might: if you intended to pass a field extension as an argument, but it'll be interpreted as a field and a set as two separate arguments unless you use parentheses: foo (F{a})

Yeah, but we set the precedence very high to deal with that, which leads to the other type of problem.

Kyle Miller (Aug 30 2020 at 20:09):

Patrick Lutz said:

Kyle Miller said:

That shouldn't be a problem, but the opposite problem might: if you intended to pass a field extension as an argument, but it'll be interpreted as a field and a set as two separate arguments unless you use parentheses: foo (F{a})

Yeah, but we set the precedence very high to deal with that, which leads to the other type of problem.

With what I was saying, you don't change the precedence of anything, because the notation is simply function application notation. The instance gives fields an interpretation as a function whose domain is sets of elements to adjoin.

Kyle Miller (Aug 30 2020 at 20:12):

It's fine to reject the idea -- I just want to make sure you're rejecting what I'm proposing (it's a solution that uses has_coe_to_fun rather than notation)

Patrick Lutz (Aug 30 2020 at 21:27):

@Kyle Miller Yeah, I think I understand your proposal. It may be reasonable, but I personally find it annoying to have to frequently put parentheses around F{a} and the curly brackets are not typically used in normal math for this kind of thing (although there is a certain appeal to writing the closure of F and S as the concatenation F S). This seems to me to be a situation where the ideal option is not available and every alternative has some advantages and disadvantages. I personally favor using unicode variants of the round parentheses, but I'm not sure if that is actually the best choice.

Patrick Lutz (Aug 30 2020 at 21:29):

With my previous reply I meant that with the precedence set low, F[a] has the same issue you described where you often have to write (F[a]) but with the precedence set high, Lean may start thinking that other things mean field extension even when they don't.

Thomas Browning (Aug 30 2020 at 22:18):

@Patrick Lutz There's something going on in the adjoin file that I just noticed. Remember all those ( _ : set E)'s? Those are actually casting from a subalgebra type to a subset type, I think. So some of the lemmas are equalities of subalgebras (like adjoin_singleton), whereas some of the lemmas are equalities of subsets (like adjoin_adjoin_left).

Thomas Browning (Aug 30 2020 at 22:18):

Is there anything bad about this?

Thomas Browning (Aug 30 2020 at 22:19):

adjoin_adjoin_left is a little weird because it's basically saying that something of type subalgebra (adjoin F E) E equals something of type subalgebra F E (I think), which is why there's this casting to set E

Patrick Lutz (Aug 30 2020 at 22:41):

I don't immediately see anything bad about it, but I wouldn't necessarily know if there was. If you know that two things are equal as subalgebras then presumably you also know they are equal as sets. But in cases where two things can't be equal as subalgebras for type reasons (as in the case of adjoin_adjoin_left (or adjoin_twice as I still think of it)), it doesn't seem unreasonable to me to instead just prove they are equal as setss. The main downside that I see is that from a UX perspective it's not great to sometimes have to type ( : set E). But maybe there is a better way to do things that I don't know about.

Patrick Lutz (Aug 30 2020 at 22:44):

I guess ultimately the hope is to replace all of this stuff with the intermediate_field type? So adjoin F S and adjoin (F S) T can be equal as things of type intermediate_field F E. But I'm not sure if I've understood that correctly.

Thomas Browning (Sep 02 2020 at 14:31):

@Patrick Lutz Now that the basic adjoin lemmas are in mathlib, what's the best plan for refactoring the rest of what we have? I was thinking that it might be a good idea to make a new primitive element theorem file, and copy over the proof in terms of the new mathlib field adjoin, and add any lemmas that we don't have yet.

Patrick Lutz (Sep 02 2020 at 16:35):

Yeah, that sounds okay. We'll probably need to modify some of the remaining theorems in adjoin.lean

Patrick Lutz (Sep 02 2020 at 16:45):

Also, should we prove that F(a) is equal to \top in the lattice of subalgebras rather than subsets?

Patrick Lutz (Sep 02 2020 at 17:38):

I've started a new file in the repo for this purpose

Patrick Lutz (Sep 02 2020 at 17:38):

Make sure to upgrade mathlib to use it

Patrick Lutz (Sep 02 2020 at 17:38):

There are still lots of errors also

Patrick Lutz (Sep 02 2020 at 17:39):

and it seems like we may end up having to write (F(a) : set E) in a lot more places, which is annoying

Patrick Lutz (Sep 02 2020 at 19:02):

oops, turns out I forgot to git add the new file

Thomas Browning (Sep 02 2020 at 20:35):

I'll take a stab at some of the errors

Patrick Lutz (Sep 02 2020 at 20:51):

Oh, I've also been working on this

Patrick Lutz (Sep 02 2020 at 20:51):

let me push my changes

Thomas Browning (Sep 02 2020 at 20:51):

I've taken care of the first error

Thomas Browning (Sep 02 2020 at 20:52):

will this conflict with your stuff?

change β = (-p.coeff 0 / p.coeff 1) at last_step,
change β  Fγ,
rw last_step,
exact subtype.mem (-p.coeff 0 / p.coeff 1),

Patrick Lutz (Sep 02 2020 at 20:53):

no I don't think so

Patrick Lutz (Sep 02 2020 at 20:53):

I just pushed

Patrick Lutz (Sep 02 2020 at 20:53):

Try pulling and let me know if there are any problems

Patrick Lutz (Sep 02 2020 at 20:54):

One very annoying thing I've discovered:

have β_in_Fαβ : β  Fα, β := field.subset_adjoin F (set.insert α (set.insert β )) (set.mem_insert_of_mem α (set.mem_insert β )),

Patrick Lutz (Sep 02 2020 at 20:54):

The only way I can see to show that b \in F(a, b) is pretty long

Patrick Lutz (Sep 02 2020 at 20:54):

It would only get worse for c \in F(a, b, c)

Thomas Browning (Sep 02 2020 at 20:54):

oh dear

Patrick Lutz (Sep 02 2020 at 20:54):

Not sure what to do about it though

Patrick Lutz (Sep 02 2020 at 20:56):

Also, I'm having to write (F(a) : set E) everywhere

Thomas Browning (Sep 02 2020 at 20:57):

If you are fine with underscores:
have β_in_Fαβ : β ∈ F⟮α, β⟯ := field.subset_adjoin F _ (set.mem_insert_of_mem α _),

Patrick Lutz (Sep 02 2020 at 21:00):

It's definitely a bit better

Patrick Lutz (Sep 02 2020 at 21:00):

The whole thing where F(a, b) doesn't mean adjoin F {a, b} is kind of irritating though

Patrick Lutz (Sep 02 2020 at 21:00):

I really wish we could get notation that did that

Thomas Browning (Sep 02 2020 at 21:01):

we haven't asked on maths about this yet have we?

Thomas Browning (Sep 02 2020 at 21:02):

there might be some foldr guru who knows how to do it

Patrick Lutz (Sep 02 2020 at 21:02):

Yeah, that's a good idea

Patrick Lutz (Sep 02 2020 at 21:06):

Do you want to, or should I?

Thomas Browning (Sep 02 2020 at 21:07):

I can do it if you want

Patrick Lutz (Sep 02 2020 at 21:16):

sure

Thomas Browning (Sep 02 2020 at 21:18):

done. feel free to add anything.

Patrick Lutz (Sep 02 2020 at 21:19):

Okay, I think after my push just now, all the sorries in new_primitive_element.lean represent theorems that are not yet included in mathlib's field_theory.adjoin (and there are no more errors)

Patrick Lutz (Sep 02 2020 at 21:19):

still, a number of things got uglier :(

Thomas Browning (Sep 02 2020 at 21:21):

the separable lemma (and maybe others?) doesn't really belong in field_theory.adjoin since it's much more general

Patrick Lutz (Sep 02 2020 at 21:21):

Yeah, for sure

Patrick Lutz (Sep 02 2020 at 21:21):

I just meant that all the sorries represent things not yet in mathlib

Thomas Browning (Sep 02 2020 at 21:22):

sure

Patrick Lutz (Sep 02 2020 at 21:22):

because currently new_primitive_element only imports from mathlib

Patrick Lutz (Sep 02 2020 at 21:22):

also, I changed all the statements to be showing that F(a) is equal to top as subalgebras rather than subsets of E

Patrick Lutz (Sep 02 2020 at 21:22):

not sure how you feel about that

Patrick Lutz (Sep 02 2020 at 21:23):

It doesn't seem to make anything harder

Thomas Browning (Sep 02 2020 at 21:27):

By the way, it doesn't seem like we use ne_zero_of_ne_zero

Patrick Lutz (Sep 02 2020 at 21:34):

hmm, that might be true

Patrick Lutz (Sep 02 2020 at 21:34):

It was probably used at some point and then the proof was changed

Thomas Browning (Sep 02 2020 at 21:58):

What's the best way to incorporate the new notation? Should we make a branch? If so, is it possible for both of us to contribute to the branch?

Patrick Lutz (Sep 02 2020 at 21:58):

A branch of mathlib or a branch of the galois theory repo?

Patrick Lutz (Sep 02 2020 at 21:59):

If so, is it possible for both of us to contribute to the branch?

Yes

Thomas Browning (Sep 02 2020 at 21:59):

of mathlib

Patrick Lutz (Sep 02 2020 at 21:59):

Yeah, that sounds reasonable

Patrick Lutz (Sep 02 2020 at 21:59):

make a branch of mathlib, push it to the mathlib github and I can get it

Patrick Lutz (Sep 02 2020 at 21:59):

but don't make a PR yet

Thomas Browning (Sep 02 2020 at 22:00):

will do

Thomas Browning (Sep 02 2020 at 22:01):

does "don't make a PR yet" mean: use "git push" rather than "git push origin"?

Patrick Lutz (Sep 02 2020 at 22:02):

Pushing shouldn't change. Just don't make a pull request on mathlib

Patrick Lutz (Sep 02 2020 at 22:02):

a pull request is a request to merge the branch with the master branch

Patrick Lutz (Sep 02 2020 at 22:03):

the first time you push you should do git push -u origin name_of_branch_goes_here and in subsequent times you should only need to do git push

Patrick Lutz (Sep 02 2020 at 22:03):

as usual

Patrick Lutz (Sep 02 2020 at 22:03):

but that doesn't have anything to do with making a PR

Thomas Browning (Sep 02 2020 at 22:03):

what step of this process (https://leanprover-community.github.io/contribute/index.html) is the request to merge? Is it the "Visit mathlib on GitHub to see an invitation to open a PR based on what you just did" step?

Patrick Lutz (Sep 02 2020 at 22:03):

Patrick Lutz said:

Pushing shouldn't change. Just don't make a pull request on mathlib

I meant github not mathlib

Patrick Lutz (Sep 02 2020 at 22:04):

Thomas Browning said:

what step of this process (https://leanprover-community.github.io/contribute/index.html) is the request to merge? Is it the "Visit mathlib on GitHub to see an invitation to open a PR based on what you just did" step?

Yes

Thomas Browning (Sep 02 2020 at 22:04):

ah, I see

Patrick Lutz (Sep 02 2020 at 22:05):

I guess I understand why it's confusing if you're just looking at those instructions

Patrick Lutz (Sep 02 2020 at 22:06):

"Pull request" is a term in version control and on github it only happens when you click the button on github that says "Pull Request" (or something like that)

Thomas Browning (Sep 02 2020 at 22:13):

Ok, I think that there should be a "primitive_element_theorem" branch now

Patrick Lutz (Sep 02 2020 at 22:33):

Yeah, I see it

Patrick Lutz (Sep 02 2020 at 22:48):

Is there any way we could get F(a)(b) to have a coercion to type subalgebra F E?

Thomas Browning (Sep 02 2020 at 23:00):

I was hoping for the same thing

Thomas Browning (Sep 02 2020 at 23:01):

basically, you need subalgebra F(a) E to have a coercion to subalgebra F E

Thomas Browning (Sep 02 2020 at 23:01):

that sounds doable, I think

Patrick Lutz (Sep 02 2020 at 23:03):

but it's not already in mathlib?

Patrick Lutz (Sep 02 2020 at 23:04):

oh wait, dumb question probably

Patrick Lutz (Sep 02 2020 at 23:05):

well, if you know E and L are F algebras and K is a subalgebra of E over L then does mathlib already know K is also a subalgebra of E over F?

Thomas Browning (Sep 02 2020 at 23:07):

(assuming that L is an algebra over F)?

Patrick Lutz (Sep 02 2020 at 23:08):

"if you know E and L are F algebras"

Patrick Lutz (Sep 02 2020 at 23:08):

although I guess we need some compatability condition on the algebra maps

Patrick Lutz (Sep 02 2020 at 23:09):

:/

Thomas Browning (Sep 02 2020 at 23:09):

for now, I think it's fine to make a special instance for adjoin

Patrick Lutz (Sep 02 2020 at 23:09):

sounds good

Patrick Lutz (Sep 03 2020 at 20:55):

I pushed a new commit to the mathlib branch that removes all sorries except for stuff about being separable and inclusion.whatever stuff. Some of the proofs are pretty ugly though and the induction proof of primitive element theorem for infinite fields is unfathomably slow

Patrick Lutz (Sep 03 2020 at 22:52):

I realized a bunch of hypotheses of primitive_element_two_aux were not actually being used, so I removed them

Thomas Browning (Sep 03 2020 at 23:40):

cool

Thomas Browning (Sep 03 2020 at 23:40):

however, a lot of this dimension stuff really should be generalized and put in tower.lean, I think

Thomas Browning (Sep 03 2020 at 23:41):

In particular: adjoin_findim_of_findim adjoin_findim_of_findim_base

Patrick Lutz (Sep 03 2020 at 23:53):

Thomas Browning said:

In particular: adjoin_findim_of_findim adjoin_findim_of_findim_base

Yeah, that's probably true. Do you want to do it or should I?

Thomas Browning (Sep 03 2020 at 23:55):

If you could do it, that would be great. I recently added a vector_space.dim version to field.tower, so it shouldn't be too hard to extract the statements about finite_dimensional from that

Patrick Lutz (Sep 03 2020 at 23:55):

By the way, we seem to need this:

def submodule_restrict_field (S : set E) (p : submodule (adjoin F S) E) : submodule F E := {
    carrier := p.carrier,
    zero_mem' := p.zero_mem',
    add_mem' := p.add_mem',
    smul_mem' :=
    begin
        intros c x hx,
        rw algebra.smul_def,
        rw is_scalar_tower.algebra_map_eq F (adjoin F S) E,
        rw ring_hom.comp_apply,
        rw  algebra.smul_def,
        exact p.smul_mem' _ hx,
    end
}

Saying that a submodule of E as an F(a)-module is also a submodule of E as an F-module. It should also probably be proved in more generality than just adjoin

Thomas Browning (Sep 04 2020 at 02:33):

Most of the remaining sorries can be resolved if we just construct a is_scalar_tower F (set.range (algebra_map F E)) E instance, I think

Thomas Browning (Sep 10 2020 at 00:46):

@Patrick Lutz I'm currently not able to compile any lean files in the mathlib branch (the orange bars never go away). Are you experiencing anything similar?

Patrick Lutz (Sep 10 2020 at 02:15):

@Thomas Browning I didn't have that problem but then I pulled your most recent changes and now I do

Patrick Lutz (Sep 10 2020 at 02:15):

Let me try to look into it

Patrick Lutz (Sep 10 2020 at 02:17):

@Thomas Browning Try leanproject get-cache from the command line

Patrick Lutz (Sep 10 2020 at 02:17):

For me that seemed to fix the problem

Patrick Lutz (Sep 10 2020 at 02:17):

Not sure why we normally don't have to do that though

Patrick Lutz (Sep 10 2020 at 02:19):

Ohh, it's because you made a change to a pretty basic file.

Patrick Lutz (Sep 10 2020 at 02:19):

So if you don't do get-cache it's trying to recompile everything that depends on that file.

Patrick Lutz (Sep 10 2020 at 02:19):

Normally when we only change primitive_element_theorem.lean it only needs to try to compile that file.

Patrick Lutz (Sep 10 2020 at 02:21):

leanproject get-cache updates the oleans files (I think copying from the compiled files from the last successful push to github). And apparently VS Code (or whatever) is smart enough to only recompile files that have changed since the oleans files were last updated

Patrick Lutz (Sep 10 2020 at 02:21):

I think running leanproject hooks will mean that you never have to manually run leanproject get-cache again though

Patrick Lutz (Sep 10 2020 at 02:22):

but I'm not entirely certain about that

Thomas Browning (Sep 10 2020 at 02:22):

ahhh, that solved it. I was wondering if that was the problem, but I didn't think so because the bottom of my VSCode seemed to indicate that it was only checking the file that I had open.

Patrick Lutz (Sep 10 2020 at 02:23):

I think to check the file currently open it has to always check all files it depends on for which it doesn't have olean files

Kevin Buzzard (Sep 10 2020 at 05:58):

You can always compile the file on the command line with lean --make path/to/file.lean and see how much other stuff lean wanta to compile before it compiles yours

Thomas Browning (Sep 14 2020 at 19:54):

@Patrick Lutz Is there anything left to do before making the PR?

Patrick Lutz (Sep 14 2020 at 20:02):

Thomas Browning said:

Patrick Lutz Is there anything left to do before making the PR?

Did you ever figure out what the deal was with the "dangerous instance"? And did we ever put the contents of primitive_element.lean in some namespace (probably field)?

Thomas Browning (Sep 14 2020 at 20:14):

well, I think this is what's going on with the dangerous instance. If it's trying to figure out that E/K is finite dimensional, then it might try to apply that instance, but it can't deduce what the base-field F is, so it could get confused or even get into an infinite loop. I changed the instance to a lemma and used haveI in the one spot where it was needed. If you still wanted to have an instance, then you could have it for subalgebras (so that the base-field can be deduced).

Thomas Browning (Sep 14 2020 at 20:14):

we haven't added a namespace yet

Thomas Browning (Sep 14 2020 at 20:15):

(field would be fine, I think)

Patrick Lutz (Sep 14 2020 at 20:18):

Okay, I guess let's add the namespace and then make the PR.

Thomas Browning (Sep 14 2020 at 20:45):

#4153

Johan Commelin (Sep 14 2020 at 20:49):

Unfortunately, there seems to be a conflict already

Thomas Browning (Sep 14 2020 at 20:50):

is it just that other stuff has been added to tower.lean?

Johan Commelin (Sep 14 2020 at 20:52):

It was with tower.lean yes, but I didn't check what exactly

Thomas Browning (Sep 14 2020 at 20:52):

I'm glancing at it now, and it appears that it might just be that the PR somehow didn't include recent additions to tower.lean

Thomas Browning (Sep 14 2020 at 20:54):

I would hope that this can be resolved by just including both

Kevin Buzzard (Sep 14 2020 at 21:00):

you should merge master into your branch maybe?

Patrick Lutz (Sep 14 2020 at 21:12):

Okay, I just merged master into our branch

Patrick Lutz (Sep 14 2020 at 21:12):

hopefully everything should work okay now

Patrick Lutz (Sep 14 2020 at 22:27):

@Thomas Browning It looks like the mathlib build failed because of some problem with separable.lean. I tried looking at it and it seems that there is a rw that no longer applies, perhaps because it follows a dsimp and changing mathlib can change what the goal looks like after dsimp (which I believe is why there is a recommendation against using nonterminal simps and dsimps without only). Anyway, I can't quickly figure out how to fix it so can you take a look?

Patrick Lutz (Sep 14 2020 at 22:31):

Also I think some of the formatting in our PR is not consistent with mathlib guidelines as described here. I think the conventions are also supposed to include putting subgoals within proofs inside brackets (so each have which is not proved in one line should be followed by {...}) which the proof in separable.lean that broke doesn't seem to follow

Thomas Browning (Sep 14 2020 at 22:35):

I'll take a look

Thomas Browning (Sep 14 2020 at 22:43):

Hopefully the separable.lean proofs are fixed now

Thomas Browning (Sep 14 2020 at 23:02):

@Patrick Lutz It looks like there's a problem with some of the finset stuff. (Line 86 in primitive_element.lean)

Kyle Miller (Sep 14 2020 at 23:12):

Do you mind if I take a pass to mathlibify things a bit more?

Patrick Lutz (Sep 14 2020 at 23:56):

Kyle Miller said:

Do you mind if I take a pass to mathlibify things a bit more?

Go for it. That would be great.

Patrick Lutz (Sep 15 2020 at 00:16):

Thomas Browning said:

Patrick Lutz It looks like there's a problem with some of the finset stuff. (Line 86 in primitive_element.lean)

Okay, I fixed it. It turned out that a few days ago, polynomial.roots was changed from a finset to a multiset

Thomas Browning (Sep 15 2020 at 00:16):

I'm surprised that didn't break more stuff

Kyle Miller (Sep 15 2020 at 01:39):

pushed some things https://github.com/leanprover-community/mathlib/pull/4153/commits/d07896f26bfeeabb6af5a836e46ed5d2c6281a19

Tried to keep lines from being too long, fixed some indentation, removed some (all?) non-terminal simps, removed field.infinite_of_infinite because you only used it once and this seems ok:

have Fα_inf : infinite Fα := infinite.of_injective _ (algebra_map F Fα).injective

It seems like primitive_element_two_inf_key could stand to be simplified. Are there any interesting sub-lemmas here?

Kyle Miller (Sep 15 2020 at 01:42):

Any reason you didn't use open_locale classical in primitive_element.lean? I switch it to that and it seems to work fine.

Thomas Browning (Sep 15 2020 at 01:51):

Kyle Miller said:

pushed some things https://github.com/leanprover-community/mathlib/pull/4153/commits/d07896f26bfeeabb6af5a836e46ed5d2c6281a19

Tried to keep lines from being too long, fixed some indentation, removed some (all?) non-terminal simps, removed field.infinite_of_infinite because you only used it once and this seems ok:

have Fα_inf : infinite Fα := infinite.of_injective _ (algebra_map F Fα).injective

It seems like primitive_element_two_inf_key could stand to be simplified. Are there any interesting sub-lemmas here?

Thanks Kyle! We've thought about trying to break off some sublemmas from primitive_element_two_inf_key, but I haven't had much success.

Patrick Lutz (Sep 15 2020 at 02:00):

Kyle Miller said:

Any reason you didn't use open_locale classical in primitive_element.lean? I switch it to that and it seems to work fine.

I don't recall, maybe @Thomas Browning did that? It could have been because it was faster at some point.

Kyle Miller (Sep 15 2020 at 02:20):

Just wanting to make sure I didn't break anything by changing it!

Patrick Lutz (Sep 15 2020 at 23:56):

Looks like bundled subfields and intermediate_field are coming soon: #4159

Thomas Browning (Sep 16 2020 at 00:36):

Looking forward to it. There was plenty of stuff that would be far less painful with the intermediate_field type.

Patrick Lutz (Sep 17 2020 at 06:52):

@Thomas Browning Is there anything I can do to help address the comments on the PR? I'm not sure what you've already done at this point.

Thomas Browning (Sep 17 2020 at 16:13):

I'm taking care of the splitting one now. Then there's just two left: the long lines one (which should be easy to finish off), and the eval one.

Thomas Browning (Sep 17 2020 at 16:21):

I'm not so sure that the eval one is a good idea. There are two places where there is an eval involving f, and in one it's a plain eval and in the other it's an eval2.

Thomas Browning (Sep 17 2020 at 16:21):

I'll give it a try though and see how it looks

Thomas Browning (Sep 17 2020 at 17:45):

There's also a new small merge conflict to sort out

Patrick Lutz (Sep 17 2020 at 17:47):

Yeah, it's because the bundled subfield got merged. I vote that for now we simply change import field_theory.subfield to import deprecated.subfield and deal with incorporating bundled subfields later (probably after intermediate_field has been merged)

Kevin Buzzard (Sep 17 2020 at 17:48):

That would be fine for now I think

Kevin Buzzard (Sep 17 2020 at 17:48):

You could promise the switch in a later PR maybe

Kevin Buzzard (Sep 17 2020 at 17:49):

I did one of these refactors and after a while you can just fix file after file because you know what's broken and how to fix it quite generally

Patrick Lutz (Sep 17 2020 at 23:55):

Okay, I've tried to merge with the master branch of mathlib. Fingers crossed that nothing else breaks

Thomas Browning (Sep 18 2020 at 01:05):

@Patrick Lutz It looks like your fingers weren't crossed enough

Patrick Lutz (Sep 18 2020 at 02:09):

Lol, I'm doing something else at the moment but I'll take a look to see what I messed up in a bit

Kyle Miller (Sep 18 2020 at 03:12):

It looks like you lost some functions from field_theory/subfield because the file moved due to the deprecation. It was surprisingly hard figuring that out from git...

Johan Commelin (Sep 18 2020 at 03:14):

Ooops... hopefully you can fix it by importing deprecated.is_subfield.

Patrick Lutz (Sep 18 2020 at 03:14):

Yeah, I just realized that too. Specifically is_subfield.pow_mem

Johan Commelin (Sep 18 2020 at 03:14):

(And don't worry about "deprecated". They will be "undeprecated" in a week or 2.)

Johan Commelin (Sep 18 2020 at 03:15):

Still, you might want to move some things over to bundled subfield if that is a more natural way of stating things.

Patrick Lutz (Sep 18 2020 at 03:15):

The problem is that is_subfield.pow_mem is not in deprecated/subfield because we added it in our PR but it wasn't there when Anne moved subfield.lean to deprecated/subfield.lean

Johan Commelin (Sep 18 2020 at 03:15):

Aha

Patrick Lutz (Sep 18 2020 at 03:15):

But it should be easy enough to fix

Patrick Lutz (Sep 18 2020 at 03:15):

The tricky part was when I merged with master VS Code wanted to compile everything and that basically always crashes my computer

Kyle Miller (Sep 18 2020 at 03:15):

I'm in the middle of fixing it

Patrick Lutz (Sep 18 2020 at 03:16):

so it was easier to just push to origin and wait for it to get compiled there and then run leanproject get-cache

Johan Commelin (Sep 18 2020 at 03:16):

Patrick Lutz said:

The tricky part was when I merged with master VS Code wanted to compile everything and that basically always crashes my computer

Yup, when the merge is ugly, I quit VS Code before it goes crazy, and I do the merge in another editor like Vim.

Patrick Lutz (Sep 18 2020 at 03:17):

Fixing the conflict itself was not so bad (though I missed that subtlety about is_subfield.pow_mem) but checking for errors is annoying

Patrick Lutz (Sep 18 2020 at 03:18):

Johan Commelin said:

Still, you might want to move some things over to bundled subfield if that is a more natural way of stating things.

Anne claimed that intermediate_field is coming soon so I think we'll wait for that before porting everything

Kyle Miller (Sep 18 2020 at 03:19):

Doing a merge when files are moved around is also tricky, so I'm not surprised you lost is_subfield.pow_mem!

Patrick Lutz (Sep 18 2020 at 03:20):

Honestly I just forgot that it was in one of the files that got changed

Patrick Lutz (Sep 18 2020 at 03:22):

I probably actually should have fixed the merge conflict in an editor besides VS Code. I was probably less careful than I should have been because I didn't want to keep VS Code open too long in case it ate up all my memory

Patrick Lutz (Sep 18 2020 at 03:23):

By the way, thanks for all the help Kyle!

Kyle Miller (Sep 18 2020 at 03:24):

Merging is usually better when files stay put because the diff will make sure you see the differences within a file. I've just found it relies on one's own memory a bit too much in cases like this.

Kyle Miller (Sep 18 2020 at 03:24):

Pushed the change

Kyle Miller (Sep 18 2020 at 03:25):

I think I last touched is_subfield.pow_mem to shorten the line lengths, and yet I forgot it was a thing. I was going through the last week of mathlib changes seeing when it was removed before I realized...

Patrick Lutz (Sep 18 2020 at 23:57):

@Thomas Browning https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/deprecated.20is_sub*

Thomas Browning (Sep 19 2020 at 00:06):

oh interesting

Patrick Lutz (Sep 19 2020 at 02:00):

@Thomas Browning I shortened the proof of primitive_element a bit. Along the way, I had to add a lemma saying that adjoin F S is equal to set.range (algebra_map (adjoin F S) E) as subsets of E, or in other words, that adjoin F S is equal to (\bot : subalgebra (adjoin F S) E) as subsets of E, which turned out to be not quite as trivial as I had imagined (perhaps due to my own ignorance)

Patrick Lutz (Sep 19 2020 at 02:02):

I'm going to take a look at primitive_element_inf next

Patrick Lutz (Sep 19 2020 at 06:48):

I just pushed some changes. Mainly I shortened the proof of primitive_element_inf. I also added two little lemmas to adjoin.lean saying that if F(x) has dimension 1 over F for every x : E then F = E. I also made the variable F implicit in some of the lemmas in adjoin.lean that deal with dimension.

Patrick Lutz (Sep 19 2020 at 07:03):

primitive_element.lean is now just about 260 lines btw

Patrick Lutz (Sep 19 2020 at 07:04):

Just pushed a little change adding names for the sections in adjoin.lean and primitive_element.lean

Patrick Lutz (Sep 19 2020 at 07:04):

@Thomas Browning Do you think we should change any of the lemmas in primitive_element.lean to private?

Thomas Browning (Sep 19 2020 at 17:23):

would it make sense to make anything private if it's a special case of the final theorem?

Johan Commelin (Sep 19 2020 at 17:24):

If it really is a special case, then yes.

Johan Commelin (Sep 19 2020 at 17:24):

But a lot of things that one thinks of as "auxilliary, implementation detail" turn out to be useful for others in a follow-up work.

Johan Commelin (Sep 19 2020 at 17:24):

And then they'll be happy if you didn't make it private

Kevin Buzzard (Sep 19 2020 at 18:43):

I'm not sure what we gain by making anything private. Why not just put a note in the docstring saying "don't use this, use this better theorem name_of_tbeorem because..."?

Johan Commelin (Sep 19 2020 at 18:46):

Making it private means it won't clutter your autocomplete

Kyle Miller (Sep 19 2020 at 18:56):

I wonder if most private things would be better as something in a sub-namespace called private. While it's not the paragon of PL design, that's the Mathematica way at least. All private does in Lean, if I remember correctly, is mangle names so you can't refer to them outside the namespace.

Patrick Lutz (Sep 20 2020 at 16:57):

@Thomas Browning #4180, #4181. It seems like intermediate_field is on its way to being merged

Patrick Lutz (Sep 21 2020 at 18:03):

@Thomas Browning I'll take care of the rest of the stuff about findim from the latest round of suggestions, but I might have to do it a little later in the day.

Thomas Browning (Sep 21 2020 at 18:18):

I'll try to finish-off the non-findim stuff

Patrick Lutz (Sep 22 2020 at 05:50):

@Thomas Browning I think I've finished refactoring the dimension lemmas. So that should be all the requested changes so far that I know about. I noticed there is also one other "unresolved" comment (namely this one). I think you already took care of it though. Is that correct?

Thomas Browning (Sep 22 2020 at 06:32):

I don't think that I've split that one off as a lemma yet.

Patrick Lutz (Sep 22 2020 at 17:22):

Thomas Browning said:

I don't think that I've split that one off as a lemma yet.

Have you done this yet? If not, I can try taking a stab at it.

Thomas Browning (Sep 22 2020 at 19:28):

Not yet. I'll have time this afternoon if you haven't done it by then.

Patrick Lutz (Sep 22 2020 at 21:43):

Okay, I've done it. But now I also want to make a couple other changes to the separability before pushing.

Patrick Lutz (Sep 22 2020 at 21:53):

Just realized there's an easier way to prove some of the dimension lemmas I added, except that it doesn't work in full generality because the lemmas proving that dimension of vector spaces is preserved by isomorphism are only for vector spaces in the same universe

Thomas Browning (Sep 22 2020 at 22:10):

Sounds good

Thomas Browning (Sep 23 2020 at 18:40):

I'm working on refactoring primitive_element_two_inf, so don't worry about those comments for now

Patrick Lutz (Sep 23 2020 at 18:47):

Oh, I recently pushed something removing all the polynomial._'s and I also just finished fixing the style issues (though I haven't pushed yet).

Patrick Lutz (Sep 23 2020 at 18:47):

should I push the style fixes anyway? They should be easy to merge later if need be

Thomas Browning (Sep 23 2020 at 18:48):

I might be doing some major rewriting, so hold off on those

Thomas Browning (Sep 23 2020 at 18:48):

actually, if you've already done them

Thomas Browning (Sep 23 2020 at 18:48):

then push them

Thomas Browning (Sep 23 2020 at 18:49):

and I'll work from there

Patrick Lutz (Sep 23 2020 at 18:50):

Okay, I just pushed them

Patrick Lutz (Sep 23 2020 at 18:50):

Let me know if you have any problems when you pull the changes

Patrick Lutz (Sep 23 2020 at 18:54):

Is it okay if I continue making some changes that don't affect primitive_element_two_inf?

Patrick Lutz (Sep 23 2020 at 18:54):

Also I can take care of the requested changes to the polynomial lemmas if that's okay with you

Thomas Browning (Sep 23 2020 at 19:05):

yeah, that's all fine

Patrick Lutz (Sep 23 2020 at 21:56):

@Thomas Browning I just pushed some changes that address some of the requested changes. I had to make a couple small changes to primitive_element_two_inf but they should be easy to deal with.

Thomas Browning (Sep 23 2020 at 23:06):

ok, I've pushed the big refactor.

Patrick Lutz (Sep 23 2020 at 23:25):

It's been kind of funny to watch the number of lines added move up and down over the course of the PR

Patrick Lutz (Sep 23 2020 at 23:26):

Hopefully we're close to merging now

Patrick Lutz (Sep 23 2020 at 23:27):

Btw, the version of the statement of the primitive element theorem that Anne mentioned needing is the same as the thing Jordan is working on right?

Thomas Browning (Sep 23 2020 at 23:32):

oh I guess so

Kevin Buzzard (Sep 24 2020 at 01:02):

Why do you need is_subfield.pow_mem in a deprecated file?

Kevin Buzzard (Sep 24 2020 at 01:03):

I did a "remove a deprecated import from a file and then fix the several hundred errors caused by this" PR once.

Patrick Lutz (Sep 24 2020 at 02:03):

Kevin Buzzard said:

Why do you need is_subfield.pow_mem in a deprecated file?

When I first wrote that lemma the file was not yet deprecated. In fact, it only became deprecated after we first made this PR.

Patrick Lutz (Sep 24 2020 at 02:04):

And right now I think it doesn't make sense to refactor everything to get rid of is_subfield until intermediate_field gets merged

Patrick Lutz (Sep 24 2020 at 02:04):

which should happen soon

Patrick Lutz (Sep 24 2020 at 18:17):

@Thomas Browning did you see Johan's comments on github? What do you think about changing the name of primitive_element to exists_adjoin_simple_eq_top?

Thomas Browning (Sep 24 2020 at 18:23):

I saw it. It is a bit of an abomination, but I would be fine with it.

Kevin Buzzard (Sep 26 2020 at 21:33):

Primitive element theorem merged! Well done to all who contributed!

Thomas Browning (Sep 26 2020 at 21:44):

@Patrick Lutz Should we make a branch for turning adjoin into intermediate field now?

Patrick Lutz (Sep 26 2020 at 21:48):

Thomas Browning said:

Patrick Lutz Should we make a branch for turning adjoin into intermediate field now?

Yeah

Thomas Browning (Sep 28 2020 at 16:58):

https://github.com/leanprover-community/mathlib/tree/adjoin_intermediate_field

Thomas Browning (Sep 28 2020 at 17:54):

at some point we should show bounded_lattice (intermediate_field K L), which might require establishing a "galois connection" (or something like that) between subsets of L containing K and intermediate fields

Thomas Browning (Sep 28 2020 at 17:58):

one issue(?) is that doing so would probably require the use of adjoin, so it would need to be done in adjoin.lean rather than intermediate_field.lean

Patrick Lutz (Sep 28 2020 at 18:02):

Thomas Browning said:

one issue(?) is that doing so would probably require the use of adjoin, so it would need to be done in adjoin.lean rather than intermediate_field.lean

That seems fine to me

Patrick Lutz (Sep 28 2020 at 18:05):

Thomas Browning said:

at some point we should show bounded_lattice (intermediate_field K L), which might require establishing a "galois connection" (or something like that) between subsets of L containing K and intermediate fields

By "galois connection" here do you just mean that if STS \subset T then L(S)L(T)L(S) \subset L(T)?

Thomas Browning (Sep 28 2020 at 18:07):

I'm not sure familiar with it, but I'm looking at ring_theory/algebra.lean, line 1100

Thomas Browning (Sep 28 2020 at 18:07):

where it does stuff with galois connections and galois insertions to quickly get bounded_lattice

Kevin Buzzard (Sep 28 2020 at 18:08):

There's a design decision to be made here

Kevin Buzzard (Sep 28 2020 at 18:08):

And I'm not sure what the right one is

Kevin Buzzard (Sep 28 2020 at 18:08):

because I'm unaware of the ramifications

Kevin Buzzard (Sep 28 2020 at 18:09):

Given a random subset of L. you want to generate a subfield of L containing K. There are two quite different ways to do this.

Kevin Buzzard (Sep 28 2020 at 18:10):

1) Prove that subfields of L containing K have an Inf (arbitrary intersections) and define the subfield corresponding to S to be the inf of the subfields of L containing K which also contain S

Kevin Buzzard (Sep 28 2020 at 18:11):

2) Define it the inductive way, so it's an inductively defined carrier (i.e. an inductive predicate) with constructors saying "k in K is in", "if a and b are in then their sum is in" etc

Kevin Buzzard (Sep 28 2020 at 18:11):

The advantage of (2) is that you get the recursor for free

Kevin Buzzard (Sep 28 2020 at 18:11):

But I don't know how important the recursor will be

Kevin Buzzard (Sep 28 2020 at 18:12):

The advantage of (1) is that it's cheap and it works. I've used it to get to very quick Galois insertion proofs when doing subrings etc

Thomas Browning (Sep 28 2020 at 18:12):

Currently we have adjoin F S which uses ring.closure (I'm not sure which of the two approaches ring.closure uses)

Thomas Browning (Sep 28 2020 at 18:12):

ah, it looks like it uses the 2nd way

Kevin Buzzard (Sep 28 2020 at 18:12):

Oh you already have this direction!

Thomas Browning (Sep 28 2020 at 18:13):

yeah

Kevin Buzzard (Sep 28 2020 at 18:13):

Are you doing subrings or subfields?

Thomas Browning (Sep 28 2020 at 18:13):

subfields

Kevin Buzzard (Sep 28 2020 at 18:13):

And adjoin produces a subfield?

Thomas Browning (Sep 28 2020 at 18:13):

yes, but now an intermediate field

Kevin Buzzard (Sep 28 2020 at 18:14):

So this is a different function to the subring adjoin?

Thomas Browning (Sep 28 2020 at 18:14):

yeah, I just said subring closure because I hadn't gone far enough down the rabbit hole

Thomas Browning (Sep 28 2020 at 18:14):

it's defined in terms of field.closure

Kevin Buzzard (Sep 28 2020 at 18:15):

gotcha

Patrick Lutz (Sep 28 2020 at 18:22):

I think following the strategy from ring_theory.algebra and proving that there is a galois connection between field.adjoin and coe seems reasonable

Patrick Lutz (Sep 28 2020 at 18:26):

Btw, @Thomas Browning, I just sent Anne a message asking if they have already done any work on refactoring field_theory/adjoin

Patrick Lutz (Sep 28 2020 at 18:32):

I also just asked in the is there code for X? stream about whether mathlib already proves anything like what Jordan is working on (the dimension and basis of F[x]/pF[x]/p)

Thomas Browning (Sep 28 2020 at 18:32):

Just proved the complete_lattice

Thomas Browning (Sep 28 2020 at 18:32):

It wasn't too bad

Thomas Browning (Sep 28 2020 at 18:33):

It will probably speed-up/obsolete some other lemmas we have in adjoin.lean

Patrick Lutz (Sep 28 2020 at 18:40):

@Thomas Browning presumably we should no longer import deprecated/subfield in field_theory/adjoin?

Thomas Browning (Sep 28 2020 at 18:40):

yeah, we need to get rid of that import

Thomas Browning (Sep 28 2020 at 18:41):

the problem is that closure is defined in that file

Patrick Lutz (Sep 28 2020 at 18:41):

oh, then I guess we need to port closure over to the new subfield file?

Patrick Lutz (Sep 28 2020 at 18:42):

No, wait, the new subfield also has some version of closure

Patrick Lutz (Sep 28 2020 at 18:44):

To me it looks like it should be fine to use the new version of subfield closure

Patrick Lutz (Sep 28 2020 at 18:48):

Since intermediate_field inherits from both subalgebra and subfield and subfield.closure is already a subfield, I feel like it should be very easy to define field.adjoin. Unfortunately I don't really know how currently

Thomas Browning (Sep 28 2020 at 18:53):

I'll take a look

Patrick Lutz (Sep 28 2020 at 18:54):

Okay, I think I found the relevant part of "Theorem Proving in Lean" (on inheritance)

Patrick Lutz (Sep 28 2020 at 18:57):

Hmm, actually that section of "Theorem Proving in Lean" is really short

Thomas Browning (Sep 28 2020 at 18:58):

I've figured out how to rewrite adjoin in terms of the bundled subfield

Thomas Browning (Sep 28 2020 at 19:32):

Ok, it's pushed but there are a bunch of errors

Patrick Lutz (Sep 28 2020 at 19:41):

I fixed a couple errors. I'll take a more serious look this evening

Patrick Lutz (Sep 28 2020 at 19:41):

A couple comments

Patrick Lutz (Sep 28 2020 at 19:41):

a lot of things need to change from field.foo to subfield.foo

Patrick Lutz (Sep 28 2020 at 19:42):

some instances are no longer necessary. Like now adjoin F S is automatically a subfield of E and also a field

Patrick Lutz (Sep 28 2020 at 19:42):

also, obviously, lots of hypotheses have to change from is_subfield to something else

Patrick Lutz (Sep 28 2020 at 20:45):

@Thomas Browning Have you seen ring_hom.field_range? Also, Anne said they were working on refactoring field.adjoin to use intermediate_field here: https://github.com/leanprover-community/mathlib/blob/Vierkantor-dedekind-domain/src/field_theory/adjoin.lean

Thomas Browning (Sep 28 2020 at 20:53):

I haven't seen ring_hom.field_range, but it looks useful. I presume that we'll merge our refactoring before "Vierkantor-dedekind-domain" gets merged, so I guess we should go ahead but try to make our version compatible with theirs?

Patrick Lutz (Sep 28 2020 at 20:56):

Thomas Browning said:

I haven't seen ring_hom.field_range, but it looks useful. I presume that we'll merge our refactoring before "Vierkantor-dedekind-domain" gets merged, so I guess we should go ahead but try to make our version compatible with theirs?

I think we should do whatever seems best, reusing any stuff they already did that seems helpful.

Patrick Lutz (Sep 28 2020 at 20:59):

But it looks like we can reuse that stuff to immediately fix a number of proofs that got messed up when we stopped importing deprecated/subfield

Patrick Lutz (Sep 28 2020 at 21:02):

Oh, it also looks like we now have a number of problems introduced by trying to use lemmas about the bottom subalgebra in places where we are now really talking about the bottom intermediate field. Should be easy to fix by proving that those two things are equal though, I think. (Or maybe by proving a bunch of lemmas like eq_bot_iff for intermediate_field)

Thomas Browning (Sep 28 2020 at 21:26):

shouldn't we just change all bottom subalgebras to bottom intermediate fields?

Thomas Browning (Sep 28 2020 at 21:27):

or are there some lemmas that should be stated in terms of the bottom subalgebra?

Patrick Lutz (Sep 28 2020 at 21:49):

Thomas Browning said:

or are there some lemmas that should be stated in terms of the bottom subalgebra?

No, the lemmas should be stated in terms of the bottom intermediate_field I guess. But the proofs are relying on lemmas about the bottom subalgebra so we need some extra lemmas to connect them

Patrick Lutz (Sep 29 2020 at 19:21):

@Thomas Browning I did a little bit more work on refactoring field.adjoin and primitive_element. Here's a couple of comments:

Patrick Lutz (Sep 29 2020 at 19:22):

1) Something weird is going on in the proof of mem_bot_of_adjoin_simple_sub_bot. I left a comment about it in the file

Patrick Lutz (Sep 29 2020 at 19:23):

2) We're missing a bunch of useful little lemmas like ext_iff and eq_top_iff etc for intermediate_field that we had for subalgebra. I think we should consider proving some of them.

Patrick Lutz (Sep 29 2020 at 19:24):

3) For some reason, previously Lean was able to figure out on its own that if E is finite dimensional over F then so is F(x) but now that F(x) is an intermediate_field it can't. I think this has something to do with the coercion from subalgebra to intermediate_field

Patrick Lutz (Sep 29 2020 at 19:25):

4) I started to fix the problems in primitive_element. It doesn't look too bad but the proof of primitive_element_two_inf might require some work

Patrick Lutz (Sep 29 2020 at 19:27):

@Thomas Browning @Jordan Brown I just pushed a change to the old galois theory repo to contribute a little bit to degree_of_simple_extension.lean. I left a long-ish comment in the source code, but let me say a little bit here too:

Patrick Lutz (Sep 29 2020 at 19:28):

1) I think the theorem that the dimension of F[x]/p is equal to the degree of p can be proved for all nonzero p (not just ones which are the minimal polynomial of something) so we should probably do that

Patrick Lutz (Sep 29 2020 at 19:29):

2) I left a comment in the source code about one strategy to do this that doesn't use bases (although it's not really fundamentally any different). Basically, I think it might be best to construct a map from Fdeg pF^{\text{deg } p} to F[x]/pF[x]/p and then show it's an isomorphism

Patrick Lutz (Sep 29 2020 at 19:30):

3) I tried asking in the Is_there_code_for_X stream about whether stuff like this is already in mathlib and nobody answered :sad: . But as Jordan said last week, I don't think it is

Patrick Lutz (Sep 29 2020 at 19:32):

Also, as long as the theorem that the dimension of F[x]/p is equal to the degree of p is really not in mathlib, I think it would make a nice self-contained PR to mathlib

Kevin Buzzard (Sep 29 2020 at 19:37):

Patrick Lutz said:

2) I left a comment in the source code about one strategy to do this that doesn't use bases (although it's not really fundamentally any different). Basically, I think it might be best to construct a map from Fdeg pF^{\text{deg } p} to F[x]/pF[x]/p and then show it's an isomorphism

Surely monic polynomials have a division / remainder algorithm? This is what you need I guess.

Patrick Lutz (Sep 29 2020 at 19:48):

Kevin Buzzard said:

Patrick Lutz said:

2) I left a comment in the source code about one strategy to do this that doesn't use bases (although it's not really fundamentally any different). Basically, I think it might be best to construct a map from Fdeg pF^{\text{deg } p} to F[x]/pF[x]/p and then show it's an isomorphism

Surely monic polynomials have a division / remainder algorithm? This is what you need I guess.

Yeah, that should go into the proof that the map is surjective.

Kevin Buzzard (Sep 29 2020 at 19:49):

There's div and mod in data.polynomial.field_division

Patrick Lutz (Sep 29 2020 at 19:49):

But first I need to actually learn how quotients work in Lean/mathlib to even know the best way to construct the map

Patrick Lutz (Sep 29 2020 at 19:50):

Kevin Buzzard said:

There's div and mod in data.polynomial.field_division

Yeah, that stuff got used in the proof of the primitive element theorem

Kevin Buzzard (Sep 29 2020 at 19:52):

This is the theory for all polys over fields; what you really want is something for monic polys over any comm ring; the quotient R[x]/(p) is free rank deg(p).

Kevin Buzzard (Sep 29 2020 at 19:54):

aah there's mod_by_monic in data.polynomial.div

Kevin Buzzard (Sep 29 2020 at 19:56):

div_mod_by_monic_unique is injectivity of the map from (deg < deg(p)) and surjectivity comes from mod_by_monic_add_div

Kevin Buzzard (Sep 29 2020 at 19:56):

linearity should be easy and now hopefully the library can take it from there

Thomas Browning (Sep 29 2020 at 21:59):

one thing that's causing some headaches is that there is a partial order defined in intermediate_field.lean, but there is also a partial order coming from the lattice stuff in adjoin.lean

Thomas Browning (Sep 29 2020 at 22:00):

(deleted)

Thomas Browning (Sep 29 2020 at 22:01):

(deleted)

Thomas Browning (Sep 29 2020 at 22:04):

the issue is that when I try to apply a result like eq_bot_iff, lean seems to have trouble reconciling the partial order defined in intermediate_field.lean with the partial order from the lattice

Thomas Browning (Sep 29 2020 at 22:06):

Here's a fun error message

Thomas Browning (Sep 29 2020 at 22:06):

type mismatch at application
  eq_bot_iff.mpr adjoin_le_bot
term
  adjoin_le_bot
has type
  @has_le.le (@intermediate_field F E _inst_1 _inst_2 _inst_3)
    (@preorder.to_has_le (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@partial_order.to_preorder (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@intermediate_field.partial_order F E _inst_1 _inst_2 _inst_3)))
    (@intermediate_field.adjoin F _inst_1 E _inst_2 _inst_3 S)
    (@has_bot.bot (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@intermediate_field.has_bot F E _inst_1 _inst_2 _inst_3))
but is expected to have type
  @has_le.le (@intermediate_field F E _inst_1 _inst_2 _inst_3)
    (@preorder.to_has_le (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@partial_order.to_preorder (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@order_bot.to_partial_order (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@bounded_lattice.to_order_bot (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@intermediate_field.bounded_lattice F E _inst_1 _inst_2 _inst_3)))))
    (@intermediate_field.adjoin F _inst_1 E _inst_2 _inst_3 S)
    (@has_bot.bot (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@order_bot.to_has_bot (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@bounded_lattice.to_order_bot (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.bounded_lattice F E _inst_1 _inst_2 _inst_3))))

Thomas Browning (Sep 29 2020 at 22:07):

produced by the code

have adjoin_le_bot : adjoin F S   := sorry,
have hh := (@eq_bot_iff (intermediate_field F E) _ (adjoin F S)).mpr adjoin_le_bot,

Patrick Lutz (Sep 29 2020 at 22:28):

Thomas Browning said:

the issue is that when I try to apply a result like eq_bot_iff, lean seems to have trouble reconciling the partial order defined in intermediate_field.lean with the partial order from the lattice

Maybe we need to prove they're equal?

Thomas Browning (Sep 29 2020 at 23:02):

The weird thing is that the lattice is defined from the partial order defined in intermediate_field.lean

Thomas Browning (Sep 30 2020 at 00:05):

ok, I found the issue. There was another bot instance, another top instance, and another bounded_lattice instance that were conflicting with the main complete_lattice instance.

Thomas Browning (Sep 30 2020 at 00:09):

(deleted)

Kevin Buzzard (Sep 30 2020 at 09:36):

There shouldn't be any diamonds in mathlib and this sounds like a diamond

Patrick Lutz (Sep 30 2020 at 16:54):

Kevin Buzzard said:

There shouldn't be any diamonds in mathlib and this sounds like a diamond

Which part sounds like a diamond?

Patrick Lutz (Sep 30 2020 at 16:55):

Also is the ban on diamonds by convention or by law (i.e. part of the rules of Lean)?

Patrick Lutz (Sep 30 2020 at 16:55):

The only time I've seen it mentioned before was in Thomas Hales' blog post on Lean

Johan Commelin (Sep 30 2020 at 17:05):

It's a convention. But without it you land in a swamp that you really don't want to get into

Kevin Buzzard (Sep 30 2020 at 18:25):

If you have two non defeq partial orders then that's a great example of a diamond

Kevin Buzzard (Sep 30 2020 at 18:25):

If mathlib made both of those partial orders then people will want to know about it

Patrick Lutz (Sep 30 2020 at 18:55):

Oh wait, I think I understand what's happening. Anne pointed us to some work they had already done refactoring adjoin.lean which included proving that field.adjoin gives an adjunction. I included this in our version of field_theory/adjoin but Thomas had also already added a proof that field.adjoin forms a galois connection. Both of those things give instances of bounded_lattice I guess.

Patrick Lutz (Sep 30 2020 at 18:55):

Not sure what the right solution is though

Kyle Miller (Sep 30 2020 at 19:18):

If both bounded_lattice instances are equal, can you delete a less-general one?

Patrick Lutz (Sep 30 2020 at 20:03):

Wait, actually I might be wrong. There seems to be a bounded_lattice instance hanging around in intermediate_field.lean for some reason with no proof (only a sorry). So maybe this was a simple oversight.

Patrick Lutz (Sep 30 2020 at 20:03):

The adjunction is probably fine.

Patrick Lutz (Sep 30 2020 at 20:05):

@Thomas Browning actually the proof of primitive_element_inf_aux turned out to be really easy to fix. I just had to add .to_subalgebra in one place

Patrick Lutz (Sep 30 2020 at 20:12):

(deleted)

Patrick Lutz (Sep 30 2020 at 20:13):

Patrick Lutz said:

Wait, actually I might be wrong. There seems to be a bounded_lattice instance hanging around in intermediate_field.lean for some reason with no proof (only a sorry). So maybe this was a simple oversight.

Oh, it looks like Thomas already took care of this yesterday

Patrick Lutz (Sep 30 2020 at 20:14):

@Thomas Browning I think the main thing to do now to get everything to compile is to prove that the bottom and top intermediate_fields are equal to the bottom and top subalgebras

Patrick Lutz (Sep 30 2020 at 20:14):

and then figure out how to get Lean to infer that an intermediate field is finite dimensional if the entire field extension is

Kevin Buzzard (Sep 30 2020 at 20:14):

If one of your definitions of <= was "sorry" then no wonder Lean was finding it hard to work with :-)

Patrick Lutz (Sep 30 2020 at 20:15):

Yeah, I just didn't even realize that line was there. And it looks like Thomas actually removed it yesterday

Patrick Lutz (Sep 30 2020 at 20:15):

I just hadn't pulled any changes since then

Thomas Browning (Sep 30 2020 at 20:19):

yeah, I think that the issue is resolved now

Thomas Browning (Sep 30 2020 at 20:19):

and there was a sorried lattice instance (which I might have been responsible for... oops)

Thomas Browning (Sep 30 2020 at 23:14):

Patrick Lutz said:

Thomas Browning I think the main thing to do now to get everything to compile is to prove that the bottom and top intermediate_fields are equal to the bottom and top subalgebras

I proved a few lemmas along these lines.

Thomas Browning (Oct 03 2020 at 02:35):

@Patrick Lutz I've fixed the remaining issues, so the branch is ready to pull. Is there anything else that you or I should take a look at before making the PR?

Thomas Browning (Oct 03 2020 at 18:39):

Here's one thing: If (K : intermediate_field F E) then should we add coersions (or lift?) from intermediate_field F K and intermediate_field K E to intermediate_field F E?

Kevin Buzzard (Oct 03 2020 at 20:23):

Are the corresponding coercions there for eg submonoid?

Kevin Buzzard (Oct 03 2020 at 20:24):

Maybe subalgebra is a better question

Thomas Browning (Oct 04 2020 at 23:39):

I'm not sure whether or not they are there, but I added them for intermediate_field and it seemed to clean up some stuff.

Thomas Browning (Oct 04 2020 at 23:40):

In particular, the end of the proof of the primitive element theorem got a little easier (now working directly with intermediate_fields rather than their carriers)

Thomas Browning (Oct 04 2020 at 23:45):

@Patrick Lutz Is there anything else you want done before the PR?

Thomas Browning (Oct 05 2020 at 08:09):

I proved the general induction result, although the proof turned out to be longer than I expected.

Patrick Lutz (Oct 05 2020 at 08:24):

@Thomas Browning Sorry I've been incommunicado the past couple days. I'll take a look at it on Monday and make any changes I think should be made. If for some reason I still haven't responded by the end of the day on Monday, feel free to just go ahead and make the PR

Thomas Browning (Oct 06 2020 at 16:29):

#4468

Thomas Browning (Oct 06 2020 at 16:29):

Unfortunately there's a merge conflict in algebra.lean

Thomas Browning (Oct 09 2020 at 22:58):

@Jordan Brown I just pushed some changes. Defining an explicit inverse seems a little tricky, but we can just do injectivity and surjectivity manually. Surjectivity will require doing stuff with mods.

Jordan Brown (Oct 10 2020 at 01:28):

What was the problem with defining an inverse?

Thomas Browning (Oct 10 2020 at 02:54):

it just seems a little tricky to write down a function that takes a lift and takes it mod p

Jordan Brown (Oct 14 2020 at 21:03):

Is there an easy way to get Lean to see that adjoin_root.mk is surjective? It's an ideal quotients, and mathlib has that ideal quotients are surjective, but for some reason I can't get Lean to realize that that applies to adjoin_root.mk

Thomas Browning (Oct 14 2020 at 21:52):

lemma surjective : function.surjective (adjoin_root.mk p) :=
begin
  exact ideal.quotient.mk_surjective,
end

Thomas Browning (Oct 14 2020 at 21:53):

@Jordan Brown so you should be able to just use ideal.quotient.mk_surjective as is

Thomas Browning (Oct 21 2020 at 20:09):

@Patrick Lutz @Jordan Brown We are actually very close to the Galois correspondence. I think that the last big ingredient that we need is this:
If E/K is finite Galois (i.e., finite, normal, and separable) then [E:K] = |Aut(E/K)|. This should follow from the primitive element theorem + Jordan's isomorphism (both sides are equal to the degree of the minimal polynomial of the primitive element).

Kevin Buzzard (Oct 21 2020 at 20:18):

oh wow, I always prove this in lectures by counting, and then deduce the primitive element theorem from it.

Kevin Buzzard (Oct 21 2020 at 20:19):

This would be a very cool milestone

Patrick Lutz (Oct 21 2020 at 21:05):

Thomas Browning said:

Patrick Lutz Jordan Brown We are actually very close to the Galois correspondence. I think that the last big ingredient that we need is this:
If E/K is finite Galois (i.e., finite, normal, and separable) then [E:K] = |Aut(E/K)|. This should follow from the primitive element theorem + Jordan's isomorphism (both sides are equal to the degree of the minimal polynomial of the primitive element).

Oh, wow, nice. I just submitted my nsf application, so I should actually have some time to work on this again

Patrick Lutz (Oct 25 2020 at 03:37):

@Thomas Browning @Jordan Brown I just pushed a change to the galois theory repo which finishes the surjectivity proof and cleans it up a little bit (see module_map_sujective'). It turns out that mathlib does already contain a lemma saying that if p is nonzero then q % p has lower degree than p (it's called euclidean_domain.mod_lt, as I learned from Heather Macbeth in the Is there code for X stream). Also the lemma only needs the assumption that p is nonzero, not that it is non-constant.

Patrick Lutz (Oct 25 2020 at 03:53):

@Thomas Browning adjoin_root_equiv_adjoin_simple looks kind of scary somehow

Patrick Lutz (Oct 25 2020 at 03:53):

So many @s

Patrick Lutz (Oct 25 2020 at 03:54):

I'm going to work on findim_adjoin_integral either tonight or tomorrow morning

Thomas Browning (Oct 25 2020 at 09:52):

Patrick Lutz said:

Thomas Browning adjoin_root_equiv_adjoin_simple looks kind of scary somehow

You don't say...
Actually, it's not that bad.
Those @'s are just because I wasn't able to get Lean to automatically use the assumption h : is_integral F α.
If you can figure out how to get Lean to do this automatically, let me know.

Thomas Browning (Oct 25 2020 at 13:53):

They're gone: https://github.com/leanprover-community/mathlib/commit/f3bce8782b23c50d553bed41819ac8df1f336a40

Thomas Browning (Oct 25 2020 at 17:06):

Minor bad news: We can't use lagrange.fun_equiv_degree_lt because it requires the finset to be of elements of the field, so we'll run into trouble if the field is finite.

Thomas Browning (Oct 25 2020 at 17:08):

so we need another way of showing that polynomial.degree_lt K n has findim equal to n

Thomas Browning (Oct 25 2020 at 17:51):

Patrick Lutz said:

I'm going to work on findim_adjoin_integral either tonight or tomorrow morning

It's all finished except for the annoying findim of degree_lt.

Kevin Buzzard (Oct 25 2020 at 17:56):

Thomas Browning said:

Minor bad news: We can't use lagrange.fun_equiv_degree_lt because it requires the finset to be of elements of the field, so we'll run into trouble if the field is finite.

What's the problem here?

Thomas Browning (Oct 25 2020 at 18:00):

Well, lagrange.fun_equiv_degree_lt states that for any finset s : finset F, there is an isomorphism degree_lt F s.card ≃ₗ[F] ((↑s : set F) → F)

Thomas Browning (Oct 25 2020 at 18:01):

this is great, except that if F is finite then we can't necessarily choose an s : finset F of cardinality n

Thomas Browning (Oct 25 2020 at 18:09):

We're trying to show this:

instance temp_inst (F : Type*) [field F] (n : ) :
  finite_dimensional F (polynomial.degree_lt F n) := sorry

lemma temp_lem (F : Type*) [field F] (n : ) :
  finite_dimensional.findim F (polynomial.degree_lt F n) = n := sorry

Kevin Buzzard (Oct 25 2020 at 18:15):

fun_equiv_degree_lt is somehow not the correct theorem, is it! s could be any finite subset of anything.

Kevin Buzzard (Oct 25 2020 at 18:17):

I see -- this is a very explicit map coming from evaluation and using the fact that F is a field.

Thomas Browning (Oct 25 2020 at 18:18):

Yeah, but you're right that it should be true for any finset s (of any Type)

Kevin Buzzard (Oct 25 2020 at 18:18):

degree_lt_eq_span_X_pow is what you want

Kevin Buzzard (Oct 25 2020 at 18:19):

in ring_theory.polynomial.basic

Thomas Browning (Oct 25 2020 at 18:19):

I saw that, but do we know that they are linearly independent?

Kevin Buzzard (Oct 25 2020 at 18:19):

that'll be another lemma

Kevin Buzzard (Oct 25 2020 at 18:19):

"a polynomial is zero iff all its coefficients are zero"

Kevin Buzzard (Oct 25 2020 at 18:20):

but I agree that there's work to do here

Patrick Lutz (Oct 25 2020 at 21:38):

@Thomas Browning You haven't added module_map from the galois_theory repo anywhere right?

Patrick Lutz (Oct 25 2020 at 21:38):

At least I don't see it in any of the changes you've pushed

Thomas Browning (Oct 25 2020 at 21:58):

it should be in adjoin_root.lean

Thomas Browning (Oct 25 2020 at 21:59):

https://github.com/leanprover-community/mathlib/blob/galois_definition/src/ring_theory/adjoin_root.lean

Patrick Lutz (Oct 25 2020 at 22:10):

oh, I see it

Patrick Lutz (Oct 25 2020 at 22:11):

I've been refactoring that a little bit so I'm going to change it soon

Thomas Browning (Oct 25 2020 at 22:14):

cool

Thomas Browning (Oct 25 2020 at 22:15):

I've almost proved the two sorries, so don't mess with those just yet

Thomas Browning (Oct 25 2020 at 22:15):

actually, let me just push what I have now

Thomas Browning (Oct 25 2020 at 22:15):

pushed

Patrick Lutz (Oct 25 2020 at 22:31):

Okay, now I pushed

Patrick Lutz (Oct 25 2020 at 22:31):

I'll look at what you did in a sec

Patrick Lutz (Oct 25 2020 at 22:31):

do you think we should give degree_lt_linear_map a different name?

Patrick Lutz (Oct 25 2020 at 22:32):

also I think it might make sense to combine the injectivity and surjectivity proofs into one big proof

Thomas Browning (Oct 25 2020 at 22:58):

that seems reasonable

Patrick Lutz (Oct 25 2020 at 23:12):

the linter is not very happy btw

Thomas Browning (Oct 25 2020 at 23:12):

where should all the temp stuff go?

Patrick Lutz (Oct 25 2020 at 23:13):

why did you decide to define a new map? Why not just prove that the obvious basis for degree_lt is really a basis since half of it has already been done?

Patrick Lutz (Oct 25 2020 at 23:13):

and it looks like injectivity was the easier part anyway and that corresponds the proving linear independence, which is the part that hasn't been done yet

Thomas Browning (Oct 25 2020 at 23:14):

well, proving the basis seemed rather hard

Patrick Lutz (Oct 25 2020 at 23:14):

Thomas Browning said:

where should all the temp stuff go?

hmm, not sure. Most stuff about degree_lt seems to be in ring_theory.polynomial.basic so maybe there

Patrick Lutz (Oct 25 2020 at 23:15):

the linter is mostly unhappy that documentation is missing but it also doesn't like f \ne 0 as a hypothesis of an instance

Patrick Lutz (Oct 25 2020 at 23:16):

maybe the finite_dimensional instance should just be a lemma?

Thomas Browning (Oct 25 2020 at 23:16):

where is the f \ne 0 hypothesis?

Thomas Browning (Oct 25 2020 at 23:16):

oh I see

Patrick Lutz (Oct 25 2020 at 23:16):

instance finite_dimensional (hf : f  0) : finite_dimensional K (adjoin_root f) :=
linear_equiv.finite_dimensional (degree_lt_linear_equiv f hf)

Thomas Browning (Oct 25 2020 at 23:16):

yeah, that could be lemma

Patrick Lutz (Oct 25 2020 at 23:16):

it's actually probably possible to remove the hypothesis too

Thomas Browning (Oct 25 2020 at 23:17):

it's not true for f=0 is it?

Patrick Lutz (Oct 25 2020 at 23:17):

I don't know what adjoin_root 0 does but it probably is finite dimensional

Kevin Buzzard (Oct 25 2020 at 23:17):

Depends on how lean defined things!

Kevin Buzzard (Oct 25 2020 at 23:17):

But I bet it just adds 37

Thomas Browning (Oct 25 2020 at 23:17):

wouldn't it be the quotient by the zero ideal?

Patrick Lutz (Oct 25 2020 at 23:17):

oh maybe

Patrick Lutz (Oct 25 2020 at 23:18):

you're probably right

Patrick Lutz (Oct 25 2020 at 23:18):

oh well

Kevin Buzzard (Oct 25 2020 at 23:18):

I'm on mobile but am now very interested :-)

Kevin Buzzard (Oct 25 2020 at 23:18):

If f is reducible what does it add?

Patrick Lutz (Oct 25 2020 at 23:18):

?

Patrick Lutz (Oct 25 2020 at 23:19):

Kevin Buzzard said:

If f is reducible what does it add?

what do you mean by add?

Kevin Buzzard (Oct 25 2020 at 23:20):

I just didn't know the definition. I've looked now and disappointingly it does just quotient out by (f)

Kevin Buzzard (Oct 25 2020 at 23:21):

So yes it looks like it's not true when f=0.

Kevin Buzzard (Oct 25 2020 at 23:21):

If you're in a relative situation then I envisaged throwing in a random root of the big field into the small field and then you might have got away with it because 37 is a root of the zero polynomial

Patrick Lutz (Oct 25 2020 at 23:24):

yeah, in a sense I think the quotient by (0) is not the same as adjoining a root of 0

Patrick Lutz (Oct 25 2020 at 23:24):

but it makes sense that it's defined this way

Patrick Lutz (Oct 25 2020 at 23:27):

hmm, why is it so hard to work with bases in mathlib?

Thomas Browning (Oct 25 2020 at 23:29):

It's possible that if you know how to use them then it's fine, but I find them very hard to work with

Patrick Lutz (Oct 25 2020 at 23:31):

yeah, somehow even defining the basis is getting annoying

Patrick Lutz (Oct 25 2020 at 23:33):

because to know something is a member of degree_lt K n you need to know its degree is less than n. But if you just want to take the image of {0,1,,n1}\{0,1, \ldots, n-1\} under ixii \mapsto x^i then you need to somehow know in the definition of ixii \mapsto x^i that i<ni < n

Patrick Lutz (Oct 25 2020 at 23:36):

actually, it would be nice to have the following lemma (maybe it's already in mathlib?): if SS is a subset of a vector space VV which happens to be linearly independent, contained in a subspace WW and span WW then it's a basis for WW (after some appropriate coercion)

Patrick Lutz (Oct 25 2020 at 23:36):

but I can't immediately find anything like that

Thomas Browning (Oct 25 2020 at 23:45):

Do you know how to finish off the last sorry?

Thomas Browning (Oct 25 2020 at 23:45):

lean knows that functions from a finset are finite_dimensional, so I assume that it also knows what the dimension is

Patrick Lutz (Oct 25 2020 at 23:52):

yeah, I think it's dim_fun

Patrick Lutz (Oct 25 2020 at 23:52):

I can try finishing it off

Thomas Browning (Oct 25 2020 at 23:56):

lemma findim (hf : f  0) : finite_dimensional.findim K (adjoin_root f) = f.nat_degree :=
by rw [linear_equiv.findim_eq (((polynomial.degree_lt_linear_equiv K (f.nat_degree)).symm).trans
      (degree_lt_linear_equiv f hf)), finite_dimensional.findim_fintype_fun_eq_card K,
      fintype.card_coe, finset.card_range]

Thomas Browning (Oct 25 2020 at 23:57):

findim_fintype_fun_eq_card did the trick (thanks for telling me about dim_fun)

Patrick Lutz (Oct 26 2020 at 00:06):

nice

Patrick Lutz (Oct 26 2020 at 00:08):

is linear_algebra.lagrange still needed at the top of the file?

Patrick Lutz (Oct 26 2020 at 00:08):

looks like it's not

Thomas Browning (Oct 26 2020 at 00:08):

oh, I guess not

Thomas Browning (Oct 26 2020 at 00:09):

should we include a bijection(either just an equiv or something more fancy) between subgroup and intermediate_field ?

Patrick Lutz (Oct 26 2020 at 00:17):

I just pushed some changes adding documentation to make the linter happy

Patrick Lutz (Oct 26 2020 at 00:18):

Thomas Browning said:

should we include a bijection(either just an equiv or something more fancy) between subgroup and intermediate_field ?

You mean as part of the galois correspondence? Probably

Thomas Browning (Oct 26 2020 at 00:52):

@Patrick Lutz Anything else you want to do before the PR?

Thomas Browning (Oct 26 2020 at 00:52):

do we need any namespaces?

Patrick Lutz (Oct 26 2020 at 00:53):

for field_theory/galois? Probably should put it in some namespace.

Patrick Lutz (Oct 26 2020 at 00:54):

Thomas Browning said:

Patrick Lutz Anything else you want to do before the PR?

I think the linter is not happy with galois.lean

Thomas Browning (Oct 26 2020 at 00:54):

even on the most recent push?

Patrick Lutz (Oct 26 2020 at 00:54):

Three defs are missing documentation

Patrick Lutz (Oct 26 2020 at 00:54):

yeah I think so

Patrick Lutz (Oct 26 2020 at 00:55):

Try writing #lint at the bottom of the file

Thomas Browning (Oct 26 2020 at 00:55):

Ah

Thomas Browning (Oct 26 2020 at 00:55):

I'll take care of that

Patrick Lutz (Oct 26 2020 at 00:57):

okay, cool. I also made a couple tiny changes to the documentation

Patrick Lutz (Oct 26 2020 at 00:58):

so what does this PR add? Everything in galois.lean plus the changes to adjoin_root, ring_theory.polynomial.basic and field_theory.adjoin. Anything else?

Thomas Browning (Oct 26 2020 at 01:02):

there are some small changes to other files, but not much else

Thomas Browning (Oct 26 2020 at 01:03):

I guess one major thing is that field adjoin is isomorphic to adjoin_root

Patrick Lutz (Oct 26 2020 at 01:03):

where was that? In field_theory/adjoin.lean?

Thomas Browning (Oct 26 2020 at 01:03):

yeah

Thomas Browning (Oct 26 2020 at 01:03):

are you drafting the PR?

Patrick Lutz (Oct 26 2020 at 01:03):

no

Patrick Lutz (Oct 26 2020 at 01:03):

should I?

Patrick Lutz (Oct 26 2020 at 01:04):

Thomas Browning said:

are you drafting the PR?

I was just trying to look over everything to see if there's anything that should obviously be changed before a PR

Thomas Browning (Oct 26 2020 at 01:04):

should we make some namespaces first?

Patrick Lutz (Oct 26 2020 at 01:04):

yeah

Patrick Lutz (Oct 26 2020 at 01:05):

--TODO: Maybe upgrade this to some sort of lattice anti-isomorphism?

Do you want to leave this in?

Thomas Browning (Oct 26 2020 at 01:05):

might as well, I don't know if mathlib has anti-isomorphisms yet?

Patrick Lutz (Oct 26 2020 at 01:06):

sure

Patrick Lutz (Oct 26 2020 at 01:07):

it does have antitone galois connections I think?

Patrick Lutz (Oct 26 2020 at 01:07):

is galois a reasonable namespace?

Thomas Browning (Oct 26 2020 at 01:07):

sure

Thomas Browning (Oct 26 2020 at 01:07):

should is_galois go in the namespace?

Patrick Lutz (Oct 26 2020 at 01:08):

oh, maybe not

Patrick Lutz (Oct 26 2020 at 01:08):

I'm not really sure how that works

Patrick Lutz (Oct 26 2020 at 01:09):

but judging off other files in mathlib, maybe not

Patrick Lutz (Oct 26 2020 at 01:09):

Patrick Lutz said:

it does have antitone galois connections I think?

Actually I'm not sure this is true

Thomas Browning (Oct 26 2020 at 01:10):

I guess putting it all in a galois namespace is fine

Patrick Lutz (Oct 26 2020 at 01:11):

Thomas Browning said:

I guess putting it all in a galois namespace is fine

You mean all of galois.lean? I do think that maybe certain things like classes don't always go into namespaces in mathlib, but I'm not really sure

Patrick Lutz (Oct 26 2020 at 01:12):

should I ask about antitone galois connections in one of the bigger streams on zulip?

Patrick Lutz (Oct 26 2020 at 01:13):

Patrick Lutz said:

Thomas Browning said:

I guess putting it all in a galois namespace is fine

You mean all of galois.lean? I do think that maybe certain things like classes don't always go into namespaces in mathlib, but I'm not really sure

although I'm sure anything like that would also get fixed in the PR review process if there's a problem

Thomas Browning (Oct 26 2020 at 01:32):

Patrick Lutz said:

should I ask about antitone galois connections in one of the bigger streams on zulip?

Sure, although isn't an order anti-isomorphism more appropriate, since a galois connection doesn't have to be a bijection?

Thomas Browning (Oct 26 2020 at 01:33):

Patrick Lutz said:

Patrick Lutz said:

Thomas Browning said:

I guess putting it all in a galois namespace is fine

You mean all of galois.lean? I do think that maybe certain things like classes don't always go into namespaces in mathlib, but I'm not really sure

although I'm sure anything like that would also get fixed in the PR review process if there's a problem

Good point.

Patrick Lutz (Oct 26 2020 at 01:40):

Thomas Browning said:

Patrick Lutz said:

should I ask about antitone galois connections in one of the bigger streams on zulip?

Sure, although isn't an order anti-isomorphism more appropriate, since a galois connection doesn't have to be a bijection?

Yeah, that's true.

Patrick Lutz (Oct 26 2020 at 01:40):

It just seems funny that the type of galois_connection that's in mathlib actually doesn't apply to the original galois correspondence

Patrick Lutz (Oct 26 2020 at 02:03):

@Thomas Browning Looks like there's still a few missing docstrings: https://github.com/leanprover-community/mathlib/runs/1306429257

Thomas Browning (Oct 26 2020 at 04:40):

#4786

Patrick Lutz (Oct 26 2020 at 06:16):

@Thomas Browning Isn't this backwards:

- `fixed_field K` where `K : intermediate_field F E`
- `fixing_subgroup H` where `H : subgroup (E ≃ₐ[F] E)`

Like it should be fixed_field H and fixing_subgroup K?

Thomas Browning (Oct 26 2020 at 06:27):

oops, you're right

Johan Commelin (Oct 26 2020 at 07:55):

@Thomas Browning @Patrick Lutz Congrats with this milestone!

Johan Commelin (Oct 26 2020 at 07:56):

I think it would be good to split this into a bunch of smaller PRs

Johan Commelin (Oct 26 2020 at 07:56):

This doesn't have to be a lot of work. If you want some help on how to do this with a bit of git, please let me know.

Thomas Browning (Oct 26 2020 at 17:02):

I manually made a few of the splits that you suggested in the github conversation. The commits often spanned several files, and I wasn't able to figure out the fancy git way to split up the PR

Thomas Browning (Oct 26 2020 at 17:03):

@Johan Commelin

Johan Commelin (Oct 26 2020 at 17:06):

@Thomas Browning I wouldn't reuse the existing git history. Rather, I would do the following:

git checkout the-big-galois-branch # sorry, I didn't look up the name that you are using
git checkout -b new-branch-name
git reset master # this has the effect that all changes of your project are now no longer commited
git status # this will show you exactly which files have changes
git add src/ring_theory/file_1.lean src/algebra/file_2.lean
git commit -am "feat(*): some prerequisites for Galois"
git push

Thomas Browning (Oct 26 2020 at 17:08):

oooh, interesting

Thomas Browning (Oct 26 2020 at 17:08):

should I delete the other PR's then?

Thomas Browning (Oct 26 2020 at 17:09):

or rather, close them?

Johan Commelin (Oct 26 2020 at 17:11):

depends...

Johan Commelin (Oct 26 2020 at 17:11):

I didn't look at them yet.

Johan Commelin (Oct 26 2020 at 17:11):

If they are logical units, then I would just use those

Thomas Browning (Oct 26 2020 at 17:12):

They are #4791 #4792 #4793

Johan Commelin (Oct 26 2020 at 17:12):

From a first glance, I think you can leave those open

Johan Commelin (Oct 26 2020 at 17:13):

And maybe use this approach to create some more PRs

Patrick Lutz (Oct 26 2020 at 18:09):

Johan Commelin said:

Thomas Browning Patrick Lutz Congrats with this milestone!

Thomas did almost all the work for this one btw.

Thomas Browning (Oct 29 2020 at 16:28):

@Johan Commelin I'm a little confused. The three smaller PR's have now been merged, but the galois_definition PR still seems to include the changes to those three files (in the "Files changed" tab on github), even after I ran git merge master.

Thomas Browning (Oct 29 2020 at 16:30):

Presumably there's a way to have the galois_definition PR no longer include changes to those three files?

Johan Commelin (Oct 29 2020 at 17:42):

Hmm weird. You sure you pushed after the git merge? (@Thomas Browning)

Thomas Browning (Oct 29 2020 at 17:44):

I tried:

git checkout master
git pull master
git checkout galois_definition
git merge master
git push

Thomas Browning (Oct 29 2020 at 17:44):

(e.g., https://github.com/leanprover-community/mathlib/pull/4786/commits/29cc4970236ebb6654c95c50e5a6bd5017f33681)

Johan Commelin (Oct 29 2020 at 17:45):

Weird. Maybe someone else can help. I need to do other stuff atm

Patrick Massot (Oct 29 2020 at 17:46):

I guess git push errored, right?

Patrick Massot (Oct 29 2020 at 17:46):

It should have been git push -f

Thomas Browning (Oct 29 2020 at 17:47):

no, it didn't error

Patrick Lutz (Oct 29 2020 at 17:47):

Doesn't the fact that the automatic check detected no merge conflicts with master show that the push was successful?

Patrick Massot (Oct 29 2020 at 17:47):

Do you want me to try?

Patrick Massot (Oct 29 2020 at 17:48):

It would be a bit risky since I have no idea what you're doing

Thomas Browning (Oct 29 2020 at 17:51):

you can go ahead and try

Thomas Browning (Oct 29 2020 at 17:52):

Patrick Lutz said:

Doesn't the fact that the automatic check detected no merge conflicts with master show that the push was successful?

I guess so, but there should be merge conflicts

Patrick Lutz (Oct 29 2020 at 17:53):

Thomas Browning said:

Patrick Lutz said:

Doesn't the fact that the automatic check detected no merge conflicts with master show that the push was successful?

I guess so, but there should be merge conflicts

What do you mean? What I was trying to say is that the automatic check on all pull requests detected no merge conflicts, which seems to indicate that the latest commit does have all the changes from the other PRs. But I could be wrong.

Patrick Massot (Oct 29 2020 at 17:54):

This is definitely conflict

Patrick Massot (Oct 29 2020 at 17:54):

I just did:

  • git checkout master
  • git pull
  • git checkout galois-definition
  • git rebase master

Patrick Massot (Oct 29 2020 at 17:54):

and I get a conflict in src/field_theory/adjoin.lean

Thomas Browning (Oct 29 2020 at 17:55):

ah, what's the definition between git merge and git rebase?

Patrick Lutz (Oct 29 2020 at 17:56):

Patrick Massot said:

and I get a conflict in src/field_theory/adjoin.lean

That's surprising because the three other PRs don't touch field_theory/adjoin.lean

Kevin Buzzard (Oct 29 2020 at 17:56):

IIRC there's a stackoverflow question called that with a gazillion votes

Patrick Massot (Oct 29 2020 at 17:57):

I pushed something

Patrick Lutz (Oct 29 2020 at 17:57):

As far as I know, the difference between merge and rebase is how the commit graph looks

Patrick Lutz (Oct 29 2020 at 17:58):

but I'm hardly a git guru

Patrick Massot (Oct 29 2020 at 17:58):

Does it look better now?

Patrick Lutz (Oct 29 2020 at 17:59):

It looks identical to me

Patrick Lutz (Oct 29 2020 at 17:59):

I think this may be just something to do with the way github displays changes made by a pull request. But I'm not sure

Patrick Massot (Oct 29 2020 at 17:59):

Does it still show stuff as new whereas it's already in mathlib?

Patrick Lutz (Oct 29 2020 at 18:00):

yes

Thomas Browning (Oct 29 2020 at 18:00):

yeah. For a concrete example, mathlib now has equalizer (and also a mem_equalizer lemma)

Thomas Browning (Oct 29 2020 at 18:00):

so I wouldn't expect the PR to have any changes to subalgebra.lean

Patrick Lutz (Oct 29 2020 at 18:01):

but also I detect no changes after what @Patrick Massot just did

Patrick Lutz (Oct 29 2020 at 18:03):

It's surprisingly hard to find information on what github decides to display in the "files changed" tab on pull requests

Patrick Massot (Oct 29 2020 at 18:04):

git got confused by moving stuff

Patrick Massot (Oct 29 2020 at 18:04):

The PR now duplicates this equalizer stuff

Patrick Massot (Oct 29 2020 at 18:04):

It got one from master and one from the PR

Patrick Massot (Oct 29 2020 at 18:05):

Git didn't see any conflict here: master after stuff at line 289 and galois-definition branch added the same stuff at line 260 and those were treated as two disjoint edits by git

Patrick Massot (Oct 29 2020 at 18:05):

So Patrick, if you still have the old galois-definition branch you should force push

Patrick Massot (Oct 29 2020 at 18:06):

(I mean before Thomas's attempted merge)

Patrick Massot (Oct 29 2020 at 18:06):

A lot more manual work will be needed

Patrick Lutz (Oct 29 2020 at 18:06):

okay, let me look into it

Patrick Lutz (Oct 29 2020 at 18:08):

Patrick Massot said:

The PR now duplicates this equalizer stuff

okay, this all makes a lot more sense now

Patrick Massot (Oct 29 2020 at 18:08):

Alternatively someone could fetch the branch as it sits now on GitHub and manually hunt down stuff that you know have been merged

Patrick Massot (Oct 29 2020 at 18:09):

I don't really see how git could have been smarter here, unless it learns about Galois theory.

Patrick Lutz (Oct 29 2020 at 18:09):

Would it have to worked to merge the branches from the other PRs instead of master?

Patrick Lutz (Oct 29 2020 at 18:10):

it might be easiest to just delete stuff by hand

Patrick Massot (Oct 29 2020 at 18:11):

No, git would still have compared the content of the other PRs with the content of galois-definition and see no conflict in this equalizer stuff for instance

Patrick Lutz (Oct 29 2020 at 18:12):

What if the other PRs were from branches that shared a common commit with this branch?

Patrick Massot (Oct 29 2020 at 18:15):

Oh, yes that would help

Patrick Lutz (Oct 29 2020 at 18:16):

Although I'm not sure that's the case here.

Patrick Lutz (Oct 29 2020 at 18:16):

And now those other branches are deleted because the PRs were merged

Patrick Massot (Oct 29 2020 at 18:16):

Life is difficult.

Patrick Lutz (Oct 29 2020 at 18:17):

I mean in this case it shouldn't be too difficult to do by hand

Patrick Lutz (Oct 29 2020 at 18:17):

but if there's a better way it would be nice to figure it out

Johan Commelin (Oct 29 2020 at 18:18):

Patrick Lutz said:

And now those other branches are deleted because the PRs were merged

They still exist on github under refs/pull/1234 (where 1234 is the PR number)

Patrick Lutz (Oct 29 2020 at 18:27):

hmm, but I think they don't share commits in common with the galois_definition branch

Patrick Lutz (Oct 29 2020 at 18:30):

@Thomas Browning, this is only a problem for #4791 right? The stuff in the other two PRs is not duplicated?

Thomas Browning (Oct 29 2020 at 18:42):

nope, it's also a problem for finite_dimensional.lean

Thomas Browning (Oct 29 2020 at 18:43):

algebra_equiv_equiv_algebra_hom is duplicated

Patrick Lutz (Oct 29 2020 at 18:44):

okay, but not for degree_lt_iff_coeff_zero right?

Thomas Browning (Oct 29 2020 at 18:49):

not sure

Patrick Lutz (Oct 29 2020 at 18:50):

okay, I'll double check

Thomas Browning (Oct 29 2020 at 18:53):

that one looks fine

Thomas Browning (Oct 29 2020 at 18:53):

I just pushed some commits where I removed some redundant stuff

Patrick Lutz (Oct 29 2020 at 18:54):

Oh, I was also about to push a commit doing that. I pushed it anyway because it also fixed a typo I noticed

Thomas Browning (Oct 29 2020 at 18:55):

"removing duplicates created by merge": Removes duplicate "i"

Thomas Browning (Oct 29 2020 at 18:55):

lol

Patrick Lutz (Oct 29 2020 at 18:56):

I ran git diff on the files algebra/algebra/subalgebra.lean, linear_algebra/finite_dimensional.lean and data/polynomial/degree/basic.lean comparing them between the galois_definition branch and master and there were no differences (besides the fixed typo). So if those were the only files changed in the other commits then I think everything is fine

Thomas Browning (Oct 29 2020 at 18:56):

they were

Thomas Browning (Oct 29 2020 at 18:56):

we might need to change other files that use those three results

Thomas Browning (Oct 29 2020 at 18:57):

since some namespaces got changed

Patrick Lutz (Oct 29 2020 at 18:57):

oh good point. But I guess that would have happened regardless

Patrick Lutz (Oct 29 2020 at 18:59):

I actually had to turn off the automatic checking in VS Code to edit this since it was causing my computer to crash (from trying to compile large parts of mathlib I guess)

Thomas Browning (Oct 29 2020 at 19:01):

right now I can't edit anything until I can pull the oleans from github (once the compliation finishes)

Thomas Browning (Oct 29 2020 at 19:02):

or rather, I can edit stuff but I can't see whether it worked or not

Patrick Lutz (Oct 29 2020 at 19:02):

I'm trying to do it right now

Patrick Lutz (Oct 29 2020 at 19:18):

Okay, I tried pushing a commit that makes those changes. I guess we'll find out if it worked once it finishes compiling

Patrick Lutz (Oct 29 2020 at 19:36):

hmm, something else has broken somehow. Lean doesn't know about adjoin_le_algebra_adjoin

Patrick Lutz (Oct 29 2020 at 19:42):

hmm, this worries me a lot

Thomas Browning (Oct 29 2020 at 19:50):

@Patrick Lutz I fixed it.

Patrick Lutz (Oct 29 2020 at 19:50):

but do you know how it happened?

Thomas Browning (Oct 29 2020 at 19:50):

That lemma got renamed to adjoin_eq_algebra_adjoin at some point

Patrick Lutz (Oct 29 2020 at 19:50):

but wasn't everything compiling recently?

Patrick Lutz (Oct 29 2020 at 19:50):

was it renamed in the last day?

Thomas Browning (Oct 29 2020 at 19:50):

oh huh

Thomas Browning (Oct 29 2020 at 19:50):

not sure

Thomas Browning (Oct 29 2020 at 19:50):

maybe the rebase did something?

Patrick Lutz (Oct 29 2020 at 19:51):

Yeah, I'm a little confused what's going on

Patrick Lutz (Oct 29 2020 at 20:19):

hmm, somehow nothing else seems to have changed

Patrick Lutz (Oct 29 2020 at 20:19):

as far as I can tell, the adjoin_le_algebra_adjoin thing is the only thing that got messed up

Patrick Lutz (Oct 29 2020 at 20:19):

but I can't figure out how what Patrick did caused that to mess up but nothing else

Patrick Lutz (Oct 29 2020 at 20:21):

I assume it's because of the use of force push but I'm still confused

Johan Commelin (Oct 30 2020 at 05:16):

Hey, please let me know if you need more (git) help.

Thomas Browning (Oct 30 2020 at 05:18):

I think we got it all cleaned up, thanks though

Johan Commelin (Oct 30 2020 at 05:48):

I left a review on github, copying it here:

Thanks for splitting of those 3 PRs. As you may have noticed, those small PRs get quite a bit of feedback, and they aren't merged immediately. The process is slow. I understand that this might feel frustrating at times. But the end product will have a much higher quality.
Having all those small discussions in one big PR would lead to a lot of confusion (or it will just not happen at all, which isn't desirable.)
Ideally, everything that doesn't belong to the actual galois file (and the 1-line change in overview.yaml) should be done in separate PRs.

I hope and expect that you will have less git troubles next time.

Johan Commelin (Oct 30 2020 at 05:49):

Concerning git: I guess if you git merge helper-PR into the galois-branch everytime you process feedback on one of the helper PRs, then the confusion might not happen. (You might get merge conflicts, but it will be easy to fix them. But probably you won't even get merge conflicts.)

Thomas Browning (Oct 30 2020 at 06:19):

How do I handle PRs that depend on each other? For example, the changes to adjoin.lean depend on the changes to adjoin_root.lean which depend on the changes to ring_theory/polynomial/basic.lean

Johan Commelin (Oct 30 2020 at 06:37):

The PR that depends on a smaller one can include the changes from the small one.

Johan Commelin (Oct 30 2020 at 06:38):

I guess if you don't, then CI will throw a bunch of errors.

Johan Commelin (Oct 30 2020 at 06:39):

I wish github was better at handling this... and only show the diff with the dependent PR. (It can do that, but it has the very bad side-effect of deleting the big PR once the smaller PR is merged. :face_palm: :sad: :crying_cat: )

Johan Commelin (Oct 30 2020 at 07:42):

Do you have any plans to follow this up with work on solvable extensions? If you can prove the insolvability of a generic quintic, that would be worth a really nice paper I think. It hasn't been done before in any other library.

Thomas Browning (Oct 30 2020 at 07:55):

Honestly, I hadn't thought that far ahead. I guess we'll discuss our plans at the meeting tomorrow.

Kevin Buzzard (Oct 30 2020 at 08:19):

Quintic hasn't been done in any theorem prover??

Johan Commelin (Oct 30 2020 at 08:22):

It's still open on Freek's list

Kevin Buzzard (Oct 30 2020 at 08:23):

I had it in my head that it was just silly things like FLT which were still open.

Kevin Buzzard (Oct 30 2020 at 08:24):

That's very much an accessible goal for us now

Johan Commelin (Oct 30 2020 at 08:25):

16. Insolvability of General Higher Degree Equations

Thomas Browning (Oct 30 2020 at 21:27):

We're going to go for it!

Thomas Browning (Oct 31 2020 at 00:57):

@Patrick Lutz The PR's now have
noncomputable def alg_hom_adjoin_integral_equiv : (F⟮α⟯ →ₐ[F] K) ≃ (↑((minimal_polynomial h).map (algebra_map F K)).roots.to_finset : set K)
I think this is all we need (+ the modified induction lemma)?

Patrick Lutz (Oct 31 2020 at 02:42):

wow, fast work

Thomas Browning (Oct 31 2020 at 03:11):

well, we basically already had that result, except with the K's replaced by F(a).

Patrick Lutz (Oct 31 2020 at 04:01):

I just merged abel-ruffini with galois_definition to incorporate that change

Jordan Brown (Oct 31 2020 at 04:19):

what would be the best way to state that the commutator of normal subgroups is normal?

Jordan Brown (Oct 31 2020 at 04:19):

as an instance of normal_subgroup?

Patrick Lutz (Oct 31 2020 at 04:22):

Yeah, I think so

Jordan Brown (Oct 31 2020 at 04:44):

I don't think I have permission to push changes to abel-ruffini

Jordan Brown (Oct 31 2020 at 04:45):

also, I'm not sure which file the definition of solvability should go into

Thomas Browning (Oct 31 2020 at 04:55):

@Jordan Brown Send a message like this one: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Access.20to.20Mathlib

Thomas Browning (Oct 31 2020 at 04:55):

I think it's fine to put solvability in abelianization for now (although maybe the file would be better named as commutator.lean)

Patrick Lutz (Oct 31 2020 at 06:26):

@Thomas Browning Should we update abel-ruffini every time galois_definition is changed?

Thomas Browning (Oct 31 2020 at 06:26):

doesn't need to be every time, but whenever it's convenient, I think

Johan Commelin (Oct 31 2020 at 06:28):

At least whenever a PR is merged (or marked as ready to merge).

Patrick Lutz (Oct 31 2020 at 06:49):

@Thomas Browning Do we know that a splitting field of a polynomial is generated (in the sense of adjoin) by the roots of that polynomial? Also, is it worth proving the following induction principle: Suppose PP is some property of intermediate fields of E/FE/F, E=F(a1,,an)E = F(a_1,\ldots, a_n) and for each intermediate field KK such that PP holds of KK and each aia_i, PP holds of K(ai)K(a_i). Then PP holds of EE

Patrick Lutz (Oct 31 2020 at 06:51):

(And assume PP holds for FF of course)

Patrick Lutz (Oct 31 2020 at 06:55):

Just noticed this in intermediate_field.lean:

## TODO

 * `field.adjoin` currently returns a `subalgebra`, this should become an
   `intermediate_field`. The lattice structure on `intermediate_field` will
   follow from the adjunction given by `field.adjoin`.

Presumably it should now be removed

Thomas Browning (Oct 31 2020 at 17:44):

Patrick Lutz said:

Thomas Browning Do we know that a splitting field of a polynomial is generated (in the sense of adjoin) by the roots of that polynomial? Also, is it worth proving the following induction principle: Suppose PP is some property of intermediate fields of E/FE/F, E=F(a1,,an)E = F(a_1,\ldots, a_n) and for each intermediate field KK such that PP holds of KK and each aia_i, PP holds of K(ai)K(a_i). Then PP holds of EE

It's probably not stated now, but it shouldn't be too hard: You do know that the polynomial splits in F(a1,...,an), so there is a map from the splitting field to F(a1,...,an), where F(a1,...,an) is a subfield of the splitting field. By dimension stuff, this alg_hom must be an alg_equiv (this is alg_hom.bijective).

Thomas Browning (Oct 31 2020 at 17:47):

As for the induction, I guess that would be reasonable, although I would probably state it in terms of a set. Either assume that the set is finite or the extension is finite-dimensional. And assume that for each intermediate field K such that P holds of K and each a in S, P holds of K(a). Then P holds of E.

Jordan Brown (Nov 01 2020 at 05:37):

is it okay to push things to the branch if they still have sorrys?

Jordan Brown (Nov 01 2020 at 05:37):

I stated that the commutator of two normal subgroups is normal in the abelianization file but haven't proved it

Jordan Brown (Nov 01 2020 at 05:38):

I could just take it out and push the definition of solvability

Patrick Lutz (Nov 01 2020 at 06:16):

Jordan Brown said:

is it okay to push things to the branch if they still have sorrys?

Sure.

Patrick Lutz (Nov 01 2020 at 06:17):

Jordan Brown said:

I could just take it out and push the definition of solvability

No, definitely leave it in

Thomas Browning (Nov 01 2020 at 07:05):

@Jordan Brown sorries are totally fine. Just make sure that it compiles.

Patrick Lutz (Nov 02 2020 at 19:41):

@Jordan Brown Did you push your changes yet?

Patrick Lutz (Nov 02 2020 at 19:41):

By the way, sorries can actually be pretty good to push because it makes it easier for other people to help out. And it's fun to be able to gradually eliminate sorries from things

Patrick Lutz (Nov 02 2020 at 19:42):

@Thomas Browning I just pushed some small changes to abel-ruffini. In particular, I included statements of the induction principle I mentioned and of the fact that the splitting field is galois.

Patrick Lutz (Nov 02 2020 at 19:43):

But when I pulled the latest changes to the branch, something broke in the proof of alg_hom_adjoin_integral_equiv

Patrick Lutz (Nov 02 2020 at 19:44):

wait, nevermind

Patrick Lutz (Nov 02 2020 at 19:45):

I now ran leanproject get-cache and the problem is gone

Patrick Lutz (Nov 02 2020 at 19:46):

By the way, for our current approach to proving the splitting field is galois, we need to know that being galois is equivalent to the condition that Aut(E/F)=[E:F]|Aut(E/F)| = [E : F], right? Which we don't currently have?

Patrick Lutz (Nov 02 2020 at 19:47):

Also, it would be nice if we had some way to be able to switch between (\bot : intermediate_field F E) and F and likewise between (\top : intermediate_field F E) and E. Do you know of the best way to do that?

Patrick Lutz (Nov 02 2020 at 19:48):

I guess it's necessary to have some statement saying that the field structures on \top and E are the same and that the F-algebra structures are also the same.

Patrick Lutz (Nov 02 2020 at 19:58):

Or actually, maybe it would be better to prove that e.g. \top is equivalent to E as a field and as an F-algebra and then show that being a galois extension is preserved by such equivalences?

Patrick Lutz (Nov 02 2020 at 20:10):

Also, should we at some point introduce special notation for the degree of a field extension? I know it's just findim but it's funny that when you write findim F E it's in the opposite order of the usual notation [E : F]

Patrick Lutz (Nov 02 2020 at 20:44):

Patrick Lutz said:

By the way, for our current approach to proving the splitting field is galois, we need to know that being galois is equivalent to the condition that Aut(E/F)=[E:F]|Aut(E/F)| = [E : F], right? Which we don't currently have?

On the assumption that this hasn't already been done, I started working on a proof. I've now pushed a proof which has a few sorries left (see is_galois_of_card_aut_eq_findim). I realized that with what's already been done, the proof is actually easy in a human sense, but there are still a few annoying parts that I haven't finished.

Thomas Browning (Nov 02 2020 at 21:05):

@Patrick Lutz I can take care of this lemma

Thomas Browning (Nov 02 2020 at 21:07):

oh actually, I see what issue you're running into

Thomas Browning (Nov 02 2020 at 21:08):

passing from E/bot to E/F

Patrick Lutz (Nov 02 2020 at 21:15):

Yeah, and likewise from top/F to E/F

Thomas Browning (Nov 02 2020 at 21:19):

it seems like there really should be some sort of "isomorphism of field extensions"

Thomas Browning (Nov 02 2020 at 21:19):

E/F isomorphic to E'/F'

Patrick Lutz (Nov 02 2020 at 21:19):

Yeah, that's probably the right way to do this

Thomas Browning (Nov 02 2020 at 21:20):

it might be a ring isomorphism taking F to F'

Patrick Lutz (Nov 02 2020 at 21:20):

and we would need to show that things like separability and normality are preserved by isomorphism

Thomas Browning (Nov 02 2020 at 21:20):

yeah

Patrick Lutz (Nov 02 2020 at 21:20):

and galois-ness

Patrick Lutz (Nov 02 2020 at 21:20):

Thomas Browning said:

it might be a ring isomorphism taking F to F'

It also needs to preserve algebra structure

Thomas Browning (Nov 02 2020 at 21:21):

maybe it's a pair of ring isomorphisms E -> E' and F -> F'?

Patrick Lutz (Nov 02 2020 at 21:22):

Sounds reasonable

Thomas Browning (Nov 02 2020 at 21:22):

where would such a thing be defined?

Patrick Lutz (Nov 02 2020 at 21:22):

I don't know

Thomas Browning (Nov 02 2020 at 21:22):

it would have to be below separable.lean and normal.lean, I think

Patrick Lutz (Nov 02 2020 at 21:23):

what does below mean?

Thomas Browning (Nov 02 2020 at 21:23):

in the file structure

Patrick Lutz (Nov 02 2020 at 21:23):

yeah but does below mean "depends on" or "is depended on"?

Thomas Browning (Nov 02 2020 at 21:23):

depends on

Patrick Lutz (Nov 02 2020 at 21:23):

I think it should be independent of separable and normal

Thomas Browning (Nov 02 2020 at 21:23):

oops

Patrick Lutz (Nov 02 2020 at 21:24):

and then separable and normal should have lemmas saying they are preserved by isomorphism

Thomas Browning (Nov 02 2020 at 21:24):

yeah

Thomas Browning (Nov 02 2020 at 21:24):

that's what I meant

Patrick Lutz (Nov 02 2020 at 21:24):

ohh

Patrick Lutz (Nov 02 2020 at 21:24):

maybe one of us should ask some questions on the outside zulip about this

Thomas Browning (Nov 02 2020 at 21:24):

yeah, we should

Patrick Lutz (Nov 02 2020 at 21:25):

like where it should go, how best to state it

Thomas Browning (Nov 02 2020 at 21:25):

I can do that

Patrick Lutz (Nov 02 2020 at 21:25):

sounds good

Patrick Lutz (Nov 02 2020 at 21:26):

btw, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20Together.202021

Patrick Lutz (Nov 02 2020 at 21:27):

also, apparently some stuff about cyclotomic polynomials is about to enter mathlib: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Cyclotomic.20polynomials/near/215254310

Thomas Browning (Nov 02 2020 at 21:34):

It's asked in #maths

Thomas Browning (Nov 02 2020 at 21:34):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Isomorphism.20of.20Field.20Extensions

Jordan Brown (Nov 02 2020 at 22:21):

I just pushed the changes!

Jordan Brown (Nov 02 2020 at 22:22):

Is there a simple proof that the commutator of normal subgroups is normal that is easy to formalize? The proof that I'm thinking of -- where the conjugation is distributed through the product -- seems like it would require a lot of messing with fintypes and such

Patrick Lutz (Nov 02 2020 at 22:23):

@Thomas Browning I just pushed some more changes to abel-ruffini. I noticed that some lemmas about the dimension of intermediate fields were stated only in terms of adjoin for no reason (when they hold for all intermediate fields). Since I needed the more general form, I restated them and added a couple more. Also, I think those lemmas should go in intermediate_field.lean rather than adjoin.lean

Thomas Browning (Nov 02 2020 at 22:23):

well, the generating set is closed under conjugation

Patrick Lutz (Nov 02 2020 at 22:23):

Patrick Lutz said:

Thomas Browning I just pushed some more changes to abel-ruffini. I noticed that some lemmas about the dimension of intermediate fields were stated only in terms of adjoin for no reason (when they hold for all intermediate fields). Since I needed the more general form, I restated them and added a couple more. Also, I think those lemmas should go in intermediate_field.lean rather than adjoin.lean

Also, feel free to plug any sorries that you want to. But I'll also keep working on them

Thomas Browning (Nov 02 2020 at 22:24):

@Jordan Brown so maybe there's a lemma saying that if you take the closure of a set closed under conjugation then the result is normal

Patrick Lutz (Nov 02 2020 at 22:25):

https://leanprover-community.github.io/mathlib_docs/deprecated/subgroup.html#group.normal_closure.is_normal?

Thomas Browning (Nov 02 2020 at 22:26):

The problem is that Jordan is take closure, not normal_closure

Patrick Lutz (Nov 02 2020 at 22:27):

The definition of normal closure in mathlib is group closure of the set of conjugates of a set

Thomas Browning (Nov 02 2020 at 22:28):

oh, that might make it not too bad

Patrick Lutz (Nov 02 2020 at 22:29):

yeah, it would require unfolding the definition of normal_closure a bit but that should work I think

Thomas Browning (Nov 02 2020 at 22:29):

@Jordan Brown so if you can prove that s = conjugates_of_set s then it should follow from normal_closure_normal (this is all in the group_theory/subgroup.lean file)

Patrick Lutz (Nov 02 2020 at 22:30):

@Thomas Browning Do you know if mathlib knows that the top subgroup of a group has the same cardinality as the group?

Patrick Lutz (Nov 02 2020 at 22:30):

If you don't know, I can ask in one of the main streams

Patrick Lutz (Nov 02 2020 at 22:31):

I assume it would be enough to know that there is an isomorphism between (\top : subgroup G) and G

Thomas Browning (Nov 02 2020 at 22:31):

I'd assume so, because of an isomorphism like that, but I don't know exactly

Patrick Lutz (Nov 02 2020 at 22:32):

Yeah, the problem is I can't find such an isomorphism in mathlib right now

Jordan Brown (Nov 02 2020 at 22:37):

ah okay, that does reduce it to something a lot more manageable

Jordan Brown (Nov 02 2020 at 22:38):

also, mathlib is telling me that continuous integration failed on Lint style and Build mathlib; what should I do about this?

Thomas Browning (Nov 02 2020 at 22:38):

in this case, it's just complaining that you used sorry

Thomas Browning (Nov 02 2020 at 22:38):

https://github.com/leanprover-community/mathlib/runs/1344650495

Thomas Browning (Nov 02 2020 at 22:39):

it's worth checking what went wrong, but if it's just sorries then there's nothing to worry about

Patrick Lutz (Nov 02 2020 at 22:41):

and the lint is complaining that some lines have more than 100 characters

Patrick Lutz (Nov 02 2020 at 22:41):

to fix that, just insert newlines in reasonable places so that the lines are less than 100 characters

Patrick Lutz (Nov 02 2020 at 22:41):

VSCode should display a helpful vertical line showing where 100 characters is

Patrick Lutz (Nov 02 2020 at 22:59):

@Thomas Browning sorry if I accidentally derailed the maths thread. Also, I'm not really what sure what the main takeaway is so far

Thomas Browning (Nov 02 2020 at 22:59):

no worries, it's an interesting discussion

Thomas Browning (Nov 02 2020 at 22:59):

although I don't think that the automation will solve the immediate problem at hand

Patrick Lutz (Nov 02 2020 at 23:00):

lol, I agree. At least not this year

Patrick Lutz (Nov 02 2020 at 23:30):

@Thomas Browning I just encountered another place where it would be convenient to change the base field: we already know that E is galois over any fixed field of a subgroup of the set of automorphisms of E. But we would like to know that this means if the fixed points of Aut(E/F)Aut(E/F) are exactly FF then E/FE/F is Galois

Patrick Lutz (Nov 02 2020 at 23:30):

To be fair, this is a place where it would be pretty reasonable to just talk about subfields

Patrick Lutz (Nov 03 2020 at 00:45):

Patrick Lutz said:

Thomas Browning I just pushed some more changes to abel-ruffini. I noticed that some lemmas about the dimension of intermediate fields were stated only in terms of adjoin for no reason (when they hold for all intermediate fields). Since I needed the more general form, I restated them and added a couple more. Also, I think those lemmas should go in intermediate_field.lean rather than adjoin.lean

I realized these lemmas can't go in intermediate_field.lean because they depend on the fact that intermediate_fields form a lattice, which depends on adjoin

Patrick Lutz (Nov 05 2020 at 01:10):

@Jordan Brown I pushed a few style changes to abelianization.lean. I didn't add/change any of the content though

Patrick Lutz (Nov 05 2020 at 01:12):

@Thomas Browning If EE and EE' are equivalent as FF algebras then one way to conclude E/FE/F is Galois if you know E/FE'/F is Galois is to show that FEEF \sub E \sub E' forms an is_scalar_tower and then use is_galois_tower_top_of_is_galois. I tried to start implementing this strategy but ran into problems with Lean's type inference engine

Patrick Lutz (Nov 05 2020 at 01:12):

Note that this strategy wouldn't work for the case where E/FE/F is equivalent to E/FE/F'

Patrick Lutz (Nov 05 2020 at 01:13):

And that case is still needed to translate between the field mul_action.fixed_points G E and the intermediate_field fixed_field G

Thomas Browning (Nov 05 2020 at 01:43):

For that translation, I think you need to show that if K : intermediate_field F E then E/K is Galois iff E/K.to_subfield is Galois. Can't you do something similar? Define a scalar tower and use the galois top result?

Thomas Browning (Nov 05 2020 at 02:01):

actually, I don't think that's quite enough

Thomas Browning (Nov 05 2020 at 02:01):

for is_galois_of_fixed_field_eq_bot, I've reduced it to showing that is_galois (⊥ : intermediate_field F E) E implies is_galois F E

Thomas Browning (Nov 05 2020 at 02:02):

have key : is_galois ( : intermediate_field F E) E,
  { rw h,
    exact galois.is_galois_of_fixed_field E ( : subgroup (E ≃ₐ[F] E)) },

Patrick Lutz (Nov 05 2020 at 02:13):

yeah, I had originally imagined having some kind of result about transferring Galois from E/FE/F to E/FE/F' and then using that to first transfer from mul_action.fixed_points to fixed_field and then rw that to \bot and then use the transfer again to get to F

Patrick Lutz (Nov 05 2020 at 02:13):

did you push the changes you made btw?

Patrick Lutz (Nov 05 2020 at 02:15):

we also need to prove is_galois F (\bot : intermediate_field F E) btw though I don't imagine it will be hard

Patrick Lutz (Nov 05 2020 at 02:34):

Also, have you proved anywhere that if E is a splitting field for p over F and s is the set of roots of p in E then adjoin F s is isomorphic to E as an F-algebra? I don't think that's stated anywhere yet but I wanted to make sure

Thomas Browning (Nov 05 2020 at 02:34):

Patrick Lutz said:

Thomas Browning If EE and EE' are equivalent as FF algebras then one way to conclude E/FE/F is Galois if you know E/FE'/F is Galois is to show that FEEF \sub E \sub E' forms an is_scalar_tower and then use is_galois_tower_top_of_is_galois. I tried to start implementing this strategy but ran into problems with Lean's type inference engine

Wait, don't you have this the wrong way around? Wouldn't is_galois_tower_top_of_galois only tell you that E'/E is Galois?

Thomas Browning (Nov 05 2020 at 02:35):

Patrick Lutz said:

Also, have you proved anywhere that if E is a splitting field for p over F and s is the set of roots of p in E then adjoin F s is isomorphic to E as an F-algebra? I don't think that's stated anywhere yet but I wanted to make sure

I haven't

Patrick Lutz (Nov 05 2020 at 02:35):

Thomas Browning said:

Patrick Lutz said:

Thomas Browning If EE and EE' are equivalent as FF algebras then one way to conclude E/FE/F is Galois if you know E/FE'/F is Galois is to show that FEEF \sub E \sub E' forms an is_scalar_tower and then use is_galois_tower_top_of_is_galois. I tried to start implementing this strategy but ran into problems with Lean's type inference engine

Wait, don't you have this the wrong way around? Wouldn't is_galois_tower_top_of_galois only tell you that E'/E is Galois?

ohh, yeah, oops

Patrick Lutz (Nov 05 2020 at 02:38):

actually, we could use the galois.tower_top thing in one place: if we know that E/FE/F is Galois then we can conclude that EE is Galois over (\bot : intermediate_field F E)

Patrick Lutz (Nov 05 2020 at 02:39):

although I guess I'm not sure if we ever need to do that now that I think about it

Patrick Lutz (Nov 05 2020 at 03:14):

also, did you ever prove that adjoining a set of algebraic elements is the same as algebra adjoin? I see it for adjoining one element (adjoin_simple_to_subalgebra_of_integral) but not for a set

Thomas Browning (Nov 05 2020 at 04:54):

I think we only have it for a single element

Jordan Brown (Nov 06 2020 at 07:09):

does mathlib know that G is a normal subgroup of itself? it seems to know that the trivial subgroup is normal, but when I try to library_search to show that the top subgroup is normal, I get nothing

Kevin Buzzard (Nov 06 2020 at 07:14):

My instinct would be to find the proof that the trivial subgroup is normal in mathlib and then literally look in that file around the area where that result is proved.

Johan Commelin (Nov 06 2020 at 07:55):

@Jordan Brown I think it's missing

Johan Commelin (Nov 06 2020 at 07:55):

Should be a 3-line PR (-;

Jordan Brown (Nov 08 2020 at 02:36):

I just pushed the proof of top.normal and the nth_commutator being normal; it's in abelianization now, but we could definitely split it into its own PR

Jordan Brown (Nov 08 2020 at 02:36):

also, Patrick, have you pushed the cases reduction for the normal commutator proof yet?

Thomas Browning (Nov 09 2020 at 17:46):

@Patrick Lutz @Jordan Brown I've signed up to give a Many Cheerful Facts talk at 12:30. Could we push this week's meeting to 1:30?

Kevin Buzzard (Nov 09 2020 at 17:53):

Do you guys meet in person?

Patrick Lutz (Nov 09 2020 at 18:08):

@Kevin Buzzard No, on zoom. Actually the majority of us are not even physically in Berkeley right now.

Patrick Lutz (Nov 09 2020 at 18:08):

Thomas Browning said:

Patrick Lutz Jordan Brown I've signed up to give a Many Cheerful Facts talk at 12:30. Could we push this week's meeting to 1:30?

Fine with me.

Patrick Lutz (Nov 09 2020 at 18:09):

Jordan Brown said:

also, Patrick, have you pushed the cases reduction for the normal commutator proof yet?

Oh, no, I haven't. I can do it soon.

Patrick Lutz (Nov 09 2020 at 18:10):

By the way, I'm more likely to see your message if you tag me like @Patrick Lutz (which you can do by typing "@" and then my name). But I do check zulip every day or two so I will see eventually no matter what

Patrick Lutz (Nov 09 2020 at 20:54):

@Jordan Brown I've now pushed some changes to abelianization.lean. I also propose we add some basic lemmas about normal_closure to the appropriate file

Patrick Lutz (Nov 09 2020 at 20:55):

E.g. show that normal_closure is idempotent, show that it is always bigger than the subgroup closure, etc

Patrick Lutz (Nov 09 2020 at 20:55):

I can do those myself later today. Or you can do them if you want

Patrick Lutz (Nov 09 2020 at 20:56):

I also think we should prove some theorem of the form "the general_commutator/commutator is equal to the set of commutators (even without taking the subgroup closure/normal_closure)"

Patrick Lutz (Nov 09 2020 at 20:56):

just for convenience

Thomas Browning (Nov 09 2020 at 20:57):

it's not

Thomas Browning (Nov 09 2020 at 20:57):

the commutator subgroup can contain non-commutators

Patrick Lutz (Nov 09 2020 at 21:00):

Thomas Browning said:

the commutator subgroup can contain non-commutators

oh, lol, nevermind then.

Patrick Lutz (Nov 09 2020 at 21:00):

well, at least a lemma saying that for commutator we don't need to use normal_closure

Patrick Lutz (Nov 09 2020 at 21:01):

which should follow from commutator_eq_general_commutator_top_top

Kevin Buzzard (Nov 09 2020 at 21:06):

You could prove that normal closure and forgetful functor form a Galois insertion between normal subgroups and subsets

Kevin Buzzard (Nov 09 2020 at 21:06):

Is this not all already there though?

Kevin Buzzard (Nov 09 2020 at 21:08):

normal_closure is defined in group_theory.subgroup and there's a ton of lemmas about it

Kevin Buzzard (Nov 09 2020 at 21:08):

but the Galois insertion fact doesn't seem to be proved

Patrick Lutz (Nov 09 2020 at 21:14):

Kevin Buzzard said:

Is this not all already there though?

I don't see it

Patrick Lutz (Nov 09 2020 at 21:14):

Kevin Buzzard said:

normal_closure is defined in group_theory.subgroup and there's a ton of lemmas about it

I actually don't see very many lemmas about normal_closure though there are a few (and I don't know that there needs to be that many)

Patrick Lutz (Nov 09 2020 at 21:16):

Thomas Browning said:

Patrick Lutz Jordan Brown I've signed up to give a Many Cheerful Facts talk at 12:30. Could we push this week's meeting to 1:30?

maybe we should even push it a bit later if your talk ends right at 1:30?

Patrick Lutz (Nov 09 2020 at 21:16):

also what are you going to talk about?

Patrick Lutz (Nov 09 2020 at 21:16):

just out of curiosity

Thomas Browning (Nov 09 2020 at 21:18):

Patrick Lutz said:

also what are you going to talk about?

Lean!

Patrick Lutz (Nov 09 2020 at 21:18):

maybe I should go

Thomas Browning (Nov 09 2020 at 21:21):

You're certainly welcome, although you probably won't learn anything new

Patrick Lutz (Nov 09 2020 at 21:22):

are you going to advertise the "Berkeley Lean seminar" (maybe a misleading name at this point)?

Patrick Lutz (Nov 09 2020 at 21:23):

https://github.com/leanprover/lean4/commit/cf7779936419085093ab0ea20f4738dd08030f90 btw

Patrick Lutz (Nov 09 2020 at 21:23):

unrelated

Thomas Browning (Nov 09 2020 at 21:28):

I think I'll mention what we've been doing in Galois theory

Patrick Lutz (Nov 09 2020 at 21:28):

we could consider offering to help newcomers

Patrick Lutz (Nov 09 2020 at 21:28):

who are working through tutorials or w/e

Patrick Lutz (Nov 09 2020 at 21:28):

not that there will necessarily be very many

Patrick Lutz (Nov 09 2020 at 21:29):

or any

Kevin Buzzard (Nov 09 2020 at 21:39):

You're right, they've proved the basics but they didn't prove it was a Galois insertion

Kevin Buzzard (Nov 09 2020 at 21:39):

There is some abstract thing called a closure operator

Kevin Buzzard (Nov 09 2020 at 21:40):

Which satisfies some axioms, which are presumably the ones they prove

Patrick Lutz (Nov 09 2020 at 21:42):

wouldn't a closure operator be idempotent?

Kevin Buzzard (Nov 09 2020 at 22:10):

Normal closure of normal closure is normal closure, right?

Patrick Lutz (Nov 09 2020 at 22:10):

yeah, but that's not proved in mathlib I think

Kevin Buzzard (Nov 09 2020 at 22:11):

Oh well clearly whoever did it did a shoddy job :-) I think I've even seen closure operators axiomatised somewhere -- Wikipedia?

Patrick Lutz (Nov 09 2020 at 23:20):

I mean it's also possible that it's already in mathlib and I just can't find it

Patrick Lutz (Nov 09 2020 at 23:23):

Kevin Buzzard said:

Oh well clearly whoever did it did a shoddy job :-) I think I've even seen closure operators axiomatised somewhere -- Wikipedia?

yeah, there does seem to be an axiomatization on wikipedia. Also apparently if (f,g)(f, g) is a Galois connection then fgf \circ g is a closure operator so proving that the normal closure and forgetful functor form a Galois insertion is a stronger result than showing that normal closure is a closure operator

Kevin Buzzard (Nov 09 2020 at 23:29):

on the other hand, you might need to first prove it's a closure operator to prove it's a Galois insertion :-) I think there are tricks for proving things are Galois insertion -- Bhavik knows them.

Thomas Browning (Nov 09 2020 at 23:32):

@Patrick Lutz You can look at field_theory/adjoin.lean for how to quickly prove Galois insertions

Kevin Buzzard (Nov 09 2020 at 23:32):

my impression is that proving something is a Galois insertion is somehow the "last word" in the API for this sort of thing -- if you have that then you have what most people need.

Kevin Buzzard (Nov 09 2020 at 23:33):

A partial order (or even a preorder) is a poor person's category: a <= b means there's a map from a to b

Kevin Buzzard (Nov 09 2020 at 23:33):

A Galois connection is a pair of adjoint functors between preorders.

Kevin Buzzard (Nov 09 2020 at 23:34):

A Galois insertion is a pair of adjoint functors such that one of the two compositions is the identity map.

Kevin Buzzard (Nov 09 2020 at 23:34):

This sort of stuff works really well in mathlib, it can be thought of as "categories where the hom-sets are in Prop rather than Type"

Patrick Lutz (Nov 09 2020 at 23:35):

Kevin Buzzard said:

on the other hand, you might need to first prove it's a closure operator to prove it's a Galois insertion :-) I think there are tricks for proving things are Galois insertion -- Bhavik knows them.

It doesn't look like it should be too hard in this case. I can do it later this afternoon

Kevin Buzzard (Nov 09 2020 at 23:37):

my memory is that (just like in the adjoint functor setting!) there are a couple of cool constructors for Galois insertions -- you prove a minimal amount of stuff (like closure_mono, closure_subset, closure_closure etc) and then some magic function makes the Galois insertion for you. But I have forgotten the details :-/

Patrick Lutz (Nov 10 2020 at 00:34):

Actually, there seems to be a little problem here. Namely, normal_closure has type set G -> subgroup G not set G -> subgroup.normal G. But actually, the way subgroup.normal is defined right now, it's impossible for normal_closure to have this type; that's because subgroup.normal is a structure with type Prop.

Patrick Lutz (Nov 10 2020 at 00:35):

I propose we redefine subgroup.normal as follows

Patrick Lutz (Nov 10 2020 at 00:36):

right now it looks like this:

structure normal : Prop :=
(conj_mem :  n, n  H   g : G, g * n * g⁻¹  H)

I propose we change this to

structure normal_subgroup :=
(carrier : subgroup G)
(conj_mem :  n, n  carrier   g : G, g * n * g⁻¹  carrier)

Patrick Lutz (Nov 10 2020 at 00:37):

Actually, very confusingly, it looks like this used to be the definition of normal_subgroup in mathlib in the now deprecated file deprecated.subgroup

Patrick Lutz (Nov 10 2020 at 00:37):

It would be nice to know why it was changed

Patrick Lutz (Nov 10 2020 at 01:16):

I just pushed some changes that prove the lemmas I mentioned above. I didn't prove the instance of galois insertion for the reasons I mentioned

Patrick Lutz (Nov 10 2020 at 01:41):

just pushed a commit showing that abelian groups are solvable.

Patrick Lutz (Nov 10 2020 at 03:45):

just pushed a commit proving is_galois F (\bot : intermediate_field F E). Hopefully this wasn't already done somewhere (at least I didn't see it)

Kevin Buzzard (Nov 10 2020 at 07:48):

Yes, I'd recommend you don't bundle normal subgroups. Me and some students built group theory from scratch over the summer (starting with the definition, going up to sylow) and I specifically bundled normal subgroups to see if it made life easier, but the students revolted so we changed it back.

Kevin Buzzard (Nov 10 2020 at 07:48):

They said it was really annoying

Thomas Browning (Nov 10 2020 at 20:32):

@Patrick Lutz #4830 is getting merged. That leaves #4831 (should be quick), and then #4786 (which introduces galois.lean). After this, I can start making smaller PRs with some of the new stuff.

Patrick Lutz (Nov 11 2020 at 18:15):

@Thomas Browning I've run into kind of a weird problem which may just be because I'm doing things in a bad way. I would like to prove that if E/FE/F and K/FK/F are both field extensions and LL is an intermediate field of E/FE/F then there is an equivalence between maps of EE into KK which fix FF and pairs of maps the first of which maps LL into KK fixing FF and the second of which maps EE into KK as an LL-algebra (using the first map to think of KK as an LL-algebra). I stated this as

def alg_hom_equiv_sigma_subalgebra (L : subalgebra F E) :
  (E →ₐ[F] K)  Σ (f : L →ₐ[F] K), @alg_hom L E K _ _ _ _ (ring_hom.to_algebra f)

I have almost proved it, but when proving right_inv I tried using ext and ended up needing to prove a goal of the form x == y. When I looked up what this notation meant I found out it is heq and the documentation for heq says

If you have a goal ⊢ x == y, your first instinct should be to ask (either yourself, or on zulip) if something has gone wrong already.

which seems concerning.

Kevin Buzzard (Nov 11 2020 at 18:46):

Are the types of x and y different?

Kevin Buzzard (Nov 11 2020 at 18:48):

Which one is right_inv? Are you trying to prove that two terms of the sigma type are equal? I can see how one might blunder into a heq there :-/

Kevin Buzzard (Nov 11 2020 at 18:51):

import tactic

example (A B : Type) (F : A  Type) (x y : Σ (a : A), F a) : x = y :=
begin
  ext,
  /-
  A B : Type
  F : A → Type
  x y : Σ (a : A), F a
  ⊢ x.fst = y.fst
  A B : Type
  F : A → Type
  x y : Σ (a : A), F a
  ⊢ x.snd == y.snd
-/
end

Kevin Buzzard (Nov 11 2020 at 18:55):

You start with an f and an alg-hom. You make a map E -> K, and then you make a new f. Is this new f equal to the original one by rfl? If not then you want the alg homs to be equal but they are terms of types which are not definitionally equal; this is exactly what heq is for. Chris Hughes told me he wasn't scared of it any more. But I still am.

Kevin Buzzard (Nov 11 2020 at 18:56):

This is the kind of question which Mario, Reid and Chris are good at

Kevin Buzzard (Nov 11 2020 at 18:58):

There will be ways to avoid the heq which work in your situation, I suspect. The first question is whether the new f and the old f are equal by rfl.

Kevin Buzzard (Nov 11 2020 at 19:00):

You can probably find this out by trying to apply heq_of_eq to your heq goal and seeing if the elaborator can sort things out. If this works you're in the clear.

Kevin Buzzard (Nov 11 2020 at 19:02):

If it doesn't then you might need to call for help.

Kevin Buzzard (Nov 11 2020 at 19:05):

The next possibility is to somehow use the fact that even though x and y are terms of different types, they are both functions from E to K with some properties, so they will be equal if they're the same function. You might need a type theory ninja to reduce it to that though.

Kevin Buzzard (Nov 11 2020 at 19:06):

If you apply sigma.eq instead of sigma.ext you'll end up with a goal with eq.rec in and this is different but also bad (for the same sort of reasons)

Kevin Buzzard (Nov 11 2020 at 19:09):

eq_mpr_heq might be a better approach. eq.recs are hard to get rid of.

Patrick Lutz (Nov 11 2020 at 19:17):

Kevin Buzzard said:

Which one is right_inv? Are you trying to prove that two terms of the sigma type are equal? I can see how one might blunder into a heq there :-/

Yes, right_inv is the part where I need to show two elements of a sigma type are equal. You can see it here

Patrick Lutz (Nov 11 2020 at 19:19):

They are not equal by rfl

Patrick Lutz (Nov 11 2020 at 19:20):

the issue is that when going from (f, g) to a map E -> K I just used g as the map but going back the other way I restrict the map from E -> K to a map L -> K. This is equal to the original f because of the condition commutes' on g but they are not definitionally equal

Patrick Lutz (Nov 11 2020 at 19:23):

Also it's definitely possible that there's a better way to go about this

Kevin Buzzard (Nov 11 2020 at 19:25):

Aah yes, so you have convinced me that the proof is not rfl. I wonder if you can minimise. Hang on a sec...

Kevin Buzzard (Nov 11 2020 at 19:32):

I think that this

import tactic

variables (A B : Type) (S : set A)

example : (A  B)  Σ (f : S  B), {φ : A  B //  (s : A) (h : s  S), φ s = f s, h } :=

might be a better question to ask. This is just pure type theory so people like Mario might respond. I think it has the same problems that your example has, and the important thing is that it's much more minimal so a much more attractive question.

Kevin Buzzard (Nov 11 2020 at 19:33):

The φ s = f ⟨s, h⟩ is some random hypothesis when you're in the middle of all this, so it's not rfl, so I think this example exhibits the same problems that you have.

Kevin Buzzard (Nov 11 2020 at 19:34):

example : (A  B)  Σ (f : S  B), {φ : A  B //  (s : A) (h : s  S), φ s = f s, h } :=
{ to_fun := λ g, λ s, g s.1, sorry⟩,
  inv_fun := λ , fφ.2.1,
  left_inv := sorry,
  right_inv := begin
    intro x,
    ext, sorry,
    -- heq
    sorry
  end }

One can certainly get further with the proof but I think it's "the same heq"

Patrick Lutz (Nov 11 2020 at 19:35):

okay, let me look at it a bit and then I'll ask in one of the bigger streams

Patrick Lutz (Nov 11 2020 at 19:35):

thanks for the help

Kevin Buzzard (Nov 11 2020 at 19:35):

no problem

Kevin Buzzard (Nov 11 2020 at 19:35):

You're all PhD students/post-docs, right?

Kevin Buzzard (Nov 11 2020 at 19:36):

I have a lot of time for people like you

Patrick Lutz (Nov 11 2020 at 19:36):

there aren't very many of us any more. But we're all PhD students I guess

Patrick Lutz (Nov 11 2020 at 19:36):

although I hope to be a postdoc soon

Kevin Buzzard (Nov 11 2020 at 19:36):

yeah, you can go and spread the word elsewhere :-)

Patrick Lutz (Nov 11 2020 at 19:50):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Dealing.20with.20heq.20and.20Sigma.20types

Thomas Browning (Nov 11 2020 at 19:51):

Patrick Lutz said:

the issue is that when going from (f, g) to a map E -> K I just used g as the map but going back the other way I restrict the map from E -> K to a map L -> K. This is equal to the original f because of the condition commutes' on g but they are not definitionally equal

I'm a little confused though, because
have key : alg_hom_extend_base F (alg_hom_compose F L f g) L x = g x := rfl,

Thomas Browning (Nov 11 2020 at 19:52):

doesn't that show that they are definitionally equal pointwise?

Thomas Browning (Nov 11 2020 at 19:54):

Here's the context:

rintros f, g⟩,
    apply sigma.eq,
    { ext,
      have key : alg_hom_extend_base F (alg_hom_compose F L f g) L x = g x := rfl,
      rw  key, },
    { ext,
      exact @alg_hom.commutes' L E K _ _ _ _ (ring_hom.to_algebra f) g x },

Kevin Buzzard (Nov 11 2020 at 19:57):

The problem is perhaps that functional extensionality (pointwise equality implies equality) isn't rfl :-( It might even be basically an axiom of the type theory? The problem with axioms is that they are true by magic.

Kevin Buzzard (Nov 11 2020 at 19:57):

and not by rfl

Patrick Lutz (Nov 11 2020 at 19:59):

Yeah, the problem is that definitional equality means something much stronger than what we normally think of as "mathematical objects being equal"

Patrick Lutz (Nov 11 2020 at 19:59):

it means they are equal for purely syntactic reasons

Patrick Lutz (Nov 11 2020 at 20:00):

literally it means that they can be beta reduced to the same term

Patrick Lutz (Nov 11 2020 at 20:01):

and this is causing problems here because f is being used in the specification of the type of g

Patrick Lutz (Nov 11 2020 at 20:03):

Reid has solved the problem

Thomas Browning (Nov 11 2020 at 20:05):

I saw, although I'm having trouble coming up with the analog of have : f = λ s, φ s.1, sorry,

Kevin Buzzard (Nov 11 2020 at 20:06):

Oh lol, you accused me of making the lambda <a, b> sin :-)

Kevin Buzzard (Nov 11 2020 at 20:06):

I see that you inserted the sin and then claimed it was due to me :-)

Kevin Buzzard (Nov 11 2020 at 20:06):

NB i don't care :-)

Kevin Buzzard (Nov 11 2020 at 20:07):

In your case, you want to prove that the algebra maps are the same before you do the subst

Patrick Lutz (Nov 11 2020 at 20:07):

I didn't realize it was a sin when I inserted it

Kevin Buzzard (Nov 11 2020 at 20:08):

It's fine in proofs in term mode, but if you look at what it does when defining data you get some weird _x.fun_match stuff which just causes noise

Patrick Lutz (Nov 11 2020 at 20:10):

yeah, that makes sense

Kevin Buzzard (Nov 11 2020 at 20:13):

OK so in summary, you don't apply ext, you create a proof that the two alg homs are equal first, and then subst magic might help.

Patrick Lutz (Nov 11 2020 at 20:13):

yeah, the subst thing seems really helpful here

Patrick Lutz (Nov 11 2020 at 20:25):

Thomas Browning said:

I saw, although I'm having trouble coming up with the analog of have : f = λ s, φ s.1, sorry,

hmm, I'm also running into problems. I assumed I should use

have : f = alg_hom_restrict F (alg_hom_compose F L f g) L := sorry,

But when I try to use subst with that, Lean complains about it

Patrick Lutz (Nov 11 2020 at 20:25):

context

subst tactic failed, hypothesis 'this' is not of the form (x = t) or (t = x)
state:
F : Type u_1,
_inst_1 : field F,
E : Type u_2,
_inst_2 : field E,
_inst_3 : algebra F E,
K : Type u_3,
_inst_4 : field K,
_inst_5 : algebra F K,
L : subalgebra F E,
f : L →ₐ[F] K,
g : E →ₐ[L] K,
this : f = alg_hom_restrict F (alg_hom_compose F L f g) L
 alg_hom_restrict F (alg_hom_compose F L f g) L, alg_hom_extend_base F (alg_hom_compose F L f g) L = f, g

Patrick Lutz (Nov 11 2020 at 20:26):

I guess maybe the problem is that you want to subsitute a term for f that contains f?

Patrick Lutz (Nov 11 2020 at 20:27):

which would lead to an infinite loop of substitutions

Patrick Lutz (Nov 11 2020 at 20:37):

no, actually that doesn't seem to be the issue

Patrick Lutz (Nov 11 2020 at 20:37):

This also doesn't work:

    rintros φ, ψ⟩,
    have : φ = {to_fun := λ x, ψ x.val, map_one' := sorry, map_zero' := sorry,
      map_mul' := sorry, map_add' := sorry, commutes' := sorry} := sorry,
    subst this,

Patrick Lutz (Nov 11 2020 at 20:38):

I get the same error where Lean says that the thing I want to substitute is not of the form x = t

Thomas Browning (Nov 11 2020 at 20:40):

Patrick Lutz said:

Thomas Browning said:

I saw, although I'm having trouble coming up with the analog of have : f = λ s, φ s.1, sorry,

hmm, I'm also running into problems. I assumed I should use

have : f = alg_hom_restrict F (alg_hom_compose F L f g) L := sorry,

But when I try to use subst with that, Lean complains about it

I tried that exact same thing

Patrick Lutz (Nov 11 2020 at 20:45):

yeah, but I think that's probably the wrong thing to do because it would replace f with a term that includes f

Patrick Lutz (Nov 11 2020 at 20:45):

we really want to actually replace f with a term that doesn't involve f

Patrick Lutz (Nov 11 2020 at 20:45):

which is why I tried

have : φ = {to_fun := λ x, ψ x.val, map_one' := sorry, map_zero' := sorry,
      map_mul' := sorry, map_add' := sorry, commutes' := sorry} := sorry,

(I had renamed f to phi for clarity)

Patrick Lutz (Nov 11 2020 at 20:45):

but that also didn't work

Patrick Lutz (Nov 11 2020 at 20:46):

but somehow this does work:

import tactic

variables (A B : Type) (S : set A)

structure foo_map (X : Type) (Y : Type) :=
(to_fun : X  Y)
(foo : true)

example : (foo_map A B)  Σ (f : foo_map S B), {φ : A  B //  (s : A) (h : s  S), φ s = f.to_fun s, h } :=
{ to_fun := λ g, ⟨{to_fun := λ s, g.to_fun s.1, foo := trivial}, g.to_fun, λ _ _, rfl⟩⟩,
  inv_fun := λ p, {to_fun := p.2.1, foo := trivial},
  left_inv := sorry,
  right_inv := begin
    rintros f, φ, h⟩,
    have : f = {to_fun := λ s, φ s.1, foo := trivial} := sorry,
    subst this,
  end }

Patrick Lutz (Nov 11 2020 at 20:53):

Patrick Lutz said:

but that also didn't work

although maybe it's somehow because of the sorries in the definition of the term?

Patrick Lutz (Nov 11 2020 at 20:53):

No, I guess not.

Patrick Lutz (Nov 11 2020 at 21:36):

Oh, I think I sort of see why it's happening

Patrick Lutz (Nov 11 2020 at 21:37):

the problem is that I'm trying to substitute \phi for a term that depends on \phi

Patrick Lutz (Nov 11 2020 at 21:37):

but in the second example this dependence is hidden in a sneaky way

Patrick Lutz (Nov 11 2020 at 21:38):

the type of psi depends on phi

Patrick Lutz (Nov 11 2020 at 21:38):

and I'm trying to substitute a term that uses psi

Patrick Lutz (Nov 11 2020 at 21:39):

for instance, this does work (although the sorries are obviously not provable):

    rintros φ, ψ⟩,
    have : φ = {to_fun := λ x, (0 : K), map_one' := sorry, map_zero' := sorry,
      map_mul' := sorry, map_add' := sorry, commutes' := sorry} := sorry,
    subst this,

Kevin Buzzard (Nov 11 2020 at 21:41):

Can you just rewrite instead?

Patrick Lutz (Nov 11 2020 at 21:41):

instead of subst?

Kevin Buzzard (Nov 11 2020 at 21:43):

Yeah, subst is just rewrite

Patrick Lutz (Nov 11 2020 at 21:43):

Lean tells me "motive is not type correct"

Kevin Buzzard (Nov 11 2020 at 21:43):

But rewrite wouldn't mind changing x to f(x)

Kevin Buzzard (Nov 11 2020 at 21:43):

Try simp only this

Patrick Lutz (Nov 11 2020 at 21:44):

Lean tells me "invalid simplification lemma"

Patrick Lutz (Nov 11 2020 at 21:44):

assuming by h you meant this

Kevin Buzzard (Nov 11 2020 at 21:44):

Right

Kevin Buzzard (Nov 11 2020 at 21:45):

So was my example bad? It didn't capture this repetition of f?

Patrick Lutz (Nov 11 2020 at 21:46):

it didn't capture that the type of g depends on f I think

Patrick Lutz (Nov 11 2020 at 21:46):

in your example you can separate out the function

Patrick Lutz (Nov 11 2020 at 21:46):

and forget about the condition on g which is the only thing that depends on f

Patrick Lutz (Nov 11 2020 at 21:46):

maybe that's possible here too

Patrick Lutz (Nov 11 2020 at 21:46):

let me try

Kevin Buzzard (Nov 11 2020 at 21:47):

Failing that you can always go back to the same thread with a better example

Kevin Buzzard (Nov 11 2020 at 21:47):

It's just that saying "I have a problem on this branch of mathlib" is much less likely to get a response

Patrick Lutz (Nov 11 2020 at 21:48):

yeah, I think I might be able to come up with a better example

Patrick Lutz (Nov 11 2020 at 21:48):

like foo_map above but a little more complex

Patrick Lutz (Nov 11 2020 at 21:54):

Patrick Lutz said:

in your example you can separate out the function

I guess the point is that this example also fails

example : (A  B)  Σ (f : S  B), {φ : A  B //  (s : A) (h : s  S), φ s = f s, h } :=
{ to_fun := λ g, λ s, g s.1, g, λ _ _, rfl⟩⟩,
  inv_fun := λ , fφ.2.1,
  left_inv := sorry,
  right_inv := begin
    rintros f, φ⟩,
    have : f = λ s, φ.1 s.1 := sorry,
    subst this,
  end }

for the same reason: \phi seems to depend on f. But changing rintros <f, \phi> to rintros <f, \phi, h> makes that problem go away

Patrick Lutz (Nov 11 2020 at 21:54):

we need something similar here: a way to get the raw function E -> K from psi I think

Patrick Lutz (Nov 11 2020 at 21:55):

but for some reason Lean complains at me if I try to do psi.to_fun

Patrick Lutz (Nov 11 2020 at 21:55):

because it can't remember that K is an L algebra??

Patrick Lutz (Nov 11 2020 at 21:55):

even when I use haveI to give it that instance

Patrick Lutz (Nov 11 2020 at 21:57):

okay, I think I've almost figured it out

Patrick Lutz (Nov 11 2020 at 21:58):

I just need to get Lean to let me write

have q : E -> K := psi.to_fun,

Patrick Lutz (Nov 11 2020 at 21:58):

which it won't let me do because it's very confused about K being an L-algebra??

Patrick Lutz (Nov 11 2020 at 21:59):

okay, I did it

Patrick Lutz (Nov 11 2020 at 22:00):

  right_inv :=
  begin
    rintros φ, ψ, _, _, _, _⟩,
    haveI : algebra L K := ring_hom.to_algebra φ,
    have : φ = {to_fun := λ x, ψ x.val, map_one' := sorry, map_zero' := sorry,
      map_mul' := sorry, map_add' := sorry, commutes' := sorry} := sorry,
    subst this,
    refl,
  end,

Patrick Lutz (Nov 11 2020 at 22:00):

didn't realize I could use rintros that way

Patrick Lutz (Nov 11 2020 at 22:01):

the haveI is unnecessary btw

Patrick Lutz (Nov 11 2020 at 22:01):

although the sorries look a bit annoying

Thomas Browning (Nov 11 2020 at 22:03):

(deleted)

Thomas Browning (Nov 11 2020 at 22:03):

(deleted)

Thomas Browning (Nov 11 2020 at 22:07):

one left:

right_inv :=
  begin
    rintros φ, ψ, h1, h2, h3, h4, h5⟩,
    have : φ = {to_fun := λ x, ψ x.val, map_one' := h1, map_zero' := h3,
      map_mul' := λ x y, h2 x y, map_add' := λ x y, h4 x y, commutes' := sorry },
    { ext, exact (h5 x).symm, },
    subst this,
    refl,
  end,

Patrick Lutz (Nov 11 2020 at 22:13):

the commutes' sorry is giving me trouble. I can prove it, but then subst breaks again!

Thomas Browning (Nov 11 2020 at 22:16):

wait what?

Thomas Browning (Nov 11 2020 at 22:16):

replacing sorry with a proof breaks that subst?

Thomas Browning (Nov 11 2020 at 22:16):

what's your proof?

Patrick Lutz (Nov 11 2020 at 22:16):

      λ x, by {simp *, rw  f.commutes' x,
        exact h5 (algebra_map F L x),}

Patrick Lutz (Nov 11 2020 at 22:17):

actually the first simp is unnecessary

Patrick Lutz (Nov 11 2020 at 22:17):

wait, I think I can fix it

Patrick Lutz (Nov 11 2020 at 22:20):

  right_inv :=
  begin
    rintros ⟨⟨f, _, _, _, _, _⟩, g, h1, h2, h3, h4, hg⟩,
    have : f = λ x, g x.val :=
    begin
      ext,
      exact (hg x).symm,
    end,
    subst this,
    refl,
  end,

Thomas Browning (Nov 11 2020 at 22:20):

woah

Patrick Lutz (Nov 11 2020 at 22:21):

  right_inv :=
  begin
    rintros ⟨⟨f, _, _, _, _, _⟩, g, _, _, _, _, hg⟩,
    have : f = λ x, g x.val := by {ext, exact (hg x).symm},
    subst this,
    refl,
  end,
}

Patrick Lutz (Nov 11 2020 at 22:21):

golfed a little

Thomas Browning (Nov 11 2020 at 22:23):

so is the moral just: intro as much stuff as you can, and hopefully things will get de-tangled?

Patrick Lutz (Nov 11 2020 at 22:23):

I guess so

Patrick Lutz (Nov 11 2020 at 22:23):

at the level of raw functions the situation is basically the same as Kevin's example

Patrick Lutz (Nov 11 2020 at 22:26):

pushed

Patrick Lutz (Nov 12 2020 at 01:34):

https://github.com/leanprover-community/mathlib/commit/85fdd5f6a3b2cbff07e40a3f76b6d6408a07d39f :open_mouth:

Thomas Browning (Nov 12 2020 at 01:51):

there was another one too! https://github.com/leanprover-community/mathlib/commit/0c4f7deb1e2573484e3069e342f35eaabdef59cc

Thomas Browning (Nov 12 2020 at 01:52):

Couldn't figure out how to golf alg_hom_compose though

Thomas Browning (Nov 12 2020 at 01:57):

@Jordan Brown #4982

Patrick Lutz (Nov 12 2020 at 02:12):

we should've been faster I guess

Patrick Lutz (Nov 12 2020 at 02:12):

well, plenty of other PRs for us to do anyway

Patrick Lutz (Nov 12 2020 at 02:16):

Thomas Browning said:

Couldn't figure out how to golf alg_hom_compose though

I think you can almost did what you do for the others but Lean still gets hung up on figuring out how to find an instance of algebra L K. Not sure what to do about that in general

Patrick Lutz (Nov 12 2020 at 09:22):

@Thomas Browning @Jordan Brown https://github.com/ImperialCollegeLondon/group-theory-game/blob/39b4e9c474490a4cf78bb023d44ff0ced3e07310/src/subgroup/basic.lean#L28

Patrick Lutz (Nov 12 2020 at 09:22):

bundled normal subgroups in an Imperial repo

Patrick Lutz (Nov 13 2020 at 00:06):

@Thomas Browning We don't currently have that if [E:F][E : F] is finite then every element of EE is integral over FF right?

Patrick Lutz (Nov 13 2020 at 00:07):

also it would be nice to eventually have that if finite_dimensional F E then fintype (E \to\_a[F] K) no matter what K is

Patrick Lutz (Nov 13 2020 at 00:08):

that might take more work though I guess

Aaron Anderson (Nov 13 2020 at 00:10):

Patrick Lutz said:

Thomas Browning We don't currently have that if [E:F][E : F] is finite then every element of EE is integral over FF right?

This is mostly is_integral_of_noetherian, no?

Thomas Browning (Nov 13 2020 at 00:17):

Patrick Lutz said:

Thomas Browning We don't currently have that if [E:F][E : F] is finite then every element of EE is integral over FF right?

@Patrick Lutz This might follow from results in the algebraic.lean file (namely: finite_dimensional implies algebraic, algebraic implies integral)

Patrick Lutz (Nov 13 2020 at 00:19):

Aaron Anderson said:

Patrick Lutz said:

Thomas Browning We don't currently have that if [E:F][E : F] is finite then every element of EE is integral over FF right?

This is mostly is_integral_of_noetherian, no?

You're right. I just didn't know that theorem was in mathlib

Patrick Lutz (Nov 13 2020 at 00:24):

wait, what's the difference between is_algebraic and is_integral? Just that is_integral does not require the algebra to be commutative and does require the polynomial to be monic?

Patrick Lutz (Nov 13 2020 at 00:29):

Also @Thomas Browning @Jordan Brown is there an easy proof that quotients/subgroups of solvable groups are solvable using the commutator definition of solvable?

Thomas Browning (Nov 13 2020 at 00:30):

subgroup yes: by induction H^(n) <= G^(n)

Patrick Lutz (Nov 13 2020 at 00:34):

it appears that one (minor) problem in proving that is that Lean doesn't know that a subgroup of a subgroup is a subgroup

Patrick Lutz (Nov 13 2020 at 00:34):

at least it can't infer it automatically

Thomas Browning (Nov 13 2020 at 00:47):

sounds like you need a lift from subgroup (H : subgroup G) -> subgroup G

Patrick Lutz (Nov 13 2020 at 01:07):

I agree. Though right now I'm going the lazy way and working at the level of sets instead

Patrick Lutz (Nov 13 2020 at 01:07):

a little annoying though

Patrick Lutz (Nov 13 2020 at 02:14):

@Thomas Browning I've started converting things to lift and should be able to finish subgroup of solvable group is solvable soon. But I have to go do something else first

Patrick Lutz (Nov 13 2020 at 05:16):

okay, it's finished

Patrick Lutz (Nov 13 2020 at 05:17):

though probably not very clean

Patrick Lutz (Nov 13 2020 at 06:15):

Thomas Browning said:

subgroup yes: by induction H^(n) <= G^(n)

now that I actually think of it, quotient is also easy. You just need that if there is a surjection from G1G_1 to G2G_2 then there is a surjection from [G1,G1][G_1, G_1] to [G2,G2][G_2, G_2]

Jordan Brown (Nov 19 2020 at 00:59):

does anyone know why simp will not prove for me that bottom is less than or equal to top in a group

Jordan Brown (Nov 19 2020 at 00:59):

it seems like there are lemmas for bottom being a least element and top being a maximal element, both tagged with simp

Thomas Browning (Nov 19 2020 at 01:13):

it should just be a special case of "bot_le" or "le_top"

Thomas Browning (Nov 19 2020 at 01:14):

simp works for me: example : (⊥ : subgroup G) ≤ (⊤ : subgroup G) := by simp

Jordan Brown (Nov 19 2020 at 03:37):

okay, so my computer is just being weird

Jordan Brown (Nov 19 2020 at 03:37):

that's what I thought

Patrick Lutz (Nov 19 2020 at 03:39):

@Jordan Brown what happens when you try to use simp?

Jordan Brown (Nov 19 2020 at 06:20):

it just says that the tactic failed to simplify

Patrick Lutz (Nov 19 2020 at 06:36):

Jordan Brown said:

it seems like there are lemmas for bottom being a least element and top being a maximal element, both tagged with simp

What happens when you feed simp those lemmas directly?

Kevin Buzzard (Nov 19 2020 at 06:55):

simps job is usually to prove equalities or iffs, I'm always slightly confused about how much further beyond this its remit extends

Patrick Lutz (Nov 19 2020 at 07:01):

I guess the weird part is that simp is doing something different for Jordan than for Thomas and me

Patrick Lutz (Nov 19 2020 at 07:03):

@Jordan Brown what is the exact context in which you are trying to use simp? If it's in the middle of a longer lemma then the actual context may be different from the example that Thomas wrote

Kevin Buzzard (Nov 19 2020 at 08:01):

One of you isn't up to date. There was a lemma added about top and bot in group theory just a few days ago

Patrick Lutz (Nov 19 2020 at 08:10):

Surely bot_le and le_top have been in mathlib since forever though? Since they're just theorems about lattices or something

Patrick Lutz (Nov 19 2020 at 08:11):

and git blame shows that the complete_lattice instance for subgroup G was last touched 6 months ago

Kevin Buzzard (Nov 19 2020 at 08:23):

I just remember that something changed with subgroups and bot and top very recently. It is one possibility for the explanation of the difference in behaviour.

Kevin Buzzard (Nov 19 2020 at 08:24):

There was some missing lemma which was accidentally dropped when subgroups were bundled.

Johan Commelin (Nov 19 2020 at 08:27):

I think it was the lemma that top (or bot) is normal

Kevin Buzzard (Nov 19 2020 at 08:32):

Aah, so this sounds like it is unlikely to have made a difference

Thomas Browning (Nov 22 2020 at 20:28):

@Patrick Lutz I've proved the theorem, modulo the induction lemma

Patrick Lutz (Nov 23 2020 at 07:12):

Nice! Tomorrow I'll think about proving the induction principle

Thomas Browning (Nov 23 2020 at 07:59):

@Patrick Lutz I actually just did it. There's a finset lemma at the top of adjoin.lean that is in #5087

Thomas Browning (Nov 23 2020 at 22:05):

@Patrick Lutz I'm having some trouble with the galois_theory PR: https://github.com/leanprover-community/mathlib/pull/4786#discussion_r529024783

Do you think you could take a look at some point?

Patrick Lutz (Nov 23 2020 at 22:13):

yeah

Kevin Buzzard (Nov 23 2020 at 22:13):

convert key works for me

Kevin Buzzard (Nov 23 2020 at 22:16):

oh no I spoke too soon.

Patrick Lutz (Nov 23 2020 at 22:16):

yeah it says goals accomplished but then also says either deterministic timeout or excessive memory consumption

Patrick Lutz (Nov 23 2020 at 22:17):

it's done both to me now

Kevin Buzzard (Nov 23 2020 at 22:20):

key

Kevin Buzzard (Nov 23 2020 at 22:21):

goal

Kevin Buzzard (Nov 23 2020 at 22:23):

oh crap they are identical!

Patrick Lutz (Nov 23 2020 at 22:23):

well the problem seems to be entirely on the fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) side

Patrick Lutz (Nov 23 2020 at 22:23):

if I rearrange the order of rws that's the part that never works

Patrick Lutz (Nov 23 2020 at 22:26):

actually I'm not so sure

Kevin Buzzard (Nov 23 2020 at 22:26):

so in fact the problem is somewhere else.

Patrick Lutz (Nov 23 2020 at 22:26):

also why is it so slow?

Kevin Buzzard (Nov 23 2020 at 22:27):

because of the real problem

Kevin Buzzard (Nov 23 2020 at 22:27):

If you end with

  rw card_eq_card,
  exact intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  sorry,

then you get an error on the sorry saying "no goals to be solved", so the exact is working fine.

Patrick Lutz (Nov 23 2020 at 22:28):

the goals accomplished coexisting with deterministic timeout is pretty crazy

Kevin Buzzard (Nov 23 2020 at 22:28):

The problem is when Lean's kernel then tries to verify the proof which all the tactics have put together

Kevin Buzzard (Nov 23 2020 at 22:29):

It's not the exact key timing out, it's something else.

Patrick Lutz (Nov 23 2020 at 22:29):

so there's some extra goal hanging around which the infoview isn't showing you?

Patrick Lutz (Nov 23 2020 at 22:29):

because maybe Lean thinks it can be solved by the type inference engine or something?

Patrick Lutz (Nov 23 2020 at 22:29):

but which actually can't

Kevin Buzzard (Nov 23 2020 at 22:30):

This is all at the edge of my understanding, but what I think is happening is that there's a buggy tactic somewhere.

Patrick Lutz (Nov 23 2020 at 22:30):

like a tactic that thinks it solved some goal but actually didn't?

Kevin Buzzard (Nov 23 2020 at 22:31):

Tactics are unverified code. They just throw together something which they claim is a proof, and then the kernel actually checks to see that it is a proof. I believe that the problem is that the kernel is having trouble checking that the proof constructed by the tactics is actually a proof, perhaps because it is not.

Patrick Lutz (Nov 23 2020 at 22:31):

I think the problem is in one of the subproofs

Patrick Lutz (Nov 23 2020 at 22:32):

specifically the replace h_splits proof

Patrick Lutz (Nov 23 2020 at 22:32):

when I replace that with sorry everything works fine

Kevin Buzzard (Nov 23 2020 at 22:32):

Oh good catch!

Patrick Lutz (Nov 23 2020 at 22:33):

something to do with ext1 I think

Kevin Buzzard (Nov 23 2020 at 22:34):

Putting sorry after ext1 and it still compiles.

Kevin Buzzard (Nov 23 2020 at 22:34):

I think the problem is the exact (iso.symm.commutes x).symm line.

Patrick Lutz (Nov 23 2020 at 22:35):

how can exact cause a problem?

Kevin Buzzard (Nov 23 2020 at 22:35):

If you change it to convert then you get the timeout again.

Patrick Lutz (Nov 23 2020 at 22:35):

also when I replace ext1 with ext something funny happens

Patrick Lutz (Nov 23 2020 at 22:35):

I think Lean might be trying to prove that E = F(a)

Kevin Buzzard (Nov 23 2020 at 22:39):

⊢ ⇑(iso.symm) (⇑(algebra_map F E) x) = ⇑(iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E)) x

Kevin Buzzard (Nov 23 2020 at 22:40):

Lean is managing to prove this with refl and then the kernel seems to reject the proof.

Patrick Lutz (Nov 23 2020 at 22:41):

Yeah I tried rwing (iso.symm.commutes x).symm and got that goal

Patrick Lutz (Nov 23 2020 at 22:41):

which then simp hint and tidy couldn't figure out

Patrick Lutz (Nov 23 2020 at 22:42):

and refl works but causes the previous problems. So does exact rfl

Kevin Buzzard (Nov 23 2020 at 22:42):

unfold_coes seems to hang Lean

Kevin Buzzard (Nov 23 2020 at 22:43):

Maybe convert is being too clever.

Patrick Lutz (Nov 23 2020 at 22:44):

congrand refl and exact rfl all cause the same problem

Patrick Lutz (Nov 23 2020 at 22:44):

oh I misunderstood what you said

Kevin Buzzard (Nov 23 2020 at 22:45):

I've never seen unfold_coes hang Lean before.

Kevin Buzzard (Nov 23 2020 at 22:45):

This goal has somehow been corrupted. Perhaps by the convert.

Kevin Buzzard (Nov 23 2020 at 22:45):

Tactics can do that. They can literally make goals which don't make any sense.

Patrick Lutz (Nov 23 2020 at 22:46):

yeah I think you're right that the convert is probably to blame

Kevin Buzzard (Nov 23 2020 at 22:46):

So maybe it is the ext after all.

Patrick Lutz (Nov 23 2020 at 22:46):

lol

Kevin Buzzard (Nov 23 2020 at 22:46):

I don't know which

Kevin Buzzard (Nov 23 2020 at 22:46):

did you say you fiddled with the ext?

Kevin Buzzard (Nov 23 2020 at 22:47):

algebra_map F ↥F⟮α⟯ = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E)

Kevin Buzzard (Nov 23 2020 at 22:47):

What does that mean mathematically?

Patrick Lutz (Nov 23 2020 at 22:48):

some evidence: this works

    have := polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits,
    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E) := sorry,
    rw this,
    assumption,

Kevin Buzzard (Nov 23 2020 at 22:49):

I see. iso is some isomorphism F(α)EF(\alpha)\to E

Patrick Lutz (Nov 23 2020 at 22:49):

yes, established earlier in the proof

Kevin Buzzard (Nov 23 2020 at 22:50):

so the goal seems to make sense mathematically, and ext certainly seems like the next step.

Patrick Lutz (Nov 23 2020 at 22:50):

this proof fails

    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      ext,
      refl,
    },

Patrick Lutz (Nov 23 2020 at 22:50):

even though it works after the convert for the same goal in the original proof

Patrick Lutz (Nov 23 2020 at 22:50):

so I think convert is probably the culprit

Kevin Buzzard (Nov 23 2020 at 22:51):

show_term {ext1} says it's applying ring_hom.ext

Kevin Buzzard (Nov 23 2020 at 22:52):

     apply ring_hom.ext,
     intro x,
     unfold_coes,

works after the convert, so that's a way of unfolding the coes

Patrick Lutz (Nov 23 2020 at 22:52):

actually, I was too hasty but I'm not sure it mattered. This proof hangs

    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      ext,
      rw (iso.symm.commutes x).symm,
      refl,
    },

Kevin Buzzard (Nov 23 2020 at 22:53):

but now rw (iso.symm.commutes x).symm, is failing for me.

Patrick Lutz (Nov 23 2020 at 22:53):

hmm it works for me but then causes the same problems as before

Patrick Lutz (Nov 23 2020 at 22:53):

so now I think you're right and ext really is the problem

Kevin Buzzard (Nov 23 2020 at 22:54):

lol

Kevin Buzzard (Nov 23 2020 at 22:55):

I was about to say "I think you're right, the problem must be with the convert

Patrick Lutz (Nov 23 2020 at 22:55):

but there's no more convert anywhere

Patrick Lutz (Nov 23 2020 at 22:56):

this proof works fine

  cases field.exists_primitive_element h.1 with α ,
  have iso : Fα ≃ₐ[F] E,
  {
    -- sorry,
    rw ,
    exact intermediate_field.top_equiv
    },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  {
    have := polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits,
    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      sorry,
    },
    rw this,
    assumption,
    },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,

Patrick Lutz (Nov 23 2020 at 22:57):

this proof has all the same problems as the original

  cases field.exists_primitive_element h.1 with α ,
  have iso : Fα ≃ₐ[F] E,
  {
    -- sorry,
    rw ,
    exact intermediate_field.top_equiv
    },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  {
    have := polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits,
    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      ext,
      rw  iso.symm.commutes x,
      refl,
    },
    rw this,
    assumption,
    },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,

Kevin Buzzard (Nov 23 2020 at 23:00):

It's just apply ring_hom.ext.

Patrick Lutz (Nov 23 2020 at 23:02):

yeah but there's literally no more converts in the proof

Kevin Buzzard (Nov 23 2020 at 23:02):

annoyingly, extract_goal doesn't give you a failing example.

Patrick Lutz (Nov 23 2020 at 23:03):

well this also fails

    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      apply ring_hom.ext,
      intros x,
      rw  iso.symm.commutes x,
      refl,
    },

Patrick Lutz (Nov 23 2020 at 23:04):

maybe it's the refl that's the problem??

Kevin Buzzard (Nov 23 2020 at 23:05):

example (F : Type u_1) (E : Type u_2)
  [field F]
  [field E]
  [algebra F E]
  [finite_dimensional F E]
  [h : is_galois F E]
  (α : E)
  ( : Fα = )
  (iso : Fα ≃ₐ[F] E)
  (H : is_integral F α)
  (h_sep : (minimal_polynomial H).separable)
  (h_splits : polynomial.splits (algebra_map F E) (minimal_polynomial H))
  (this : polynomial.splits
            (iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E))
            (minimal_polynomial H)) :
  algebra_map F Fα =
    iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E) :=
begin
  apply ring_hom.ext,
  intro x,
  unfold_coes,
  exact (iso.symm.commutes x).symm,
end

works fine

Kevin Buzzard (Nov 23 2020 at 23:06):

I used extract_goal to get exactly what we thought the problem was.

Patrick Lutz (Nov 23 2020 at 23:06):

this is bizarre

Kevin Buzzard (Nov 23 2020 at 23:06):

If we could minimise we could ask a much better question.

Patrick Lutz (Nov 23 2020 at 23:06):

yeah

Patrick Lutz (Nov 23 2020 at 23:07):

I just ran into a weird thing where dsimp does something and squeeze_dsimp suggests dsimp only but dsimp only fails

Kevin Buzzard (Nov 23 2020 at 23:08):

This works, with the sorry in the other place. Maybe you already said that.

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  have iso : Fα ≃ₐ[F] E,
  {
    sorry,
    },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  {
    have := polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits,
    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
       apply ring_hom.ext,
       intro x,
       exact (iso.symm.commutes x).symm,
    },
    rw this,
    assumption,
    },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,
end

Patrick Lutz (Nov 23 2020 at 23:09):

ohh I didn't try that

Kevin Buzzard (Nov 23 2020 at 23:09):

I think this is just an indication that we're looking in the wrong place.

Patrick Lutz (Nov 23 2020 at 23:09):

I tried putting sorry in both

Patrick Lutz (Nov 23 2020 at 23:09):

yeah I agree

Patrick Lutz (Nov 23 2020 at 23:09):

so a sorry anywhere in the proof makes it work??

Kevin Buzzard (Nov 23 2020 at 23:11):

no

Patrick Lutz (Nov 23 2020 at 23:12):

this works:

lemma foo [finite_dimensional F E] [h : is_galois F E] (α : E) ( : Fα = ):
  Fα ≃ₐ[F] E := sorry

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  have iso := foo F E α ,
  -- have iso : F⟮α⟯ ≃ₐ[F] E,
  -- {
  --   -- sorry,
  --   rw hα,
  --   exact intermediate_field.top_equiv
  --   },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  {
    have := polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits,
    have : algebra_map F Fα = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E),
    {
      apply ring_hom.ext,
      intros x,
      rw  iso.symm.commutes x,
      refl,
    },
    rw this,
    assumption,
    },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,
  -- sorry,
end

Patrick Lutz (Nov 23 2020 at 23:12):

so I think iso is somehow causing problems

Patrick Lutz (Nov 23 2020 at 23:13):

I conjecture that replacing iso with a term mode proof will fix the problems

Patrick Lutz (Nov 23 2020 at 23:13):

it fails again when I fill in foo with a tactic mode proof

Kevin Buzzard (Nov 23 2020 at 23:16):

Your lemma should be a def

Kevin Buzzard (Nov 23 2020 at 23:17):

let iso : F⟮α⟯ ≃ₐ[F] E,

Patrick Lutz (Nov 23 2020 at 23:18):

ohh

Kevin Buzzard (Nov 23 2020 at 23:18):

unfortunately this doesn't fix it :-(

Kevin Buzzard (Nov 23 2020 at 23:19):

You shouldn't be proving this in tactic mode

Patrick Lutz (Nov 23 2020 at 23:19):

yeah, see my conjecture

Kevin Buzzard (Nov 23 2020 at 23:19):

This is the problem

Kevin Buzzard (Nov 23 2020 at 23:19):

I mean, this is _a_ problem

Thomas Browning (Nov 23 2020 at 23:20):

Just saw this thread. Is the consensus that tactic-mode iso is likely the only culprit?

Kevin Buzzard (Nov 23 2020 at 23:21):

The proof of iso should be to beef up h\alpha to an isomorphism and then to apply transitivity of isomorphisms.

Kevin Buzzard (Nov 23 2020 at 23:22):

Lean is getting stuck on the eq.rec which the rw is inserting.

Kevin Buzzard (Nov 23 2020 at 23:22):

If you change the have to a let (which it should have been) then the problems show up earlier with stuff taking a long time.

Patrick Lutz (Nov 23 2020 at 23:23):

how can I say very concisely in Lean that if A = B then A \equiv B?

Patrick Lutz (Nov 23 2020 at 23:24):

I can't find any lemma to that effect in mathlib

Patrick Lutz (Nov 23 2020 at 23:24):

Thomas Browning said:

Just saw this thread. Is the consensus that tactic-mode iso is likely the only culprit?

I'm not confident but I think that's the strongest contender right now

Kevin Buzzard (Nov 23 2020 at 23:24):

That's a definition, not a lemma.

Patrick Lutz (Nov 23 2020 at 23:24):

well I can't find that definition either

Kevin Buzzard (Nov 23 2020 at 23:25):

/-- Linear equivalence between two equal submodules. -/
def of_eq (h : p = q) : p ≃ₗ[R] q :=
{ map_smul' := λ _ _, rfl, map_add' := λ _ _, rfl, .. equiv.set.of_eq (congr_arg _ h) }

Kevin Buzzard (Nov 23 2020 at 23:26):

Not the one you want, but it looks like we're looking for of_eq

Thomas Browning (Nov 23 2020 at 23:26):

If the algebra version is not in mathlib, we can just add it, right?

Kevin Buzzard (Nov 23 2020 at 23:30):

def algebra.of_eq {p q : subalgebra F E} (h : p = q) : p ≃ₐ[F] q :=
{ to_fun := λ x, x.1, h  x.2⟩,
  inv_fun := λ y, y.1, h.symm  y.2⟩,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := sorry,
  map_add' := sorry,
  commutes' := sorry }

That's a start

Kevin Buzzard (Nov 23 2020 at 23:34):

There's no alg_equiv.comp?

Kevin Buzzard (Nov 23 2020 at 23:35):

oh it's trans

Patrick Lutz (Nov 23 2020 at 23:35):

yeah but I'm having a hard time using it

Patrick Lutz (Nov 23 2020 at 23:35):

the types of things don't quite match up

Kevin Buzzard (Nov 23 2020 at 23:38):

How do I turn an intermediate_field into a subalgebra?

Kevin Buzzard (Nov 23 2020 at 23:39):

h\alpha is an equality of intermediate_fields

Patrick Lutz (Nov 23 2020 at 23:39):

.to_subalgebra

Kevin Buzzard (Nov 23 2020 at 23:43):

Here's a cool error (note I do _not_ have pp.all on):

type mismatch at application
  (algebra.of_eq F E hα').trans intermediate_field.top_equiv
term
  intermediate_field.top_equiv
has type
  @alg_equiv F
    (@coe_sort (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@intermediate_field.has_coe_to_sort F E _inst_1 _inst_2 _inst_3)
       (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                   (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))))
    E
    (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
    (@ring.to_semiring
       (@coe_sort (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@intermediate_field.has_coe_to_sort F E _inst_1 _inst_2 _inst_3)
          (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                   (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                      (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))))
       (@division_ring.to_ring
          (@coe_sort (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@intermediate_field.has_coe_to_sort F E _inst_1 _inst_2 _inst_3)
             (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                   (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                      (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                         (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))))
          (@field.to_division_ring
             (@coe_sort (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@intermediate_field.has_coe_to_sort F E _inst_1 _inst_2 _inst_3)
                (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                   (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                      (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                         (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                            (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))))
             (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                   (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                      (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                         (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))).to_field)))
    (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
    (@has_top.top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
       (@order_top.to_has_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
          (@bounded_lattice.to_order_top (@intermediate_field F E _inst_1 _inst_2 _inst_3)
             (@complete_lattice.to_bounded_lattice (@intermediate_field F E _inst_1 _inst_2 _inst_3)
                (@intermediate_field.complete_lattice F _inst_1 E _inst_2 _inst_3))))).algebra
    _inst_3
but is expected to have type
  @alg_equiv F
    (@coe_sort
       (@subalgebra F E
          (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
          (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
          _inst_3)
       (@coe_sort_trans
          (@subalgebra F E
             (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
             (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
             _inst_3)
          (@submodule F E
             (@comm_semiring.to_semiring F
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
             (@semiring.to_add_comm_monoid E
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2))))
             (@algebra.to_semimodule F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3))
          (@submodule.has_coe_to_sort F E
             (@comm_semiring.to_semiring F
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
             (@semiring.to_add_comm_monoid E
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2))))
             (@algebra.to_semimodule F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3))
          (@coe_base_aux
             (@subalgebra F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3)
             (@submodule F E
                (@comm_semiring.to_semiring F
                   (@comm_ring.to_comm_semiring F
                      (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1))))
                (@semiring.to_add_comm_monoid E
                   (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2))))
                (@algebra.to_semimodule F E
                   (@comm_ring.to_comm_semiring F
                      (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                   (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                   _inst_3))
             (@subalgebra.coe_to_submodule F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3)))
       (@has_top.top
          (@subalgebra F E
             (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
             (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
             _inst_3)
          (@order_top.to_has_top
             (@subalgebra F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3)
             (@bounded_lattice.to_order_top
                (@subalgebra F E
                   (@comm_ring.to_comm_semiring F
                      (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                   (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                   _inst_3)
                (@complete_lattice.to_bounded_lattice
                   (@subalgebra F E
                      (@comm_ring.to_comm_semiring F
                         (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                      (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                      _inst_3)
                   (@algebra.subalgebra.complete_lattice F E
                      (@comm_ring.to_comm_semiring F
                         (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                      (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                      _inst_3))))))
    E
    (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
    (@subalgebra.semiring F E
       (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
       (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
       _inst_3
       (@has_top.top
          (@subalgebra F E
             (@comm_ring.to_comm_semiring F (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
             (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
             _inst_3)
          (@order_top.to_has_top
             (@subalgebra F E
                (@comm_ring.to_comm_semiring F
                   (@euclidean_domain.to_comm_ring F (@field.to_euclidean_domain F _inst_1)))
                (@ring.to_semiring E (@division_ring.to_ring E (@field.to_division_ring E _inst_2)))
                _inst_3)
             (@bounded_lattice.to_order_top
...

Patrick Lutz (Nov 23 2020 at 23:43):

lol

Kevin Buzzard (Nov 23 2020 at 23:43):

So perhaps we're getting closer to the heart of the problem

Kevin Buzzard (Nov 23 2020 at 23:45):

Unfortunately I need to sleep. I think the challenge is to prove iso : F⟮α⟯ ≃ₐ[F] E using transitivity of isomorphisms, but it seems to me that there is some sort of subtle problem, perhaps coming from structure maps not being defeq.

Patrick Lutz (Nov 23 2020 at 23:46):

okay, good night

Patrick Lutz (Nov 23 2020 at 23:47):

This works

def bar {A B C : Type*} [field A] [field B] [field C] [algebra A B] [algebra A C] (h : B = C) :
  B ≃ₐ[A] C := sorry

def foo [finite_dimensional F E] [h : is_galois F E] (α : E) ( : Fα = ):
  Fα ≃ₐ[F] E :=
begin
    refine alg_equiv.trans _ intermediate_field.top_equiv,
    library_search,
end

but library_search suggest exact bar _ and when I try that it fails

Kevin Buzzard (Nov 23 2020 at 23:47):

Try convert bar _

Kevin Buzzard (Nov 23 2020 at 23:47):

although again you shouldn't be using convert in a definition.

Patrick Lutz (Nov 23 2020 at 23:48):

also this gives me a very weird error

    have := bar ,

Patrick Lutz (Nov 23 2020 at 23:48):

type mismatch at application
  bar 
term
  
has type
  Fα = 
but is expected to have type
  ?m_1 = ?m_2

Kevin Buzzard (Nov 23 2020 at 23:48):

And you shouldn't be sorrying the definition of bar. Sorrying definitions can lead to trouble.

Patrick Lutz (Nov 23 2020 at 23:48):

I'm just trying to figure out what's going on

Kevin Buzzard (Nov 23 2020 at 23:48):

def algebra.of_eq {p q : subalgebra F E} (h : p = q) : p ≃ₐ[F] q :=
{ to_fun := λ x, x.1, h  x.2⟩,
  inv_fun := λ y, y.1, h.symm  y.2⟩,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := sorry,
  map_add' := sorry,
  commutes' := sorry }

This is better because I only sorry the proofs.

Kevin Buzzard (Nov 23 2020 at 23:49):

But I do introduce an eq.subst in the definition, which is already a bit hairy.

Kevin Buzzard (Nov 23 2020 at 23:50):

have := bar h\a is problematic because again you're using have for a definition, but also Lean can't be expected to figure out A from h, that's what the error means.

Kevin Buzzard (Nov 23 2020 at 23:51):

Just because B is an A-algebra doesn't mean that B can't be a W-algebra for some random other W, so the unifier can't solve the problem.

Patrick Lutz (Nov 23 2020 at 23:51):

oh I see

Kevin Buzzard (Nov 23 2020 at 23:54):

I cannot see how to avoid eq.subst or eq.rec here.

Kevin Buzzard (Nov 23 2020 at 23:54):

Why not just ask how to construct F⟮α⟯ ≃ₐ[F] E from F⟮α⟯ = ⊤? That sounds like a reasonable question.

Kevin Buzzard (Nov 23 2020 at 23:55):

Or you could just change the have to a let in the PR (note that the PR still contains the error in the definition of iso) and then ask people to have a look at that, but they're more likely to try the simpler question.

Kevin Buzzard (Nov 23 2020 at 23:56):

Note finally that exactly the same thing happened to Johan, Patrick and I when we were finishing the perfectoid project. We had a file which we thought was the end of it all, but couldn't tie everything together. Mario sorted out our problems in about 15 minutes flat.

Kevin Buzzard (Nov 23 2020 at 23:57):

By then we'd figured out the knack of asking the right questions of course. We weren't expecting Mario to know what a perfectoid space was :-)

Patrick Lutz (Nov 23 2020 at 23:57):

Yeah I think I can figure out how to ask a reasonable version of this question

Kevin Buzzard (Nov 23 2020 at 23:57):

We had exactly the same sort of problem, a proof which should have been refl but was instead a big time-out.

Kevin Buzzard (Nov 23 2020 at 23:57):

Sorry I couldn't solve it. I'm still learning when it comes to technical issues like this.

Patrick Lutz (Nov 23 2020 at 23:58):

lol no problem. I think we understand much better now what's going on

Kevin Buzzard (Nov 24 2020 at 00:01):

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  have hα' : Fα⟯.to_subalgebra = , rw , simp,
  let iso : Fα ≃ₐ[F] E := by refine {
    to_fun := λ e, e.1,
  inv_fun := λ e, e, begin sorry end⟩,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := sorry,
  map_add' := sorry,
  commutes' := sorry },
  -- { rw hα,
  --   exact intermediate_field.top_equiv },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  { convert polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,
end

Kevin Buzzard (Nov 24 2020 at 00:01):

this compiles and the only sorrys are props.

Kevin Buzzard (Nov 24 2020 at 00:03):

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  have hα' : Fα⟯.to_subalgebra = , rw , simp,
  let iso : Fα ≃ₐ[F] E := {
    to_fun := λ e, e.1,
  inv_fun := λ e, e, begin sorry end⟩,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := sorry,
  map_add' := sorry,
  commutes' := sorry },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  { convert polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,
end

Patrick Lutz (Nov 24 2020 at 00:04):

oh nice

Kevin Buzzard (Nov 24 2020 at 00:05):

I bet if you fill in those sorries it will compile.

Kevin Buzzard (Nov 24 2020 at 00:07):

I think the heart of the matter was always the bad definition of iso. Initially the problem was that it was defined using have so Lean didn't even have access to the maps. That was why we were getting timeout behaviour -- Lean was looking for stuff that wasn't there. When we changed it to let it could see the maps but they were some diabolical things, so the proof started timing out and Lean was now in some sense behaving "normally" (no weird errors, just timeouts because Lean could not reduce the maps to check they were equal). Here the key difference is that I am writing down the maps explicitly, so they're really easy to work with.

Kevin Buzzard (Nov 24 2020 at 00:10):

The proof takes a while to compile. Here's how to work on it: add sorry end #exit.

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  let iso : Fα ≃ₐ[F] E := {
    to_fun := λ e, e.1,
  inv_fun := λ e, e, begin rw , exact intermediate_field.mem_top end⟩,
  left_inv := sorry,
  right_inv := sorry,
  map_mul' := sorry,
  map_add' := sorry,
  commutes' := sorry },
  sorry end #exit
  have H : is_integral F α := h.is_integral α,

Kevin Buzzard (Nov 24 2020 at 00:12):

lemma card_aut_eq_findim_of_is_galois [finite_dimensional F E] [h : is_galois F E] :
  fintype.card (E ≃ₐ[F] E) = findim F E :=
begin
  cases field.exists_primitive_element h.1 with α ,
  let iso : Fα ≃ₐ[F] E := {
    to_fun := λ e, e.1,
  inv_fun := λ e, e, begin rw , exact intermediate_field.mem_top end⟩,
  left_inv := λ e, begin ext, refl, end,
  right_inv := λ e, rfl,
  map_mul' := λ x y, rfl,
  map_add' := λ x y, rfl,
  commutes' := λ x, rfl },
  have H : is_integral F α := h.is_integral α,
  have h_sep : (minimal_polynomial H).separable := h.separable α,
  have h_splits : (minimal_polynomial H).splits (algebra_map F E) := h.normal α,
  replace h_splits : polynomial.splits (algebra_map F Fα) (minimal_polynomial H),
  { convert polynomial.splits_comp_of_splits (algebra_map F E) iso.symm.to_alg_hom.to_ring_hom h_splits },
  rw  linear_equiv.findim_eq iso.to_linear_equiv,
  have card_eq_card : fintype.card (E ≃ₐ[F] E) = fintype.card (Fα ≃ₐ[F] Fα),
  { apply fintype.card_congr,
    apply equiv.mk (λ ϕ, iso.trans (trans ϕ iso.symm)) (λ ϕ, iso.symm.trans (trans ϕ iso)),
    { intro ϕ, ext1, simp only [trans_apply, apply_symm_apply] },
    { intro ϕ, ext1, simp only [trans_apply, symm_apply_apply] } },
  rw card_eq_card,
  have key := intermediate_field.adjoin_simple.card_aut_eq_findim F E H h_sep h_splits,
  exact key,
end

Compiles!

Kevin Buzzard (Nov 24 2020 at 00:12):

:D

Kevin Buzzard (Nov 24 2020 at 00:12):

It's amazing how stopping for 5 minutes and doing something else can inspire you.

Kevin Buzzard (Nov 24 2020 at 00:14):

Actually this was something I learnt in Berkeley. I would often be working late at night in the department on something, and then get hungry, so I'd have to stop working and wander up to Euclid or Telegraph to get something to eat.

Patrick Lutz (Nov 24 2020 at 00:14):

yeah I also just arrived at that proof

Patrick Lutz (Nov 24 2020 at 00:14):

the intermediate_field.mem_top was a little tricky

Kevin Buzzard (Nov 24 2020 at 00:15):

And it was amazing how many times during that walk I thought "hey why don't I try something completely different" or "hey, actually, it's completely obvious that what I've been trying to do for the last 4 hours can never work"

Patrick Lutz (Nov 24 2020 at 00:15):

unfortunately I can no longer go to Euclid for dinner :'(

Kevin Buzzard (Nov 24 2020 at 00:15):

Patrick Lutz said:

yeah I also just arrived at that proof

Yeah the entire process was collaborative.

Patrick Lutz (Nov 24 2020 at 00:15):

or Evans

Kevin Buzzard (Nov 24 2020 at 00:16):

That's the really great thing about Zulip. When I was in Berkeley we had sci.math.research which moved at a far slower pace. This really makes a difference.

Kevin Buzzard (Nov 24 2020 at 00:16):

I can't figure out why trivial didn't do the intermediate_field.mem_top thing. I also got stuck there.

Patrick Lutz (Nov 24 2020 at 00:16):

I've heard so many stories of the days of usenet

Patrick Lutz (Nov 24 2020 at 00:17):

but I was born at the end of the eternal september

Kevin Buzzard (Nov 24 2020 at 00:17):

s.m.r was moderated so it was impossible to have a conversation which went at any speed beyond about 2 exchanges per day.

Kevin Buzzard (Nov 24 2020 at 00:17):

But you have to put this into context -- my supervisor couldn't even have that.

Kevin Buzzard (Nov 24 2020 at 00:17):

s.m.r. gave you access to experts. It was a game-changer.

Kevin Buzzard (Nov 24 2020 at 00:18):

Before email you asked your advisor and if they couldn't help you were _stuck_.

Kevin Buzzard (Nov 24 2020 at 00:18):

whereas I could email the author of the paper to ask them about the proof of lemma 13.7 and if I was lucky they'd respond.

Kevin Buzzard (Nov 24 2020 at 00:19):

(and if you made it clear you'd thought hard and weren't asking a stupid question, they often would respond, unless they were too old to use email)

Kevin Buzzard (Nov 24 2020 at 00:19):

Then mathoverflow came, and now we have things like this.

Kevin Buzzard (Nov 24 2020 at 00:20):

In my academic lifetime I've seen several revolutions. And you kids just think it's all normal :-)

Kevin Buzzard (Nov 24 2020 at 00:20):

I am really surprised my partner has not come and grabbed me by the ear and told me it's time for bed.

Kevin Buzzard (Nov 24 2020 at 00:20):

She's engrossed in something else in the next room :-)

Kevin Buzzard (Nov 24 2020 at 00:21):

Anyway, what's going on with intermediate_field.mem_top? How can that not be defeq to x \in univ, and that's defeq to true, so trivial usually solves these things.

Kevin Buzzard (Nov 24 2020 at 00:22):

lemma mem_top {x : E} : x  ( : intermediate_field F E) :=
subfield.subset_closure $ or.inr trivial

o_O

Kevin Buzzard (Nov 24 2020 at 00:23):

I think top : intermediate_field F E must be defined as the closure of univ!

Patrick Lutz (Nov 24 2020 at 00:23):

yeah I guess so

Patrick Lutz (Nov 24 2020 at 00:23):

I think the problem might be that the lattice structure comes from a galois insertion between adjoin and the forgetful functor

Patrick Lutz (Nov 24 2020 at 00:23):

but I don't really know what I'm talking about

Patrick Lutz (Nov 24 2020 at 00:25):

so \top in intermediate fields is really something like F adjoin (\top in sets)

Patrick Lutz (Nov 24 2020 at 00:25):

and adjoin is defined using subfield.subset_closure

Kevin Buzzard (Nov 24 2020 at 00:26):

I think this is Thomas' doing. He's proved the existence of a Galois insertion between coe and adjoin, and then used that to inherit the structure of a complete lattice on the intermediate fields coming from the complete lattice structure on the subsets. Presumably as part of that, top is defined to be something like "adjoin everything" rather than "everything". The CS people might be a bit upset about that, but I think this is OK; the way to prove that you're in top is mem_top, not some clever proof like trivial which I was trying. We shouldn't be relying on definitional equality.

Patrick Lutz (Nov 24 2020 at 00:27):

wait, isn't that basically what I just said?

Kevin Buzzard (Nov 24 2020 at 00:27):

Yes, but I hadn't read what you were typing, I was too busy typing it myself :D

Patrick Lutz (Nov 24 2020 at 00:27):

lol, happens to me sometimes too

Kevin Buzzard (Nov 24 2020 at 00:29):

I am terrible at names, and it's very rude to get someone's name wrong, so I scrolled up all the messages we just sent just to confirm that Thomas' name was Thomas. I didn't see your messages at all but I could still see the text box I was typing in.

Thomas Browning (Nov 24 2020 at 00:45):

Yes, it's my fault. I redefined top to come from the Galois insertion, so that it would work nicely with the ordering.

Thomas Browning (Nov 24 2020 at 00:45):

There was a preliminary version of top in the intermediate_field.lean file, but I deleted it because it conflicted with the Galois insertion top

Patrick Lutz (Nov 24 2020 at 00:48):

Thomas Browning said:

Yes, it's my fault. I redefined top to come from the Galois insertion, so that it would work nicely with the ordering.

I think it's fine

Kevin Buzzard (Nov 24 2020 at 01:04):

I also think it's fine. The correct way to do stuff is via the API. I was being cocky thinking trivial would do it. There are various tricks you can do with sets because sets are just logic in disguise but the moment you move away from them, even to finsets, you shouldn't expect the same tricks to work (and they often don't)

Johan Commelin (Nov 27 2020 at 08:13):

Congratulations!!! You did it!

Johan Commelin (Nov 27 2020 at 08:13):

I hope the reviewing process wasn't too much of a pain.

Johan Commelin (Nov 27 2020 at 08:14):

But you can be proud of the end result!

Thomas Browning (Nov 27 2020 at 08:14):

It's great to have this PRed. Thanks so much to you and @Anne Baanen for the help!

Kevin Buzzard (Nov 27 2020 at 08:15):

Yes this is a great step forward

Johan Commelin (Nov 27 2020 at 08:15):

Are you going to talk about this at LT2021?

Kevin Buzzard (Nov 27 2020 at 08:15):

It's been something I've been wanting to see in mathlib for years

Kevin Buzzard (Nov 27 2020 at 08:15):

Not least because I was teaching it when I got into lean :-)

Johan Commelin (Nov 27 2020 at 08:16):

It's been something I've been wanting to see in mathlib for years

@Kevin Buzzard As in, since you first touched lean (-;

Thomas Browning (Nov 27 2020 at 08:16):

Johan Commelin said:

Are you going to talk about this at LT2021?

It's on our radar, and we'll discuss it at the next meeting.

Kevin Buzzard (Nov 27 2020 at 08:58):

My understanding of the vision of the organisers is that this stuff would be perfect for a LT2021 talk. They're not looking for big one hour talks on huge developments, they're looking for an overview of what's happening in the Lean ecosystem right now by the people who are making it happen, and even work in progress talks are fine. I think they're hoping to see 20 minute talks on cool new developments.

Jordan Brown (Nov 29 2020 at 01:50):

When I try to state the lemma about the nth commutator of H being the same of the nth commutator of H as a subgroup of G, Lean keeps telling me there is a type error

Jordan Brown (Nov 29 2020 at 01:50):

I tried to state the result as

lemma lift_nth_commutator_eq_nth_commutator_lift (G:Type u)[group G](H : subgroup G) (n:) :
  (nth_commutator (:subgroup H) n).lift = general_nth_commutator G H n

Jordan Brown (Nov 29 2020 at 01:52):

but VS Code keeps saying "unexpected argument at application
general_nth_commutator G
given argument
G
expected argument
↥H"
and
"type mismatch at application
general_nth_commutator G H
term
H
has type
subgroup G
but is expected to have type
subgroup ↥H"

Jordan Brown (Nov 29 2020 at 01:53):

and

general_nth_commutator : Π (G : Type u) [_inst_1 : group G], subgroup G    subgroup G

Jordan Brown (Nov 29 2020 at 01:53):

so I'm not quite sure what the issue is @Patrick Lutz @Thomas Browning

Patrick Lutz (Nov 29 2020 at 02:02):

Shouldn't it be

lemma lift_nth_commutator_eq_nth_commutator_lift (G : Type*) [group G] (H : subgroup G) (n : \N) :
   (nth_commutator H n).lift = general_nth_commutator G H n := sorry

Patrick Lutz (Nov 29 2020 at 02:02):

Like why are you using the top subgroup of H rather than just H itself (considered as a group)

Patrick Lutz (Nov 29 2020 at 02:03):

also btw G and H are probably already declared in the file and you don't need to declare them again

Patrick Lutz (Nov 29 2020 at 02:04):

Patrick Lutz said:

Like why are you using the top subgroup of H rather than just H itself (considered as a group)

So the problem is that nth_commutator (\top : subgroup H) n gives you a subgroup of (\top : subgroup H) and then lift lifts it to a subgroup of H

Patrick Lutz (Nov 29 2020 at 02:05):

but then Lean expects the other side to be a subgroup of H as well, which it's not

Patrick Lutz (Nov 29 2020 at 02:05):

instead you should just use nth_commutator H n which will give you a subgroup of H which lift will then lift to a subgroup of G

Patrick Lutz (Nov 29 2020 at 02:16):

also why does the name have two lifts in it when there is only one lift in the statement? Maybe it should be something like

nth_commutator_lift_eq_general_nth_commutator

Jordan Brown (Nov 29 2020 at 20:16):

Yeah, I declared them explicitly just in case that had something to do with the error, but it doesn't make a difference

Jordan Brown (Nov 29 2020 at 20:16):

but yes, the restatement fixes the problem; I don't know why I forgot how the arguments to nth_commutator work

Jordan Brown (Nov 29 2020 at 20:18):

at any rate, could someone remind me of the file where the lift is defined? the proof of this lemma is complete except for showing that the lift of the top subgroup of H is H, and I presume the result stating this is proven in that file

Patrick Lutz (Nov 29 2020 at 20:28):

Jordan Brown said:

at any rate, could someone remind me of the file where the lift is defined? the proof of this lemma is complete except for showing that the lift of the top subgroup of H is H, and I presume the result stating this is proven in that file

It's here. I didn't prove that (\top : subgroup H).lift = H but it shouldn't be too hard to do using mem_top.

Patrick Lutz (Nov 29 2020 at 20:29):

It also might be helpful to prove that if (K : subgroup H) then K.lift \leq H

Patrick Lutz (Nov 29 2020 at 20:29):

which I didn't do either

Patrick Lutz (Nov 29 2020 at 20:30):

the proofs should be somewhat similar to mem_lift or eq_bot_iff_lift_eq_bot

Patrick Lutz (Nov 29 2020 at 20:30):

You won't find this lift stuff in the mathlib documentation btw because it's not in mathlib; it's just something I defined

Kevin Buzzard (Nov 29 2020 at 22:00):

Hey, are you guys going to (a) write up your proof of the Galois correspondence for the special issue of Exp Math and (b) offer to talk at LT2021?

Thomas Browning (Nov 29 2020 at 22:05):

(b) Yes, we're planning on it. (a) We haven't discussed it. I would be open to doing it, but we'd really need to get a move on.

Kevin Buzzard (Nov 29 2020 at 23:38):

I am fully intending on writing up the formalisation of schemes and I haven't started yet either

Patrick Lutz (Dec 05 2020 at 04:59):

@Thomas Browning Does mathlib know about the compositum of two intermediate_fields?

Patrick Lutz (Dec 05 2020 at 04:59):

I think probably not

Thomas Browning (Dec 05 2020 at 05:24):

I think it must, because of the lattice stuff proved in adjoin.lean

Patrick Lutz (Dec 05 2020 at 05:26):

Thomas Browning said:

I think it must, because of the lattice stuff proved in adjoin.lean

ohh, you must be right

Patrick Lutz (Dec 05 2020 at 05:27):

so the compositum of L and K is probably adjoin F (K \cup L)?

Patrick Lutz (Dec 05 2020 at 05:27):

if you unroll the definitions?

Patrick Lutz (Dec 05 2020 at 05:28):

@Jordan Brown https://github.com/leanprover-community/mathlib/commit/b26d7940d757038d9e61db257f017e0a952a8bcb

Thomas Browning (Dec 05 2020 at 05:33):

I guess so, but it's also probably got specific notation (join or meet?)

Patrick Lutz (Dec 05 2020 at 05:38):

Thomas Browning said:

I guess so, but it's also probably got specific notation (join or meet?)

Yeah I agree. I just think it's a little funny

Kevin Buzzard (Dec 05 2020 at 10:14):

I thought the lattice notation was funny for ideals! But then I got used to it. Now I'm of the opinion it should be used everywhere, eg for subsets of a set :-)

Kevin Buzzard (Dec 05 2020 at 10:16):

The fact that adjoin S \lub adjoin T = adjoin (S union T) might not be true by definition, it depends on how it was all set up, but it shouldn't be hard to prove, it will be a few lines of lemmas about Galois insertions

Patrick Lutz (Dec 06 2020 at 09:03):

I thought it might be a good idea to write down somewhere what still needs to be done to prove the abel-ruffini theorem. Maybe the list of steps is basically obvious or maybe I'm leaving out something or there's a better way to do parts of it. But here goes. In all the steps below, I will assume that E is a field extension of a field F and primarily talk about intermediate_fields of E/F.

  1. If L and K are intermediate_field F Es which are galois over F then the compositum sup K L is also galois over F and the galois group embeds into the product of the galois groups of K/F and L/F
  2. If F \le L \le K is a tower of intermediate_field F Es where L is galois over F and K is galois over L then K is galois over F and the galois groups form a short exact sequence with the galois group of K over F in the middle
  3. If L is an intermediate_field F E and K is obtained from L by adding all nth roots of unity (assuming X^n - 1 splits in E and that E is of characteristic 0 or something) then K is galois over L and the galois group is abelian
    1. I think we may have to do a little work to be able to talk about K as a field extension over L. I don't think we currently have an algebra L instance for K but I could be wrong
    2. Also I'm not sure the best way we have currently to say K is obtained from L by adjoining all nth roots of unity. We could use sup of L and the F adjoin the roots of unity, but I'm not sure if that's the best approach.
    3. I don't know the right way in mathlib to say that a group is abelian. I know about comm_group but what if I just have a group and I want a Prop saying it's abelian?
  4. If L is an intermediate_field F E which contains all nth roots of unity and K is obtained from L by adjoining all roots of X^n - a (where a is in L) then K is galois over L and the galois group is abelian (with the same assumptions as in the previous step)
  5. If F \le L \le K are all galois over F then the galois group of K over F contains the galois group of L over F as a subgroup
  6. The product of solvable groups is solvable, if a group embeds into a solvable group it's solvable and that the middle term in a short exact sequence is solvable if the other two are (some of these things follow easily from other stuff we have done or from each other). The statement that abelian groups are solvable may have to be modified.
  7. S5S_5 is not solvable
  8. Define the inductive type solvable_by_radicals a for a in E. A term tof this type is a recipe for constructing a using arithmetic and radicals and elements of F
  9. For a term t of solvable_by_radicals a define a corresponding intermediate_field F E. I will refer to it as FtF^t below. It can be defined inductively. If t comes from addition it is the compositum and so on (for radical steps, first adjoin appropriate roots of unity then appropriate radicals)
  10. Show by induction that FtF^t is galois over F, has solvable galois group and contains a
  11. There is an irreducible polynomial (over Q\mathbb{Q} maybe) whose galois group is S5S_5
  12. Let aa be a root of this polynomial in C\mathbb{C}. Suppose solvable_by_radicals a is nonempty. Let t be a term. Then FtF^t contains a and is galois over F hence contains the splitting field of the minimal polynomial of a. The galois group of FtF^t is solvable and contains the galois group of the polynomial as a subgroup hence that group (S5S_5) is also solvable.
  13. Contradiction.

Patrick Lutz (Dec 06 2020 at 09:05):

All the parts look doable at this point, though steps 7 and 11 look annoying

Johan Commelin (Dec 06 2020 at 09:07):

@Patrick Lutz I think you can turn this into a github issue/project. That will be a lot easier to find back again than this post in a mile-long thread.

Johan Commelin (Dec 06 2020 at 09:07):

Pro tip: If you format the points using - [ ] then github automatically turns them into checkboxes

Patrick Lutz (Dec 06 2020 at 09:38):

https://github.com/leanprover-community/mathlib/issues/5258

Patrick Lutz (Dec 06 2020 at 19:05):

@Thomas Browning I replied to your comment on github but I don't know if it's easier to discuss it here or there. I hadn't thought about whether each step was true somehow but you're right that 2 is not true. But it seems like a problem for our approach. We would like to show by induction on the term t of solvable_by_radicals a that FtF^t is galois over F. But is that even true? I actually no longer think so. But maybe it's not necessary?

Patrick Lutz (Dec 06 2020 at 19:07):

But I think we do want FtF^t to be galois so that if it contains one root of the minimal polynomial of a then it contains all of them.

Patrick Lutz (Dec 06 2020 at 19:21):

I guess maybe we should modify the definition of FtF^t to make sure it is Galois?

Patrick Lutz (Dec 06 2020 at 19:25):

we never defined Galois closure right?

Thomas Browning (Dec 06 2020 at 19:31):

We could prove inductively on t that F^t is Galois over F

Thomas Browning (Dec 06 2020 at 19:32):

In the induction step, you know that the field is the splitting field of some polynomial p(x), and then the new field is the splitting field of p(x)*(x^n-a)

Patrick Lutz (Dec 06 2020 at 19:33):

Thomas Browning said:

In the induction step, the polynomial that you're a splitting field of gets multiplied by (x^n-a)

This is a different definition of FtF^t right? Edit: no, actually see the next comment

Patrick Lutz (Dec 06 2020 at 19:34):

Thomas Browning said:

In the induction step, you know that the field is the splitting field of some polynomial p(x), and then the new field is the splitting field of p(x)*(x^n-a)

wait, actually what does this mean? Because a might not be in F

Patrick Lutz (Dec 06 2020 at 19:34):

that's the whole problem right?

Thomas Browning (Dec 06 2020 at 19:34):

ah, good point

Thomas Browning (Dec 06 2020 at 19:35):

let me look up the proof in D&F

Patrick Lutz (Dec 06 2020 at 19:35):

Thomas Browning said:

let me look up the proof in D&F

it shows the galois closure of a sequence of radical extensions is also a sequence of radical extensions

Thomas Browning (Dec 06 2020 at 19:36):

yeah, looks like it

Thomas Browning (Dec 06 2020 at 19:37):

we might be able to avoid Galois closure though

Thomas Browning (Dec 06 2020 at 19:37):

rather than just adjoining the nth roots of a, can you just also adjoin the nth roots of any conjugate of a?

Patrick Lutz (Dec 06 2020 at 19:38):

Patrick Lutz said:

that's the whole problem right?

Actually an example I found on math SE is helpful: Q(2)\mathbb{Q}(\sqrt{2}) is galois over Q\mathbb{Q} and Q(1+2)\mathbb{Q}(\sqrt{1 + \sqrt{2}}) is galois over Q(2)\mathbb{Q}(\sqrt{2}) but not over Q\mathbb{Q}. And it is exactly the field that would be constructed as FtF^t

Patrick Lutz (Dec 06 2020 at 19:38):

Thomas Browning said:

rather than just adjoining the nth roots of a, can you just also adjoin the nth roots of any conjugate of a?

yeah I think that's what you have to do probably

Thomas Browning (Dec 06 2020 at 19:39):

but this avoids talking about Galois closure, just look at the orbit of a under the Galois group that we already have

Patrick Lutz (Dec 06 2020 at 19:41):

Thomas Browning said:

but this avoids talking about Galois closure, just look at the orbit of a under the Galois group that we already have

you mean the galois group of E over F right?

Thomas Browning (Dec 06 2020 at 19:43):

ah, yes

Thomas Browning (Dec 06 2020 at 19:43):

I guess we would have to use an ambient Galois extension

Patrick Lutz (Dec 06 2020 at 19:43):

Thomas Browning said:

rather than just adjoining the nth roots of a, can you just also adjoin the nth roots of any conjugate of a?

it's more annoying to show that this is a solvable extension though I guess? Though we can say it's the compositum of a bunch of radical extensions so maybe it's not too bad. Do we know that if F \le L \le E and L is galois over F then L is closed under conjugates by the galois group of E over F?

Thomas Browning (Dec 06 2020 at 19:44):

we don't, but it might follow from the (L/F Galois iff subgroup is normal)

Thomas Browning (Dec 06 2020 at 19:44):

which we'll prove at some point

Patrick Lutz (Dec 06 2020 at 19:45):

Thomas Browning said:

I guess we would have to use an ambient Galois extension

or algebraically closed field

Thomas Browning (Dec 06 2020 at 19:47):

but don't we need the extension E/F to be finite in order to use our Galois theory?

Patrick Lutz (Dec 06 2020 at 19:48):

hmm, well maybe not?

Patrick Lutz (Dec 06 2020 at 19:48):

it would be nice to be able to eventually state things for C\mathbb{C} over Q\mathbb{Q}

Thomas Browning (Dec 06 2020 at 19:48):

also, I'm wondering whether it might be easier to mostly work on the subgroup side

Thomas Browning (Dec 06 2020 at 19:49):

because then compositum is just intersection

Patrick Lutz (Dec 06 2020 at 19:49):

but I guess I would need to write down the steps more carefully to know which theorems we need to use and to see whether they are ones that have only been proved with the finite dimensional assumption

Thomas Browning (Dec 06 2020 at 19:49):

this business about "adjoining all of the Galois conjugates" is just taking the intersections of the conjugates of a subgroup

Patrick Lutz (Dec 06 2020 at 19:49):

Thomas Browning said:

also, I'm wondering whether it might be easier to mostly work on the subgroup side

not 100% sure what you mean. What is the difference from the sequence of steps I wrote down?

Patrick Lutz (Dec 06 2020 at 19:50):

Like we still need to know that we are getting a galois extension

Thomas Browning (Dec 06 2020 at 19:54):

Actually, I think working with fields is fine

Thomas Browning (Dec 06 2020 at 19:55):

Can we work inside of the splitting field of p(x)*(x^(big)-1) ?

Thomas Browning (Dec 06 2020 at 19:56):

Then we can use the Galois correspondence.

Thomas Browning (Dec 06 2020 at 19:58):

Actually, would it make sense to show that Gal(splitting(p(x) * (x^(big) - 1) / Q) is solvable?

Patrick Lutz (Dec 06 2020 at 19:58):

Thomas Browning said:

Can we work inside of the splitting field of p(x)*(x^(big)-1) ?

yeah I guess so? I mean it depends on what you want to prove. It's arguably not obvious that every solution by radicals would live inside that field

Patrick Lutz (Dec 06 2020 at 19:59):

I also just think it would be nice to be able to say stuff about C/Q\mathbb{C}/\mathbb{Q}

Thomas Browning (Dec 06 2020 at 20:00):

That's true

Patrick Lutz (Dec 06 2020 at 20:01):

but I think we should try to carefully write down what we need to prove and see how much of it depends on the finite dimensional assumption

Thomas Browning (Dec 06 2020 at 20:01):

If we ever need a finite Galois closure, we could use PET + splitting field of that polynomial

Patrick Lutz (Dec 06 2020 at 20:01):

because a lot of times we are just dealing with Ft/FF^t/F which is finite dimensional. There's only a few places we need to talk about the ambient field

Thomas Browning (Dec 06 2020 at 20:05):

Here's something that we could prove: If F < E < K are finite extensions such that E/F and K/E are both Galois and solvable, then there is a solvable Galois extension M/F containing E/F

Thomas Browning (Dec 06 2020 at 20:05):

is that true?

Patrick Lutz (Dec 06 2020 at 20:11):

wait, do you mean containing K/F?

Patrick Lutz (Dec 06 2020 at 20:12):

if so, I think it's true because you can take the galois closure of K and view it as a compositum of a bunch of copies of the chain F < E < Keach of which is solvable. But I'm not 100% sure

Thomas Browning (Dec 06 2020 at 20:15):

Yes, I meant K/F

Thomas Browning (Dec 06 2020 at 20:21):

To take a compositum, do we need to be working inside an ambient field?

Thomas Browning (Dec 06 2020 at 20:21):

I would assume so

Kevin Buzzard (Dec 06 2020 at 20:34):

When I lectured this I defined algebraic closures early on and would always work in the alg closure of the base field

Kevin Buzzard (Dec 06 2020 at 20:34):

It just made things much easier

Kevin Buzzard (Dec 06 2020 at 20:34):

I'm not sure if it makes formalisation easier though

Kevin Buzzard (Dec 06 2020 at 20:35):

The other approach is to define normal closure of a finite extension

Kevin Buzzard (Dec 06 2020 at 20:36):

I defined it as "take generators of the extension and then look at the splitting field of the product of the min polys"

Kevin Buzzard (Dec 06 2020 at 20:36):

Has this sort of stuff been done in any other prover? Is this one of the "never done before in any prover" Freek 100 questions?

Kevin Buzzard (Dec 06 2020 at 20:38):

If it's not been done in any other prover one will have to think about the best way to do it. I've lectured this stuff and I totally agree it's annoying. One year I just adjoined a ton of roots of unity to the base to deal with issues

Kevin Buzzard (Dec 06 2020 at 20:38):

There's a notion of "solvable" for a finite separable extension, which is "Galois closure is solvable"

Patrick Lutz (Dec 06 2020 at 20:41):

Kevin Buzzard said:

Has this sort of stuff been done in any other prover? Is this one of the "never done before in any prover" Freek 100 questions?

yes

Patrick Lutz (Dec 06 2020 at 20:42):

Thomas Browning said:

To take a compositum, do we need to be working inside an ambient field?

yes but I was assuming we are

Thomas Browning (Dec 06 2020 at 20:44):

Kevin Buzzard said:

There's a notion of "solvable" for a finite separable extension, which is "Galois closure is solvable"

That could be a useful concept for us

Kevin Buzzard (Dec 06 2020 at 20:45):

Working in a big ambient extension, especially one that contains all the n'th roots of unity for all n showing up in the argument, might be a really cool idea

Kevin Buzzard (Dec 06 2020 at 20:46):

I should say that I made up the notion of solvable in that generality but IIRC I checked it had good properties eg composite of solvable is solvable

Kevin Buzzard (Dec 06 2020 at 20:46):

Adjoining n'th root is solvable

Kevin Buzzard (Dec 06 2020 at 20:49):

It's not true that solvable implies "can be obtained by iterating adjoining n'th roots" but it is true that solvable implies is a subfield of a finite extension obtained by adjoining n'th roots several times

Kevin Buzzard (Dec 06 2020 at 20:50):

All this is from memory from when I was teaching this stuff a few years ago so might be wrong. But I was really annoyed when I discovered that this stuff seemed much less clean than I had expected

Kevin Buzzard (Dec 06 2020 at 20:51):

The key theorem is that if L/K is cyclic degree n and if K contains all the n'th roots of unity then L is obtained from K by throwing in an n'th root. This is proved in birch's article in Cassels-Froehlich

Kevin Buzzard (Dec 06 2020 at 20:52):

I don't know if you need to go that far though. The proof isn't hard

Patrick Lutz (Dec 06 2020 at 21:06):

Kevin Buzzard said:

Working in a big ambient extension, especially one that contains all the n'th roots of unity for all n showing up in the argument, might be a really cool idea

I think the roots of unity are actually not going to be a big issue. It's more showing that things are galois

Patrick Lutz (Dec 06 2020 at 21:07):

Kevin Buzzard said:

I should say that I made up the notion of solvable in that generality but IIRC I checked it had good properties eg composite of solvable is solvable

that's probably the fact that would be useful

Kevin Buzzard (Dec 06 2020 at 22:15):

If A in B in C in D and D/A is solvable then C/B is solvable. IIRC I sort of made the proofs up myself, perhaps because I was in a place with no internet when I realised that what I thought was going to be an easy two lectures to prepare was in fact going to be trickier than i thought!

Thomas Browning (Dec 07 2020 at 19:17):

@Patrick Lutz Would it be possible to move the meeting today to 2pm? The RTG seminar seminar today is by my algebra TA from 4 years ago, and I am interested in going.

Patrick Lutz (Dec 07 2020 at 19:59):

sure

Patrick Lutz (Dec 08 2020 at 07:07):

@Thomas Browning just an fyi, I'm speaking at JMM on January 7th, which might conflict with Lean Together 2021

Thomas Browning (Dec 08 2020 at 07:49):

thanks for the heads up

Patrick Lutz (Dec 08 2020 at 22:41):

Okay, I have a new idea for the abel-ruffini strategy

Patrick Lutz (Dec 08 2020 at 22:49):

  1. Define solvable_by_radicals a as before
  2. Show by induction that if solvable_by_radicals a is inhabited then a is algebraic over F
  3. Show by induction that if solvable_by_radicals a is inhabited then the splitting field of the minimal polynomial of a is a solvable extension of F
    1. There are two parts to doing this. First, for cases like a = b + c, show that the splitting field for a embeds into the compositum of the splitting fields for b and c and then this implies that the galois group for a embeds into the product of the galois groups for b and c
    2. Second, for the case where a^n = b, note that if p is the minimal polynomial for b then the minimal polynomial for a divides p(X^n). So the splitting field for a embeds into the field that you get from first adjoining nth roots of unity and then adjoining roots of p(X^n). So it's enough to show that the galois group of p(X^n) over a field that contains the nth roots of unity embeds into the product of the galois group of p and the galois group of X^n - c where c is any arbitrary root of p (and show that we get the same group no matter which c is used)
    3. It sounds easier to do all of this by working with intermediate_fields of some big ambient field (maybe algebraically closed) but I'm not sure
  4. Now we are done as soon as we construct an element of the big field whose minimal polynomial has non-solvable galois group

Patrick Lutz (Dec 08 2020 at 22:50):

I don't know how well this will work, but I think it might be reasonable. Hopefully it doesn't contain any false statements. Basically I'm trying to get around having to work with the galois closure by just using the splitting field of p(X^n)

Thomas Browning (Dec 08 2020 at 23:06):

Ooh, I really like this approach of using the splitting field of the minimal polynomial of the solvable_by_radicals element

Patrick Lutz (Dec 08 2020 at 23:08):

yeah, the hairy part will basically all be in part 2.2 I think

Patrick Lutz (Dec 08 2020 at 23:17):

Actually 2.2 may be a little more annoying than I made it sound. The problem is that adjoining roots of unity may mean that p is no longer irreducible

Patrick Lutz (Dec 08 2020 at 23:17):

so it's not true that the galois group of X^n - c will always be the same for all roots c of p

Patrick Lutz (Dec 08 2020 at 23:18):

I think this strategy can still work but I'm not sure the exact statement we want to prove about p(X^n)

Patrick Lutz (Dec 08 2020 at 23:19):

I mean the good news I guess is that either c already has an nth root, in which case X^n - c just splits or it doesn't, in which case the galois group of X^n - c is Z/nZ\mathbb{Z}/n\mathbb{Z}

Patrick Lutz (Dec 08 2020 at 23:21):

so I guess we can maybe show that the galois group embeds into the galois group of p over F times Z/nZ\mathbb{Z}/n\mathbb{Z}

Patrick Lutz (Dec 08 2020 at 23:22):

also it's nice that first adjoining roots of unity, then roots of p(X^n) is a splitting field for (X^n - 1)p(X^n) so it's automatically galois over F

Patrick Lutz (Dec 08 2020 at 23:28):

wait, now I'm starting to doubt some of the stuff I'm saying

Patrick Lutz (Dec 08 2020 at 23:31):

I think the galois group of p(Xn)p(X^n) may be a little complicated to describe

Thomas Browning (Dec 08 2020 at 23:35):

well, it should still be true that p(X^n) has solvable Galois group, right?

Patrick Lutz (Dec 08 2020 at 23:35):

Thomas Browning said:

well, it should still be true that p(X^n) has solvable Galois group, right?

yes, but I'm trying to figure out the easiest way to prove that

Patrick Lutz (Dec 08 2020 at 23:35):

but I have a new idea

Patrick Lutz (Dec 08 2020 at 23:36):

wait, no I don't

Patrick Lutz (Dec 08 2020 at 23:37):

I'm having trouble finding anything describing the galois group of a composition of polynomials

Patrick Lutz (Dec 08 2020 at 23:38):

but it's maybe a wreath product

Patrick Lutz (Dec 08 2020 at 23:38):

well, maybe we can express this using short exact sequences instead

Thomas Browning (Dec 08 2020 at 23:39):

You need to show that Gal(split(p(X^n))/split(p(X))) is solvable

Patrick Lutz (Dec 08 2020 at 23:39):

Thomas Browning said:

You need to show that Gal(split(p(X^n))/split(p(X))) is solvable

yeah, that's true

Patrick Lutz (Dec 08 2020 at 23:40):

which should somehow follow from adding roots of unity and then adding roots one at a time

Patrick Lutz (Dec 08 2020 at 23:40):

I guess

Patrick Lutz (Dec 08 2020 at 23:40):

maybe just an ugly induction

Patrick Lutz (Dec 09 2020 at 03:36):

Okay, I think I now understand better what's going on. The key is that if F=K0K1Kn=EF = K_0 \le K_1 \ldots \le K_n = E is a sequence of field extensions such that EE is Galois over FF and each Ki+1K_{i + 1} is Galois over KiK_i with solvable Galois group then the Galois group of EE over FF is solvable. The tricky thing is that you prove this by backwards induction on ii. I.e. prove by induction on jj that the Galois group of EE over KnjK_{n - j} is solvable (using the fact about short exact sequences of solvable groups). In our case, we can first show that the splitting field of p(Xn)(Xn1)p(X^n)(X^n - 1) is contained in the field you get by starting with FF, going to the splitting field of pp, adjoining roots of unity and then adjoining roots of equations of the form XnbX^n - b. Each of these extensions is Galois over the previous one with solvable Galois group so the whole thing is solvable. The intermediate fields are not Galois over F,F, but that doesn't matter.

Kevin Buzzard (Dec 09 2020 at 09:24):

If you define this generalised solvable to mean "Galois closure is solvable" then this follows from transitivity of generalised solvable

Patrick Lutz (Dec 09 2020 at 21:06):

Kevin Buzzard said:

If you define this generalised solvable to mean "Galois closure is solvable" then this follows from transitivity of generalised solvable

But how do you prove transitivity of "Galois closure is solvable"? Wouldn't it be similar to what I said above?

Patrick Lutz (Dec 09 2020 at 21:09):

Btw I realized that since we have the primitive element theorem it's actually pretty easy to define the galois closure of a separable extension. You can just define it as the splitting field of the minimal polynomial of the primitive element

Kevin Buzzard (Dec 09 2020 at 21:29):

How about L/K is presolvable if there exists E/L Galois over K with solvable Galois group?

Patrick Lutz (Dec 09 2020 at 22:34):

I guess I sort of do like the approach of defining "solvable" for a separable extension to mean either "galois closure is solvable" or the definition you just suggested. The only problem is that proving transitivity looks kind of messy (even messier than the way that it's used directly in the proof). To make things easy, suppose FLKEF \le L \le K \le E where EE is algebraically closed or something and L/FL/F and K/LK/L are both Galois. How easy is it to show that there is a galois extension of FF that contains LL and which is solvable?

Kenny Lau (Dec 09 2020 at 22:35):

as easy as the maths proof

Patrick Lutz (Dec 09 2020 at 22:36):

Kenny Lau said:

as easy as the maths proof

which proof?

Kenny Lau (Dec 09 2020 at 22:36):

as in, it will be equally as easy or as hard as the maths proof, if there is one.

Kenny Lau (Dec 09 2020 at 22:37):

or, phrased in another way: do you have the maths proof?

Patrick Lutz (Dec 09 2020 at 22:37):

No, but Kevin seemed convinced it's true. I started thinking about it and I don't see a really simple proof, which is why I asked

Patrick Lutz (Dec 09 2020 at 22:38):

the proof of abel-ruffini that I outlined above proves basically a special case of this where K/LK/L has a special form (adjoining a root of XnaX^n - a for some aa in KK)

Kevin Buzzard (Dec 09 2020 at 23:02):

The maths proof is that if E'/F is the Galois closure of K/F then E'/L is solvable because it's a composite of all the K'/L as K' runs over the conjugates of K, and each of those are solvable because they're isomorphic to K/L, so the Galois group of E'/F is an extension of solvable groups so solvable

Kevin Buzzard (Dec 09 2020 at 23:06):

the group-theoretic version of the argument is: if Γ\Gamma is a big ambient group, and if AA is a normal subgroup with Γ/A\Gamma/A solvable and if BB is a normal subgroup of AA with A/BA/B solvable, then conjugating by all the elements of Γ\Gamma gives you a bunch of subgroups B=gBg1B'=gBg^{-1} with A/BA/B' solvable (because isomorphic to A/BA/B), so if CC is the intersection of the BB' then A/CA/C is solvable and hence Γ/C\Gamma/C is solvable.

Thomas Browning (Dec 13 2020 at 04:14):

#5342 #5343 #5344 #5345 #5346 #5347 and then we'll have separable splitting field implies galois

Patrick Lutz (Dec 17 2020 at 00:04):

Here's a new attempt at a roadmap to the Abel-Ruffini theorem. Let me know if anything is false or if there are any other problems with it. I've also updated the list on github so that it matches this.

Facts about fields

  • If L < K are intermediate_fields of E/F then K is an L algebra
  • If K_1 < K_2 < K_3 are intermediate_fields of E/F then they form an is_scalar_tower
  • If L < K are intermediate_fields of E/F which are both galois over F then the galois group of L/F embeds into the galois group of K/F (or maybe just assume F, L, K form an is_scalar_tower?)
  • If L and K are intermediate_fields which are both galois over F then the compositum (sup K L) is also galois over F and the galois group embeds into the product of the galois groups of K/F and L/F.
  • If a = b + c and everything algebraic over F then the splitting field of the minimal polynomial of a is contained in the compositum of the splitting fields of the minimal polynomials of b and c.
  • If F, L, E form an is_scalar_tower (nothing here is an intermediate_field) and L/F, E/L and E/F are all galois then their galois groups form a short exact sequence
  • There is an irreducible polynomial p such that the splitting field of p has galois group isomorphic to S_5 (for whatever version of S_5 is proved not solvable below)
  • If p is an irreducible polynomial then the minimal polynomial of any root of p is p itself

Facts about groups

  • Product of solvable groups is solvable
  • If a group embeds into a solvable group it is solvable
  • Abelian groups are solvable
  • S_5 is not solvable (really, just prove the group of permutations on some 5 element type is not solvable)

Facts about solvability of galois groups

  • If F, L, E form an is_scalar_tower (nothing here is an intermediate_field) such that L/F and E/L are both galois and solvable and E/F is galois then E/F is solvable.
  • If L contains the nth roots of unity and K/L is obtained by adjoining an nth root of something in L then K/L is galois with solvable galois group

Abel-Ruffini theorem

  • Define solvable_by_radicals a for a in E. This is just a prop-valued inductive type, as described in this thread.
  • Show by induction that if solvable_by_radicals a then a is algebraic (or is_integral) over F
    • Base case and cases +, *, - have already been done
    • Case ^-1 should be easy
    • Case ^(1/n) should be easy (p(X^n))
  • Show by induction that if solvable_by_radicals a then the splitting field of the minimal polynomial of a over F is solvable
    • Base case is easy
    • Case ^-1 should be easy
    • Cases +, *, - correspond to compositum.
    • Case a^n = b can be done as follows: form a sequence of intermediate_fields, F = K_0 < K_1 < K_2 < ... < K_m where K_1 is the splitting field of p (min. poly. of b), K_2 is obtained by adjoining the nth roots of unity and each extension after is obtained by adjoining nth root of a root of p. Next, show that K_m is equal to the splitting field of p(X^n)(X^n - 1), hence galois. Finally, show by backwards induction on i that K_m is solvable over K_i. Finally, observe that the min. poly. of a divides p(X^n)(X^n - 1), hence its splitting field is contained in K_m, hence its galois group embeds into K_m's and hence is solvable
  • Let p be the polynomial whose galois group is S_5. If solvable_by_radicals a holds for any root of p then the splitting field of the minimal polynomial of that root is solvable. But the minimal polynomial of such a root must be p itself so S_5 is solvable. Contradiction.

Patrick Lutz (Dec 17 2020 at 01:22):

By the way, I suggest that when we complete parts of this list, we check off the appropriate box on the github issue and edit the comment (on github) to link to the place where that theorem is proved. If that seems too annoying, that's fine too

Patrick Lutz (Dec 17 2020 at 01:22):

A couple of things on the list have already been done I think

Patrick Lutz (Dec 17 2020 at 01:22):

though for some of them, we may need a slightly different version

Patrick Lutz (Dec 17 2020 at 01:23):

Also, maybe obvious, but the different items on the list are definitely not all of equal difficulty

Kevin Buzzard (Dec 17 2020 at 07:16):

Third field bullet point-- if K/L/F all Galois then Gal(L/F) doesn't embed into Gal(K/F), there's a surjection the other way around

Kevin Buzzard (Dec 17 2020 at 07:20):

Facts about solvability of Galois groups -- adding an n'th root when base field has all n'th roots of one gives you an abelian Galois group, and abelian Galois groups are solvable (seems worth mentioning)

Kevin Buzzard (Dec 17 2020 at 07:31):

Although it's not helpful, K_m is actually the splitting field of p(X^n) because this contains all the n'th roots of any root of p and hence all the n'th roots of unity

Kevin Buzzard (Dec 17 2020 at 07:31):

The one part which isn't clear to me is how this backwards induction works in the last but one bullet point

Kevin Buzzard (Dec 17 2020 at 07:50):

There's this one technical issue of how to deal with nth roots when the base field doesn't contain nth roots of unity. These K_i in your proof don't all play a symmetric role. Isn't it true that if a : E and SBR a F then SBR a K for K any extension of F. Furthermore if spl(a/K) is solvable over K and K/F is solvable then spl(a/F) is solvable over F because of the short exact sequence property. This reduces the question of nth roots to the case where the nth roots of 1 are in the base field and then you're reduced to the question of showing that if an extension is a subextension of a composite of abelian extensions then it's Galois which is easy. I think I'm still doing the backwards induction which you envisage but because the definition of the K_i isn't homogeneous (K1, K2 and the higher Ki are all defined in different ways) I'm just trying to split off the arguments so that they all occur in different proofs rather than in one nightmare proof

Kevin Buzzard (Dec 17 2020 at 11:33):

It seems that the heart of "solvable_by_radicals a F -> spl(a/F) / F solvable" is "spl (a^n/F) /F solvable -> (spl a/F) / F solvable" and perhaps it would be good to break this down into pieces more in the plan. Rather than doing splitting fields of elements one can work with splitting fields of polynomials, which reduces it to "(spl p(X)/F)/F solvable -> (spl (p(X^n))/F)/F solvable". I guess if p in F[X] and K/F is solvable then spl(p/F)/F is solvable iff spl(p/K)/K is solvable. That looks like a useful lemma which should be split off. This reduces to the case where F contains all n'th roots of 1 and then you can reduce to spl(p(X^n)/F)/spl(p(X)/F) solvable under the assumption that F contains all n'th roots of 1, which follows because over spl(p(X),F) you can factor p(X^n) as (X^n-alpha)(X^n-beta)... . Then you prove that spl(p/F) solvable and spl(q/F) solvable implies spl(pq/F) solvable and then prove the analogous statement for a product of finitely many polys by induction (there finally is the induction you want to do, but in a much simpler setting) and now I think you're home.

Kevin Buzzard (Dec 17 2020 at 11:35):

Aah -- perhaps you don't even need to reduce to the case where F contains the n'th roots of 1, because you can prove spl(X^n-alpha)/F is solvable for alpha in F whether or not F contains the n'th roots of unity; the splitting field is an extension of F(mu_n) by one n'th root of alpha so it has a two step filtration by abelian groups.

Patrick Lutz (Dec 17 2020 at 17:02):

Kevin Buzzard said:

Third field bullet point-- if K/L/F all Galois then Gal(L/F) doesn't embed into Gal(K/F), there's a surjection the other way around

oops, good point. I've edited the issue on github to reflect this.

Patrick Lutz (Dec 17 2020 at 17:05):

Kevin Buzzard said:

Facts about solvability of Galois groups -- adding an n'th root when base field has all n'th roots of one gives you an abelian Galois group, and abelian Galois groups are solvable (seems worth mentioning)

I've added an extra bullet point about showing the galois group embeds into Z/nZ\mathbb{Z}/n\mathbb{Z}. There was already an entry about showing abelian groups are solvable (which I already proved but in the "wrong way"---I showed that a comm_group is solvable but not that a group which commutes is solvable)

Patrick Lutz (Dec 17 2020 at 17:07):

Kevin Buzzard said:

Although it's not helpful, K_m is actually the splitting field of p(X^n) because this contains all the n'th roots of any root of p and hence all the n'th roots of unity

That's true, but I'm not sure it's worth proving it

Patrick Lutz (Dec 17 2020 at 17:08):

Kevin Buzzard said:

The one part which isn't clear to me is how this backwards induction works in the last but one bullet point

It just uses the first bullet point under "Facts about solvability of galois groups"

Kevin Buzzard (Dec 17 2020 at 17:24):

We're talking about this, right?

form a sequence of intermediate_fields, F = K_0 < K_1 < K_2 < ... < K_m where K_1 is the splitting field of p (min. poly. of b), K_2 is obtained by adjoining the nth roots of unity and each extension after is obtained by adjoining nth root of a root of p. Next, show that K_m is equal to the splitting field of p(X^n)(X^n - 1), hence galois. Finally, show by backwards induction on i that K_m is solvable over K_i.

This is the part which I think is hard. In particular I think your "backwards induction" is very optimistic. You take the roots of p, you make them into a list, you then make these K_i for i>=3, you then have to prove K_m is solvable over K_i for all i. If you think about it you'll actually need to prove K_j is Galois and solvable over K_i for all i as well. There are cases i=0, i=1, i=2 and i>=3 giving you six sub-theorems to prove here, all in one proof, which you can't factor out because the definition of the K_i occurs after the theorem statement, in the proof. Things will get really slow, because when proofs start hitting 100 lines it starts becoming intolerable to write them. This argument needs to be taken apart. I have suggested a way of breaking this up into far smaller pieces above. Let me know if you don't understand it or want me to go through it again. I think this backwards induction is not going to fly as it stands and needs to become five smaller theorems.

Patrick Lutz (Dec 17 2020 at 18:38):

I think there may have been some kind of misunderstanding. I didn't mean to suggest that there shouldn't be separate lemmas used in doing that step or that it should be one huge monolithic proof. And I haven't had much time to think about this since I saw your comments so I am not sure if your suggested route is the best option or not.

Patrick Lutz (Dec 17 2020 at 18:39):

also I don't think you need to show KjK_j is galois and solvable over KiK_i for all ii. Just that Ki+1K_{i + 1} is galois and solvable over KiK_i. And that KmK_m is galois over each KiK_i which comes from galois_tower_top or something like that.

Patrick Lutz (Dec 17 2020 at 18:39):

but yes, I agree that lemmas are needed.

Patrick Lutz (Dec 17 2020 at 18:39):

I just wasn't sure which ones are needed yet.

Patrick Lutz (Dec 17 2020 at 18:40):

I was going to read through your other comments and respond to them later but I just responded to the ones that I could respond to quickly

Thomas Browning (Dec 25 2020 at 02:07):

@Jordan Brown FWI, we won't be meeting tomorrow

Thomas Browning (Jan 19 2021 at 18:02):

@Patrick Lutz Have you been following this thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/

Patrick Lutz (Jan 19 2021 at 18:11):

Thomas Browning said:

Patrick Lutz Have you been following this thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/

No, I hadn't seen that

Patrick Lutz (Jan 19 2021 at 18:11):

I guess I never really fully understood the significance of subsingleton in the first place

Patrick Lutz (Jan 19 2021 at 18:11):

and I don't know why this PR would break things

Thomas Browning (Jan 19 2021 at 18:12):

It seems like simp is not handling subsingleton instances correctly

Patrick Lutz (Jan 19 2021 at 18:12):

yeah, but I don't know why that would be

Patrick Lutz (Jan 19 2021 at 18:13):

I guess it's also weird because originally this lemma did not mention subsingleton and I never really saw why it was important to change it

Thomas Browning (Jan 19 2021 at 18:14):

Was this lemma for talking about the trivial group?

Patrick Lutz (Jan 19 2021 at 18:14):

like I guess the inference engine can sometimes automatically supply subsingleton instances but not top = bot instances, but I feel like most times you'd want to apply this sort of lemma that probably doesn't matter too much

Patrick Lutz (Jan 19 2021 at 18:14):

Thomas Browning said:

Was this lemma for talking about the trivial group?

it said that if top = bot in an algebra then the top subgroup of the group of algebra automorphisms equals the bottom subgroup

Thomas Browning (Jan 19 2021 at 18:14):

I'm still not sure what the best way to talk about the trivial group is

Patrick Lutz (Jan 19 2021 at 18:14):

if an algebra is trivial then its automorphism group is trivial

Thomas Browning (Jan 19 2021 at 18:15):

bot = top doesn't seem like the best way

Patrick Lutz (Jan 19 2021 at 18:15):

Thomas Browning said:

I'm still not sure what the best way to talk about the trivial group is

I guess subsingleton is a reasonable way, but it just doesn't seem that important to me

Patrick Lutz (Jan 19 2021 at 18:15):

Thomas Browning said:

bot = top doesn't seem like the best way

fair enough

Thomas Browning (Jan 19 2021 at 18:16):

Is the notion of an algebra being trivial discussed in mathlib?

Patrick Lutz (Jan 19 2021 at 18:17):

Thomas Browning said:

Is the notion of an algebra being trivial discussed in mathlib?

there are some lemmas that I added a while ago in one of the primitive element theorem PRs about algebras with dimension 1

Patrick Lutz (Jan 19 2021 at 18:17):

which is one way of saying an algebra is trivial

Patrick Lutz (Jan 19 2021 at 18:18):

I'm just now finishing reading the thread you linked though. The effect of subsingleton instances on simps behavior seems crazy to me

Thomas Browning (Jan 19 2021 at 18:18):

On the plus side, mathlib might get a major performance increased when this is fixed

Thomas Browning (Jan 29 2021 at 21:14):

@Patrick Lutz Surjectivity is coming: #5960

Thomas Browning (Jan 30 2021 at 00:34):

@Patrick Lutz I've merged the surjectivity stuff into the abel-ruffini branch, and cleaned up the compositum proof a bit

Thomas Browning (Feb 03 2021 at 01:16):

There might be a potential flaw with our discussion on Monday. We drew an arrow from (minpoly F α).splitting_field to minpoly ((minpoly F (α ^ n)).splitting_field) α. I'm a little worried that such a map might not exist. For instance, what ifα is the 4th root of 2, and n = 2?

It seems to me that there is a fundamental obstacle: A tower of normal extensions is not necessarily normal, so we will need to take a normal closure at some point. In particular, we need to know that a finite compositum of solvable extensions is solvable (or something along these lines).

I think that we should bite the bullet and prove the following theorem: If E/K/F is an tower of fields with E/K and K/F both normal and solvable then there exists an extension L/E such that L/F is normal and solvable.

This might not be true as stated, maybe you need to assume that some or all of the tower is finite-dimensional.

I'm not sure what the best way to prove this is. Here's an ugly way, assuming that everything is finite-dimensional. We know that finite-dimensional normal extensions are splitting fields. So E is the splitting field of a polynomial over K. Applying the various F-automorphisms of K give finitely many polynomials over K. Multiply them together and let L be the splitting field of this product over E. There are things left to do:
-> The product is F-invariant so L is secretly a splitting field over F (and thus normal).
-> To show that L/F is solvable, it is enough to show that L/K is solvable. This should be a reasonable induction, since we already know that if p and q have solvable Galois group then so does p*q.

Thomas Browning (Feb 03 2021 at 01:17):

@Patrick Lutz

Patrick Lutz (Feb 03 2021 at 08:20):

You may be right. Let me spend a bit more time thinking about it in the morning.

Patrick Lutz (Feb 05 2021 at 04:36):

Sorry, I meant to write a reply to this earlier. Here's one way we could try to get around all this stuff.
First, letting p denote the minimal polynomial of ana^n, we have a tower F < split(p(X)) < split(p(X)*(X^n - 1)) < split(p(X)*(X^n - 1)*p(X^n)). It should also be easy to show that the minimal polynomial of aa divides p(Xn)p(X^n) so we get that split(min(a)) embeds into the last field in the tower. Also each field is normal over the previous one. We also know that the third field is solvable over the second one by the compositum proof. So it comes down to showing that split(p(X)*(X^n - 1)*p(X^n)) is solvable over split(p(X)*(X^n - 1)). I think for that we basically need to show that it's generated as a field extension by nth roots of the roots of p and then we can separately prove that if we have the nth roots of unity then any field extension generated by nth roots of things in the base field is solvable.

Patrick Lutz (Feb 05 2021 at 04:36):

@Thomas Browning

Thomas Browning (Feb 05 2021 at 04:49):

I like this, it sidesteps a lot of the issues that I was worried about

Thomas Browning (Feb 05 2021 at 04:49):

in particular, it's nice that everything is a splitting field over F

Patrick Lutz (Feb 05 2021 at 04:49):

I kind of feel like we even discussed this approach at some point

Patrick Lutz (Feb 05 2021 at 04:50):

but I either lost the paper where I wrote it down or I didn't write it down

Thomas Browning (Feb 05 2021 at 04:50):

for some reason I was worried about showing that the minimal polynomial of a divides p(X^n), but now that I think about it, it doesn't seem bad at all

Patrick Lutz (Feb 05 2021 at 04:50):

that seems like one of the less bad parts to me

Patrick Lutz (Feb 05 2021 at 04:50):

because you can evaluate things in E

Patrick Lutz (Feb 05 2021 at 04:55):

So here's a (partial?) list of things to do

  1. Show that split(X^n - 1) is solvable
  2. Show that min(a) divides min(a^n) comp (X^n)
  3. Show that split(p(X)*(X^n - 1)*p(X^n)) is generated over split(p(X)*(X^n - 1)) by the nth roots of the roots of p(X). One way to do this would be to note that it's generated by the roots of p(X), X^n - 1 and p(X^n) and the first two sets are already in the field split(p(X)*(X^n - 1)) and the latter roots are all nth roots of roots of p(X)
  4. Show that if a field is normal and generated by nth roots of things in the base field then its automorphism group is solvable

Patrick Lutz (Feb 05 2021 at 04:55):

Actually, here's a better way of stating (3)

Patrick Lutz (Feb 05 2021 at 04:56):

Show that if we have a field extension F/E and E is generated over F by the roots of p(X^n) and p and X^n - 1 both split in F then E is generated by nth roots of things in F

Patrick Lutz (Feb 05 2021 at 04:59):

Of course we still also need to show that if E/K/F is a normal tower and E/K and K/F are both solvable then so is E/F

Thomas Browning (Feb 05 2021 at 05:00):

That last one shouldn't be bad at all

Patrick Lutz (Feb 05 2021 at 05:00):

yeah

Patrick Lutz (Feb 05 2021 at 05:00):

(4) looks a bit tricky

Thomas Browning (Feb 05 2021 at 05:00):

By the way, are we treating is_solvable as an instance or a ordinary hypothesis?

Patrick Lutz (Feb 05 2021 at 05:00):

it's a type class

Patrick Lutz (Feb 05 2021 at 05:01):

so it should be an instance by default but sometimes it can't be I guess

Patrick Lutz (Feb 05 2021 at 05:01):

Patrick Lutz said:

(4) looks a bit tricky

I somehow thought we had discussed a way to prove this using induction_on_finset but now I don't see how

Thomas Browning (Feb 05 2021 at 05:01):

so should solvable_prod be an instance?

Patrick Lutz (Feb 05 2021 at 05:01):

Thomas Browning said:

so should solvable_prod be an instance?

yeah, is it not?

Thomas Browning (Feb 05 2021 at 05:02):

lemma solvable_prod {G' : Type*} [group G'] (h : is_solvable G) (h' : is_solvable G') :
  is_solvable (G × G') :=

Patrick Lutz (Feb 05 2021 at 05:02):

is_solvable was only changed to a type class when it got merged into mathlib so I probably forgot to change some things over

Patrick Lutz (Feb 05 2021 at 05:02):

but yeah it should be I think

Patrick Lutz (Feb 05 2021 at 05:11):

Patrick Lutz said:

Patrick Lutz said:

(4) looks a bit tricky

I somehow thought we had discussed a way to prove this using induction_on_finset but now I don't see how

Okay, I see a funny way to do this but I'm not sure it's a great idea. You could do a proof by contradiction and show by induction on the set of generators of the field extension that E/F(a1,...,ak) is not solvable but that would show E/top is not solvable which is absurd

Thomas Browning (Feb 05 2021 at 07:05):

Patrick Lutz said:

Of course we still also need to show that if E/K/F is a normal tower and E/K and K/F are both solvable then so is E/F

Done (in normal.lean)

Thomas Browning (Feb 08 2021 at 23:03):

@Patrick Lutz Does this look true to you?
example : p.splits (algebra_map F (p.comp q).splitting_field) :=

Thomas Browning (Feb 08 2021 at 23:04):

(the idea is that applying q to the roots of p.comp q gives you roots of p)

Thomas Browning (Feb 08 2021 at 23:05):

If it is true, it would be a nice lemma for polynomial_galois_group.lean, and it would construct the inclusion from the splitting field of p(x) to the splitting field of p(x^n)

Patrick Lutz (Feb 09 2021 at 00:55):

I'm pretty sure that's true. I think it's easy to see if you work in the algebraic closure (not necessarily the easiest Lean proof though of course). Then if a is a root of p, let b be a root of q - a and then q(b) gives you a so a is in the splitting field of p.comp q

Patrick Lutz (Feb 09 2021 at 00:56):

but we don't actually need to construct a map from p.splitting_field to (p.comp (X^n)).splitting_field

Patrick Lutz (Feb 09 2021 at 00:56):

because we can just use p(X)*(X^n - 1)*p(X^n)'s splitting field, i.e. show that it is solvable and that p.splitting_field embeds into it

Patrick Lutz (Feb 09 2021 at 00:57):

Patrick Lutz said:

I'm pretty sure that's true. I think it's easy to see if you work in the algebraic closure (not necessarily the easiest Lean proof though of course). Then if a is a root of p, let b be a root of q - a and then q(b) gives you a so a is in the splitting field of p.comp q

wait this didn't make sense

Patrick Lutz (Feb 09 2021 at 00:57):

oh, wait, no it does

Patrick Lutz (Feb 09 2021 at 00:58):

because b is a root of p.comp q

Thomas Browning (Feb 09 2021 at 01:01):

I guess it isn't necessary, although it feels a bit weird to take the splitting field of that product when some of the terms already split

Patrick Lutz (Feb 09 2021 at 02:14):

I guess it is a nice thing to prove. But the proof I gave might be a bit annoying in Lean

Patrick Lutz (Feb 09 2021 at 02:14):

although maybe actually not so bad

Kevin Buzzard (Feb 09 2021 at 07:18):

If q is constant this isn't true. You need some statement saying that every root of p shows up as a value of q

Patrick Lutz (Feb 09 2021 at 18:02):

Kevin Buzzard said:

If q is constant this isn't true. You need some statement saying that every root of p shows up as a value of q

Yeah, the proof I gave above doesn't work if q is constant because q - a is constant and has no roots. But the proof I gave above works whenever q is not constant (and does implicitly show that every root of p shows up as a value of q in the algebraic closure)

Thomas Browning (Feb 10 2021 at 00:51):

@Patrick Lutz I proved it:
example (hq : q.nat_degree ≠ 0) : p.splits (algebra_map F (p.comp q).splitting_field) :=

Thomas Browning (Feb 10 2021 at 07:51):

@Patrick Lutz I've made the reduction to:

lemma gal_X_pow_sub_C_is_solvable {n : } (hn : n  0) (x : F) : is_solvable (X ^ n - C x).gal :=

modulo a few sorries (transfering solvability along isomorphic F-algebras, solvability is preserved by multiset-product, constant polynomials are solvable)

Thomas Browning (Feb 10 2021 at 07:54):

now the real fun begins!

Kevin Buzzard (Feb 10 2021 at 08:36):

You can embed the Galois group into a semidirect product of abelian groups

Kevin Buzzard (Feb 10 2021 at 08:37):

So you can write down a map to an abelian group with abelian kernel

Thomas Browning (Feb 10 2021 at 17:34):

Hoorah!
"The new definitions found immediate use: soon after we contributed our definition of
intermediate_field to mathlib, the Berkeley Galois theory group used it in a formalization
of the primitive element theorem. Soon after the primitive element theorem was merged
into mathlib, we used it in our development of the trace form. This anecdote illustrates the
decentralized development style of mathlib, with different groups and people building on each
other’s results in a collaborative process."
(https://arxiv.org/pdf/2102.02600.pdf)

Patrick Lutz (Feb 12 2021 at 19:02):

Thomas Browning said:

Hoorah!
"The new definitions found immediate use: soon after we contributed our definition of
intermediate_field to mathlib, the Berkeley Galois theory group used it in a formalization
of the primitive element theorem. Soon after the primitive element theorem was merged
into mathlib, we used it in our development of the trace form. This anecdote illustrates the
decentralized development style of mathlib, with different groups and people building on each
other’s results in a collaborative process."
(https://arxiv.org/pdf/2102.02600.pdf)

wow, this is really great

Kevin Buzzard (Feb 12 2021 at 20:06):

Also check out the mention you get on p14. It's about time you guys wrote a paper, by the way. Or maybe you want to do insolvability of the quintic first.

Johan Commelin (Feb 12 2021 at 20:13):

They wrote a paper for Exp.Math. right?

Kevin Buzzard (Feb 12 2021 at 20:14):

Oh maybe!

Patrick Lutz (Feb 15 2021 at 03:53):

@Thomas Browning I think I can't make it to the meeting tomorrow (just for this week). Sorry for the short notice.

Thomas Browning (Feb 15 2021 at 03:57):

No worries. Thanks for letting me know.

Thomas Browning (Feb 15 2021 at 03:57):

@Jordan Brown Do you want to meet this week, or skip until next week?

Jordan Brown (Feb 15 2021 at 09:46):

I think skipping until next week is fine -- I don't have anything I think we desperately need to talk about

Thomas Browning (Mar 10 2021 at 02:35):

@Jordan Brown Here's a progress update on the theoretical side of abel-ruffini (SBR implies solvable).
I've moved stuff to the abel_ruffini branch (as opposed to the abel-ruffini branch), to see where things are at.
Here are the remaining sorries (of various levels of difficulty):

  • If K ≃ₐ[F] L then is_solvable (K ≃ₐ[F] K) implies is_solvable (L ≃ₐ[F] L) (the main thing is just writing down the isomorphism between the two groups).
  • Applying a field automorphism to a root of unity results in raising that root of unity to some power.
  • X ^ n splits in any field.
  • Prove solvable_of_ker_le_range. I think that this is fully proved in the abel-ruffini branch, but things are rather messy, and we will need to clean things up before PRing.

At some point, could you work on cleaning up the solvable stuff in the main abel-ruffini branch?

Kevin Buzzard (Mar 10 2021 at 06:03):

Did you guys look at the Coq work? Do they set things up substantially differently?

Thomas Browning (Mar 10 2021 at 06:12):

I think so. We're taking a bit of a wacky approach with the whole inductive solvable-by-radicals stuff, but it seems to be working quite smoothly.

Thomas Browning (Mar 10 2021 at 21:31):

All the sorries are gone! (for SBR implies solvable)

Thomas Browning (Mar 10 2021 at 21:31):

I hacked together a proof of the short exact sequence lemma, but it would still be good to clean up the remaining stuff in solvable.lean


Last updated: Dec 20 2023 at 11:08 UTC