Project ideas

Stream: Berkeley Lean Seminar

[Patrick Lutz]

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]

(deleted)

[Jalex Stark]

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

[Kevin Buzzard]

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]

Define fundamental group of a topological space?

[Kevin Buzzard]

Higher homotopy groups even?

[Kevin Buzzard]

Make a basic API for locally ringed spaces?

[Kevin Buzzard]

Define Picard groups?

[Kevin Buzzard]

Ext and Tor?

[Patrick Lutz]

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

[Patrick Lutz]

Some of the possible topics we discussed were:

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

3) Fundamental theorem of calculus

[Patrick Lutz]

4) Galois Theory. Goal: prove Galois connection

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

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]

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

[Thomas Browning]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

The fundamental theorem is still not in Lean

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Lutz]

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

Oh, work comes and goes

[Patrick Lutz]

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]

@Kenny Lau what do you think?

[Kevin Buzzard]

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

[Kenny Lau]

sure

[Kevin Buzzard]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Kenny Lau]

yeah mainly

[Patrick Lutz]

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]

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

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

[Kenny Lau]

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

[Kenny Lau]

(tower law)

[Patrick Lutz]

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]

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]

go ahead

[Jordan Brown]

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]

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

[Jalex Stark]

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

[Scott Morrison]

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]

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]

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]

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

[Patrick Lutz]

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]

I think there's a lot about integrality in mathlib

[Kenny Lau]

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]

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]

@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)$ and $F[\alpha]$ (where $f$ is the minimal polynomial of $\alpha$) and then prove the properties of this isomorphism, for instance that it takes $x$ to $\alpha$.

[Patrick Lutz]

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

[Patrick Lutz]

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 $F$ after quantifying over $n$ 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]

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]

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]

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

[Thomas Browning]

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]

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

[Kenny Lau]

#3654 @Kevin Buzzard @Johan Commelin @Chris Hughes

[Jordan Brown]

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]

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

[Jordan Brown]

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

[Thomas Browning]

oh right, I see what you mean

[Thomas Browning]

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

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Patrick Lutz]

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]

but it's not a big deal

[Thomas Browning]

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]

make a new file for properties of subfields?

[Patrick Lutz]

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

[Patrick Lutz]

Also, I added two lemma statements about the degree of $E$ over $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]

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

[Patrick Lutz]

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

[Thomas Browning]

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]

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]

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

[Patrick Lutz]

Just for the first of the two lemmas I mean

[Patrick Lutz]

The second doesn't totally make sense without it

[Patrick Lutz]

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

[Thomas Browning]

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]

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]

maybe, but I would guess not for this project

[Kevin Buzzard]

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]

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]

Patrick Lutz said:

Thomas Browning How easy is it to transfer facts about adjoining elements to a subfield $F$ of a field $E$, thought of as an algebra map from $F$ to $E$, to the subfield of $E$ 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]

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]

I'm not sure

[Patrick Lutz]

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

[Thomas Browning]

No, but I just added it: adjoin.mono

[Patrick Lutz]

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

[Thomas Browning]

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]

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 $E$ being a separable extension of $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]

proved it

[Patrick Lutz]

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]

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

[Patrick Lutz]

Jalex Stark said:

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

More or less.

[Patrick Lutz]

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

[Patrick Lutz]

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

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]

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]

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]

looks good to me

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

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]

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]

Kenny Lau said:

#3654 Kevin Buzzard Johan Commelin Chris Hughes

merged

[Thomas Browning]

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]

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]

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

[Patrick Lutz]

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]

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]

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]

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]

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]

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]

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

[Patrick Lutz]

I want to use findim_lt from #3720

[Patrick Lutz]

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

[Thomas Browning]

oh I see

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

Actually, I think I may have just been misunderstanding submodule

[Patrick Lutz]

maybe it's not so bad

[Patrick Lutz]

Okay, maybe actually it is lol

[Kevin Buzzard]

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

[Patrick Lutz]

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

adjoin_findim_lt is done

[Patrick Lutz]

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

[Patrick Lutz]

Patrick Lutz said:

adjoin_findim_lt is done

I actually meant adjoin_dim_lt

[Patrick Lutz]

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

[Thomas Browning]

Seems reasonable to me

[Patrick Lutz]

We're at 150 commits btw

[Patrick Lutz]

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]

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

[Patrick Lutz]

Kevin Buzzard said:

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

What is the discord?

[Kevin Buzzard]

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

[Kenny Lau]

https://discord.gg/cNGnzX

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

this invite link expires in 1 day

[Kenny Lau]

just like any other

[Kevin Buzzard]

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

[Patrick Lutz]

We have finished proving the primitive element theorem!

[Patrick Lutz]

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

[Kevin Buzzard]

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]

Mathlib master gets fixed when breaking changes to mathlib are made

[Kevin Buzzard]

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

[Kevin Buzzard]

So your proof is guaranteed to live

[Kevin Buzzard]

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]

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]

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]

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

[Patrick Massot]

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]

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]

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

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

[Patrick Lutz]

How about 5 pm?

[Rahul Dalal]

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]

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]

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]

vector_space is a class

[Kenny Lau]

you don't refer to the instances by name

[Kenny Lau]

Lean just figures them out using typeclass inference

[Thomas Browning]

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

[Thomas Browning]

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

[Patrick Lutz]

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

[Patrick Lutz]

somewhere between 3-5 is best for me

[Patrick Lutz]

(as the starting time for the meeting)

[Patrick Lutz]

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

[Thomas Browning]

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]

sounds good

[Jordan Brown]

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]

I think it's just adjoin_root (polynomial)

[Kevin Buzzard]

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]

docs#adjoin_root.mk

[Jordan Brown]

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

[Jordan Brown]

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]

post the code that gives the message?

[Jordan Brown]

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

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

[Kenny Lau]

#backticks

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Thomas Browning]

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

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]

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

[Thomas Browning]

Ok, I've removed the subfield assumption from primitive_element_two_inf_key

[Thomas Browning]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

I think it still needs some cleaning up though

[Patrick Lutz]

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

[Patrick Lutz]

maybe in the adjoin.lean file

[Thomas Browning]

sure, go for it

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

Lean doesn't seem to understand the type coercion there

[Patrick Lutz]

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

[Patrick Lutz]

so I'll see what they say

[Patrick Lutz]

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

I think I've finished taking out my_roots

[Patrick Lutz]

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]

Sounds good.

[Patrick Lutz]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Johan Commelin]

You can adjoin {a,b} as well

[Johan Commelin]

And the two are not defeq (-;

[Thomas Browning]

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

[Thomas Browning]

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

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

[Thomas Browning]

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]

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]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Thomas Browning]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Kevin Buzzard]

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]

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

[Patrick Lutz]

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

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

[Thomas Browning]

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

[Kevin Buzzard]

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]

Ok, I've pushed some new brackets

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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]

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

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]

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

Is there anything bad about this?

[Thomas Browning]

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]

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]

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]

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

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

Make sure to upgrade mathlib to use it

[Patrick Lutz]

There are still lots of errors also

[Patrick Lutz]

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]

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

[Thomas Browning]

I'll take a stab at some of the errors

[Patrick Lutz]

Oh, I've also been working on this

[Patrick Lutz]

let me push my changes

[Thomas Browning]

I've taken care of the first error

[Thomas Browning]

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]

no I don't think so

[Patrick Lutz]

I just pushed

[Patrick Lutz]

Try pulling and let me know if there are any problems

[Patrick Lutz]

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]

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

[Patrick Lutz]

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

[Thomas Browning]

oh dear

[Patrick Lutz]

Not sure what to do about it though

[Patrick Lutz]

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

[Thomas Browning]

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

[Patrick Lutz]

It's definitely a bit better

[Patrick Lutz]

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

[Patrick Lutz]

I really wish we could get notation that did that

[Thomas Browning]

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

[Thomas Browning]

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

[Patrick Lutz]

Yeah, that's a good idea

[Patrick Lutz]

Do you want to, or should I?

[Thomas Browning]

I can do it if you want

[Patrick Lutz]

sure

[Thomas Browning]

done. feel free to add anything.

[Patrick Lutz]

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]

still, a number of things got uglier :(

[Thomas Browning]

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

[Patrick Lutz]

Yeah, for sure

[Patrick Lutz]

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

[Thomas Browning]

sure

[Patrick Lutz]

because currently new_primitive_element only imports from mathlib

[Patrick Lutz]

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]

not sure how you feel about that

[Patrick Lutz]

It doesn't seem to make anything harder

[Thomas Browning]

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

[Patrick Lutz]

hmm, that might be true

[Patrick Lutz]

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

[Thomas Browning]

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]

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

[Patrick Lutz]

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

Yes

[Thomas Browning]

of mathlib

[Patrick Lutz]

Yeah, that sounds reasonable

[Patrick Lutz]

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

[Patrick Lutz]

but don't make a PR yet

[Thomas Browning]

will do

[Thomas Browning]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

as usual

[Patrick Lutz]

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

[Thomas Browning]

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]

Patrick Lutz said:

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

I meant github not mathlib

[Patrick Lutz]

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]

ah, I see

[Patrick Lutz]

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

[Patrick Lutz]

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

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

[Patrick Lutz]

Yeah, I see it

[Patrick Lutz]

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

[Thomas Browning]

I was hoping for the same thing

[Thomas Browning]

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

[Thomas Browning]

that sounds doable, I think

[Patrick Lutz]

but it's not already in mathlib?

[Patrick Lutz]

oh wait, dumb question probably

[Patrick Lutz]

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]

(assuming that L is an algebra over F)?

[Patrick Lutz]

"if you know E and L are F algebras"

[Patrick Lutz]

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

[Patrick Lutz]

:/

[Thomas Browning]

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

[Patrick Lutz]

sounds good

[Patrick Lutz]

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]

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

[Thomas Browning]

cool

[Thomas Browning]

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

[Thomas Browning]

In particular: adjoin_findim_of_findim adjoin_findim_of_findim_base

[Patrick Lutz]

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]

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]

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]

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]

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

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

[Patrick Lutz]

Let me try to look into it

[Patrick Lutz]

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

[Patrick Lutz]

For me that seemed to fix the problem

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

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

[Patrick Lutz]

but I'm not entirely certain about that

[Thomas Browning]

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]

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]

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]

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

[Patrick Lutz]

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]

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]

we haven't added a namespace yet

[Thomas Browning]

(field would be fine, I think)

[Patrick Lutz]

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

[Thomas Browning]

#4153

[Johan Commelin]

Unfortunately, there seems to be a conflict already

[Thomas Browning]

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

[Johan Commelin]

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

[Thomas Browning]

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]

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

[Kevin Buzzard]

you should merge master into your branch maybe?

[Patrick Lutz]

Okay, I just merged master into our branch

[Patrick Lutz]

hopefully everything should work okay now

[Patrick Lutz]

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

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]

I'll take a look

[Thomas Browning]

Hopefully the separable.lean proofs are fixed now

[Thomas Browning]

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

[Kyle Miller]

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

[Patrick Lutz]

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]

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]

I'm surprised that didn't break more stuff

[Kyle Miller]

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]

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]

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]

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]

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Patrick Lutz]

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

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]

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]

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

[Thomas Browning]

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

[Patrick Lutz]

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]

That would be fine for now I think

[Kevin Buzzard]

You could promise the switch in a later PR maybe

[Kevin Buzzard]

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]

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

[Thomas Browning]

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

[Patrick Lutz]

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]

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]

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

[Patrick Lutz]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Lutz]

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]

Aha

[Patrick Lutz]

But it should be easy enough to fix

[Patrick Lutz]

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

[Kyle Miller]

I'm in the middle of fixing it

[Patrick Lutz]

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]

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]

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]

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]

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

[Patrick Lutz]

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

[Patrick Lutz]

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]

By the way, thanks for all the help Kyle!

[Kyle Miller]

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]

Pushed the change

[Kyle Miller]

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]

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

[Thomas Browning]

oh interesting

[Patrick Lutz]

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

I'm going to take a look at primitive_element_inf next

[Patrick Lutz]

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]

primitive_element.lean is now just about 260 lines btw

[Patrick Lutz]

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

[Patrick Lutz]

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

[Thomas Browning]

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

[Johan Commelin]

If it really is a special case, then yes.

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

Making it private means it won't clutter your autocomplete

[Kyle Miller]

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]

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

[Patrick Lutz]

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

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

[Patrick Lutz]

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

I don't think that I've split that one off as a lemma yet.

[Patrick Lutz]

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]

Not yet. I'll have time this afternoon if you haven't done it by then.

[Patrick Lutz]

Okay, I've done it. But now I also want to make a couple other changes to the separability before pushing.

[Patrick Lutz]

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]

Sounds good

[Thomas Browning]

I'm working on refactoring primitive_element_two_inf, so don't worry about those comments for now

[Patrick Lutz]

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]

should I push the style fixes anyway? They should be easy to merge later if need be

[Thomas Browning]

I might be doing some major rewriting, so hold off on those

[Thomas Browning]

actually, if you've already done them

[Thomas Browning]

then push them

[Thomas Browning]

and I'll work from there

[Patrick Lutz]

Okay, I just pushed them

[Patrick Lutz]

Let me know if you have any problems when you pull the changes

[Patrick Lutz]

Is it okay if I continue making some changes that don't affect primitive_element_two_inf?

[Patrick Lutz]

Also I can take care of the requested changes to the polynomial lemmas if that's okay with you

[Thomas Browning]

yeah, that's all fine

[Patrick Lutz]

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

ok, I've pushed the big refactor.

[Patrick Lutz]

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]

Hopefully we're close to merging now

[Patrick Lutz]

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]

oh I guess so

[Kevin Buzzard]

Why do you need is_subfield.pow_mem in a deprecated file?

[Kevin Buzzard]

I did a "remove a deprecated import from a file and then fix the several hundred errors caused by this" PR once.

[Patrick Lutz]

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]

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]

which should happen soon

[Patrick Lutz]

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

I saw it. It is a bit of an abomination, but I would be fine with it.

[Kevin Buzzard]

Primitive element theorem merged! Well done to all who contributed!

[Thomas Browning]

@Patrick Lutz Should we make a branch for turning adjoin into intermediate field now?

[Patrick Lutz]

Thomas Browning said:

Patrick Lutz Should we make a branch for turning adjoin into intermediate field now?

Yeah

[Thomas Browning]

https://github.com/leanprover-community/mathlib/tree/adjoin_intermediate_field

[Thomas Browning]

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]

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]

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]

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 $S \subset T$ then $L(S) \subset L(T)$?

[Thomas Browning]

I'm not sure familiar with it, but I'm looking at ring_theory/algebra.lean, line 1100

[Thomas Browning]

where it does stuff with galois connections and galois insertions to quickly get bounded_lattice

[Kevin Buzzard]

There's a design decision to be made here

[Kevin Buzzard]

And I'm not sure what the right one is

[Kevin Buzzard]

because I'm unaware of the ramifications

[Kevin Buzzard]

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]

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]

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]

The advantage of (2) is that you get the recursor for free

[Kevin Buzzard]

But I don't know how important the recursor will be

[Kevin Buzzard]

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]

Currently we have adjoin F S which uses ring.closure (I'm not sure which of the two approaches ring.closure uses)

[Thomas Browning]

ah, it looks like it uses the 2nd way

[Kevin Buzzard]

Oh you already have this direction!

[Thomas Browning]

yeah

[Kevin Buzzard]

Are you doing subrings or subfields?

[Thomas Browning]

subfields

[Kevin Buzzard]

And adjoin produces a subfield?

[Thomas Browning]

yes, but now an intermediate field

[Kevin Buzzard]

So this is a different function to the subring adjoin?

[Thomas Browning]

yeah, I just said subring closure because I hadn't gone far enough down the rabbit hole

[Thomas Browning]

it's defined in terms of field.closure

[Kevin Buzzard]

gotcha

[Patrick Lutz]

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]

Btw, @Thomas Browning, I just sent Anne a message asking if they have already done any work on refactoring field_theory/adjoin

[Patrick Lutz]

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]/p$)

[Thomas Browning]

Just proved the complete_lattice

[Thomas Browning]

It wasn't too bad

[Thomas Browning]

It will probably speed-up/obsolete some other lemmas we have in adjoin.lean

[Patrick Lutz]

@Thomas Browning presumably we should no longer import deprecated/subfield in field_theory/adjoin?

[Thomas Browning]

yeah, we need to get rid of that import

[Thomas Browning]

the problem is that closure is defined in that file

[Patrick Lutz]

oh, then I guess we need to port closure over to the new subfield file?

[Patrick Lutz]

No, wait, the new subfield also has some version of closure

[Patrick Lutz]

To me it looks like it should be fine to use the new version of subfield closure

[Patrick Lutz]

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]

I'll take a look

[Patrick Lutz]

Okay, I think I found the relevant part of "Theorem Proving in Lean" (on inheritance)

[Patrick Lutz]

Hmm, actually that section of "Theorem Proving in Lean" is really short

[Thomas Browning]

I've figured out how to rewrite adjoin in terms of the bundled subfield

[Thomas Browning]

Ok, it's pushed but there are a bunch of errors

[Patrick Lutz]

I fixed a couple errors. I'll take a more serious look this evening

[Patrick Lutz]

A couple comments

[Patrick Lutz]

a lot of things need to change from field.foo to subfield.foo

[Patrick Lutz]

some instances are no longer necessary. Like now adjoin F S is automatically a subfield of E and also a field

[Patrick Lutz]

also, obviously, lots of hypotheses have to change from is_subfield to something else

[Patrick Lutz]

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

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]

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]

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]

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]

shouldn't we just change all bottom subalgebras to bottom intermediate fields?

[Thomas Browning]

or are there some lemmas that should be stated in terms of the bottom subalgebra?

[Patrick Lutz]

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]

@Thomas Browning I did a little bit more work on refactoring field.adjoin and primitive_element. Here's a couple of comments:

[Patrick Lutz]

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]

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]

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]

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]

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

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]

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 $F^{\text{deg } p}$ to $F[x]/p$ and then show it's an isomorphism

[Patrick Lutz]

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]

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]

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 $F^{\text{deg } p}$ to $F[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]

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 $F^{\text{deg } p}$ to $F[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]

There's div and mod in data.polynomial.field_division

[Patrick Lutz]

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]

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]

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]

aah there's mod_by_monic in data.polynomial.div

[Kevin Buzzard]

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]

linearity should be easy and now hopefully the library can take it from there

[Thomas Browning]

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]

(deleted)

[Thomas Browning]

(deleted)

[Thomas Browning]

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]

Here's a fun error message

[Thomas Browning]

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]

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]

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]

The weird thing is that the lattice is defined from the partial order defined in intermediate_field.lean

[Thomas Browning]

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]

(deleted)

[Kevin Buzzard]

There shouldn't be any diamonds in mathlib and this sounds like a diamond

[Patrick Lutz]

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]

Also is the ban on diamonds by convention or by law (i.e. part of the rules of Lean)?

[Patrick Lutz]

The only time I've seen it mentioned before was in Thomas Hales' blog post on Lean

[Johan Commelin]

It's a convention. But without it you land in a swamp that you really don't want to get into

[Kevin Buzzard]

If you have two non defeq partial orders then that's a great example of a diamond

[Kevin Buzzard]

If mathlib made both of those partial orders then people will want to know about it

[Patrick Lutz]

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]

Not sure what the right solution is though

[Kyle Miller]

If both bounded_lattice instances are equal, can you delete a less-general one?

[Patrick Lutz]

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]

The adjunction is probably fine.

[Patrick Lutz]

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

(deleted)

[Patrick Lutz]

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]

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

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]

If one of your definitions of <= was "sorry" then no wonder Lean was finding it hard to work with :-)

[Patrick Lutz]

Yeah, I just didn't even realize that line was there. And it looks like Thomas actually removed it yesterday

[Patrick Lutz]

I just hadn't pulled any changes since then

[Thomas Browning]

yeah, I think that the issue is resolved now

[Thomas Browning]

and there was a sorried lattice instance (which I might have been responsible for... oops)

[Thomas Browning]

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]

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

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]

Are the corresponding coercions there for eg submonoid?

[Kevin Buzzard]

Maybe subalgebra is a better question

[Thomas Browning]

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]

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]

@Patrick Lutz Is there anything else you want done before the PR?

[Thomas Browning]

I proved the general induction result, although the proof turned out to be longer than I expected.

[Patrick Lutz]

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

#4468

[Thomas Browning]

Unfortunately there's a merge conflict in algebra.lean

[Thomas Browning]

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

What was the problem with defining an inverse?

[Thomas Browning]

it just seems a little tricky to write down a function that takes a lift and takes it mod p

[Jordan Brown]

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]

lemma surjective : function.surjective (adjoin_root.mk p) :=
begin
  exact ideal.quotient.mk_surjective,
end

[Thomas Browning]

@Jordan Brown so you should be able to just use ideal.quotient.mk_surjective as is

[Thomas Browning]

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

oh wow, I always prove this in lectures by counting, and then deduce the primitive element theorem from it.

[Kevin Buzzard]

This would be a very cool milestone

[Patrick Lutz]

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]

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

@Thomas Browning adjoin_root_equiv_adjoin_simple looks kind of scary somehow

[Patrick Lutz]

So many @s

[Patrick Lutz]

I'm going to work on findim_adjoin_integral either tonight or tomorrow morning

[Thomas Browning]

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]

They're gone: https://github.com/leanprover-community/mathlib/commit/f3bce8782b23c50d553bed41819ac8df1f336a40

[Thomas Browning]

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]

so we need another way of showing that polynomial.degree_lt K n has findim equal to n

[Thomas Browning]

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]

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]

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]

this is great, except that if F is finite then we can't necessarily choose an s : finset F of cardinality n

[Thomas Browning]

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]

fun_equiv_degree_lt is somehow not the correct theorem, is it! s could be any finite subset of anything.

[Kevin Buzzard]

I see -- this is a very explicit map coming from evaluation and using the fact that F is a field.

[Thomas Browning]

Yeah, but you're right that it should be true for any finset s (of any Type)

[Kevin Buzzard]

degree_lt_eq_span_X_pow is what you want

[Kevin Buzzard]

in ring_theory.polynomial.basic

[Thomas Browning]

I saw that, but do we know that they are linearly independent?

[Kevin Buzzard]

that'll be another lemma

[Kevin Buzzard]

"a polynomial is zero iff all its coefficients are zero"

[Kevin Buzzard]

but I agree that there's work to do here

[Patrick Lutz]

@Thomas Browning You haven't added module_map from the galois_theory repo anywhere right?

[Patrick Lutz]

At least I don't see it in any of the changes you've pushed

[Thomas Browning]

it should be in adjoin_root.lean

[Thomas Browning]

https://github.com/leanprover-community/mathlib/blob/galois_definition/src/ring_theory/adjoin_root.lean

[Patrick Lutz]

oh, I see it

[Patrick Lutz]

I've been refactoring that a little bit so I'm going to change it soon

[Thomas Browning]

cool

[Thomas Browning]

I've almost proved the two sorries, so don't mess with those just yet

[Thomas Browning]

actually, let me just push what I have now

[Thomas Browning]

pushed

[Patrick Lutz]

Okay, now I pushed

[Patrick Lutz]

I'll look at what you did in a sec

[Patrick Lutz]

do you think we should give degree_lt_linear_map a different name?

[Patrick Lutz]

also I think it might make sense to combine the injectivity and surjectivity proofs into one big proof

[Thomas Browning]

that seems reasonable

[Patrick Lutz]

the linter is not very happy btw

[Thomas Browning]

where should all the temp stuff go?

[Patrick Lutz]

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]

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]

well, proving the basis seemed rather hard

[Patrick Lutz]

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]

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]

maybe the finite_dimensional instance should just be a lemma?

[Thomas Browning]

where is the f \ne 0 hypothesis?

[Thomas Browning]

oh I see

[Patrick Lutz]

instance finite_dimensional (hf : f ≠ 0) : finite_dimensional K (adjoin_root f) :=
linear_equiv.finite_dimensional (degree_lt_linear_equiv f hf)

[Thomas Browning]

yeah, that could be lemma

[Patrick Lutz]

it's actually probably possible to remove the hypothesis too

[Thomas Browning]

it's not true for f=0 is it?

[Patrick Lutz]

I don't know what adjoin_root 0 does but it probably is finite dimensional

[Kevin Buzzard]

Depends on how lean defined things!

[Kevin Buzzard]

But I bet it just adds 37

[Thomas Browning]

wouldn't it be the quotient by the zero ideal?

[Patrick Lutz]

oh maybe

[Patrick Lutz]

you're probably right

[Patrick Lutz]

oh well

[Kevin Buzzard]

I'm on mobile but am now very interested :-)

[Kevin Buzzard]

If f is reducible what does it add?

[Patrick Lutz]

?

[Patrick Lutz]

Kevin Buzzard said:

If f is reducible what does it add?

what do you mean by add?

[Kevin Buzzard]

I just didn't know the definition. I've looked now and disappointingly it does just quotient out by (f)

[Kevin Buzzard]

So yes it looks like it's not true when f=0.

[Kevin Buzzard]

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]

yeah, in a sense I think the quotient by (0) is not the same as adjoining a root of 0

[Patrick Lutz]

but it makes sense that it's defined this way

[Patrick Lutz]

hmm, why is it so hard to work with bases in mathlib?

[Thomas Browning]

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]

yeah, somehow even defining the basis is getting annoying

[Patrick Lutz]

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, \ldots, n-1\}$ under $i \mapsto x^i$ then you need to somehow know in the definition of $i \mapsto x^i$ that $i < n$

[Patrick Lutz]

actually, it would be nice to have the following lemma (maybe it's already in mathlib?): if $S$ is a subset of a vector space $V$ which happens to be linearly independent, contained in a subspace $W$ and span $W$ then it's a basis for $W$ (after some appropriate coercion)

[Patrick Lutz]

but I can't immediately find anything like that

[Thomas Browning]

Do you know how to finish off the last sorry?

[Thomas Browning]

lean knows that functions from a finset are finite_dimensional, so I assume that it also knows what the dimension is

[Patrick Lutz]

yeah, I think it's dim_fun

[Patrick Lutz]

I can try finishing it off

[Thomas Browning]

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]

findim_fintype_fun_eq_card did the trick (thanks for telling me about dim_fun)

[Patrick Lutz]

nice

[Patrick Lutz]

is linear_algebra.lagrange still needed at the top of the file?

[Patrick Lutz]

looks like it's not

[Thomas Browning]

oh, I guess not

[Thomas Browning]

should we include a bijection(either just an equiv or something more fancy) between subgroup and intermediate_field ?

[Patrick Lutz]

I just pushed some changes adding documentation to make the linter happy

[Patrick Lutz]

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]

@Patrick Lutz Anything else you want to do before the PR?

[Thomas Browning]

do we need any namespaces?

[Patrick Lutz]

for field_theory/galois? Probably should put it in some namespace.

[Patrick Lutz]

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]

even on the most recent push?

[Patrick Lutz]

Three defs are missing documentation

[Patrick Lutz]

yeah I think so

[Patrick Lutz]

Try writing #lint at the bottom of the file

[Thomas Browning]

Ah

[Thomas Browning]

I'll take care of that

[Patrick Lutz]

okay, cool. I also made a couple tiny changes to the documentation

[Patrick Lutz]

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]

there are some small changes to other files, but not much else

[Thomas Browning]

I guess one major thing is that field adjoin is isomorphic to adjoin_root

[Patrick Lutz]

where was that? In field_theory/adjoin.lean?

[Thomas Browning]

yeah

[Thomas Browning]

are you drafting the PR?

[Patrick Lutz]

no

[Patrick Lutz]

should I?

[Patrick Lutz]

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]

should we make some namespaces first?

[Patrick Lutz]

yeah

[Patrick Lutz]

--TODO: Maybe upgrade this to some sort of lattice anti-isomorphism?

Do you want to leave this in?

[Thomas Browning]

might as well, I don't know if mathlib has anti-isomorphisms yet?

[Patrick Lutz]

sure

[Patrick Lutz]

it does have antitone galois connections I think?

[Patrick Lutz]

is galois a reasonable namespace?

[Thomas Browning]

sure

[Thomas Browning]

should is_galois go in the namespace?

[Patrick Lutz]

oh, maybe not

[Patrick Lutz]

I'm not really sure how that works

[Patrick Lutz]

but judging off other files in mathlib, maybe not

[Patrick Lutz]

Patrick Lutz said:

it does have antitone galois connections I think?

Actually I'm not sure this is true

[Thomas Browning]

I guess putting it all in a galois namespace is fine

[Patrick Lutz]

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]

should I ask about antitone galois connections in one of the bigger streams on zulip?

[Patrick Lutz]

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]

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]

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]

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]

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]

@Thomas Browning Looks like there's still a few missing docstrings: https://github.com/leanprover-community/mathlib/runs/1306429257

[Thomas Browning]

#4786

[Patrick Lutz]

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

oops, you're right

[Johan Commelin]

@Thomas Browning @Patrick Lutz Congrats with this milestone!

[Johan Commelin]

I think it would be good to split this into a bunch of smaller PRs

[Johan Commelin]

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]

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]

@Johan Commelin

[Johan Commelin]

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

oooh, interesting

[Thomas Browning]

should I delete the other PR's then?

[Thomas Browning]

or rather, close them?

[Johan Commelin]

depends...

[Johan Commelin]

I didn't look at them yet.

[Johan Commelin]

If they are logical units, then I would just use those

[Thomas Browning]

They are #4791 #4792 #4793

[Johan Commelin]

From a first glance, I think you can leave those open

[Johan Commelin]

And maybe use this approach to create some more PRs

[Patrick Lutz]

Johan Commelin said:

Thomas Browning Patrick Lutz Congrats with this milestone!

Thomas did almost all the work for this one btw.

[Thomas Browning]

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

Presumably there's a way to have the galois_definition PR no longer include changes to those three files?

[Johan Commelin]

Hmm weird. You sure you pushed after the git merge? (@Thomas Browning)

[Thomas Browning]

I tried:

git checkout master
git pull master
git checkout galois_definition
git merge master
git push

[Thomas Browning]

(e.g., https://github.com/leanprover-community/mathlib/pull/4786/commits/29cc4970236ebb6654c95c50e5a6bd5017f33681)

[Johan Commelin]

Weird. Maybe someone else can help. I need to do other stuff atm

[Patrick Massot]

I guess git push errored, right?

[Patrick Massot]

It should have been git push -f

[Thomas Browning]

no, it didn't error

[Patrick Lutz]

Doesn't the fact that the automatic check detected no merge conflicts with master show that the push was successful?

[Patrick Massot]

Do you want me to try?

[Patrick Massot]

It would be a bit risky since I have no idea what you're doing

[Thomas Browning]

you can go ahead and try

[Thomas Browning]

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]

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]

This is definitely conflict

[Patrick Massot]

I just did:

• git checkout master
• git pull
• git checkout galois-definition
• git rebase master

[Patrick Massot]

and I get a conflict in src/field_theory/adjoin.lean

[Thomas Browning]

ah, what's the definition between git merge and git rebase?

[Patrick Lutz]

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]

IIRC there's a stackoverflow question called that with a gazillion votes

[Patrick Massot]

I pushed something

[Patrick Lutz]

As far as I know, the difference between merge and rebase is how the commit graph looks

[Patrick Lutz]

but I'm hardly a git guru

[Patrick Massot]

Does it look better now?

[Patrick Lutz]

It looks identical to me

[Patrick Lutz]

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]

Does it still show stuff as new whereas it's already in mathlib?

[Patrick Lutz]

yes

[Thomas Browning]

yeah. For a concrete example, mathlib now has equalizer (and also a mem_equalizer lemma)

[Thomas Browning]

so I wouldn't expect the PR to have any changes to subalgebra.lean

[Patrick Lutz]

but also I detect no changes after what @Patrick Massot just did

[Patrick Lutz]

It's surprisingly hard to find information on what github decides to display in the "files changed" tab on pull requests

[Patrick Massot]

git got confused by moving stuff

[Patrick Massot]

The PR now duplicates this equalizer stuff

[Patrick Massot]

It got one from master and one from the PR

[Patrick Massot]

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]

So Patrick, if you still have the old galois-definition branch you should force push

[Patrick Massot]

(I mean before Thomas's attempted merge)

[Patrick Massot]

A lot more manual work will be needed

[Patrick Lutz]

okay, let me look into it

[Patrick Lutz]

Patrick Massot said:

The PR now duplicates this equalizer stuff

okay, this all makes a lot more sense now

[Patrick Massot]

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]

I don't really see how git could have been smarter here, unless it learns about Galois theory.

[Patrick Lutz]

Would it have to worked to merge the branches from the other PRs instead of master?

[Patrick Lutz]

it might be easiest to just delete stuff by hand

[Patrick Massot]

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]

What if the other PRs were from branches that shared a common commit with this branch?

[Patrick Massot]

Oh, yes that would help

[Patrick Lutz]

Although I'm not sure that's the case here.

[Patrick Lutz]

And now those other branches are deleted because the PRs were merged

[Patrick Massot]

Life is difficult.

[Patrick Lutz]

I mean in this case it shouldn't be too difficult to do by hand

[Patrick Lutz]

but if there's a better way it would be nice to figure it out

[Johan Commelin]

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]

hmm, but I think they don't share commits in common with the galois_definition branch

[Patrick Lutz]

@Thomas Browning, this is only a problem for #4791 right? The stuff in the other two PRs is not duplicated?

[Thomas Browning]

nope, it's also a problem for finite_dimensional.lean

[Thomas Browning]

algebra_equiv_equiv_algebra_hom is duplicated

[Patrick Lutz]

okay, but not for degree_lt_iff_coeff_zero right?

[Thomas Browning]

not sure

[Patrick Lutz]

okay, I'll double check

[Thomas Browning]

that one looks fine

[Thomas Browning]

I just pushed some commits where I removed some redundant stuff

[Patrick Lutz]

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]

"removing duplicates created by merge": Removes duplicate "i"

[Thomas Browning]

lol

[Patrick Lutz]

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]

they were

[Thomas Browning]

we might need to change other files that use those three results

[Thomas Browning]

since some namespaces got changed

[Patrick Lutz]

oh good point. But I guess that would have happened regardless

[Patrick Lutz]

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]

right now I can't edit anything until I can pull the oleans from github (once the compliation finishes)

[Thomas Browning]

or rather, I can edit stuff but I can't see whether it worked or not

[Patrick Lutz]

I'm trying to do it right now

[Patrick Lutz]

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]

hmm, something else has broken somehow. Lean doesn't know about adjoin_le_algebra_adjoin

[Patrick Lutz]

hmm, this worries me a lot

[Thomas Browning]

@Patrick Lutz I fixed it.

[Patrick Lutz]

but do you know how it happened?

[Thomas Browning]

That lemma got renamed to adjoin_eq_algebra_adjoin at some point

[Patrick Lutz]

but wasn't everything compiling recently?

[Patrick Lutz]

was it renamed in the last day?

[Thomas Browning]

oh huh

[Thomas Browning]

not sure

[Thomas Browning]

maybe the rebase did something?

[Patrick Lutz]

Yeah, I'm a little confused what's going on

[Patrick Lutz]

hmm, somehow nothing else seems to have changed

[Patrick Lutz]

as far as I can tell, the adjoin_le_algebra_adjoin thing is the only thing that got messed up

[Patrick Lutz]

but I can't figure out how what Patrick did caused that to mess up but nothing else

[Patrick Lutz]

I assume it's because of the use of force push but I'm still confused

[Johan Commelin]

Hey, please let me know if you need more (git) help.

[Thomas Browning]

I think we got it all cleaned up, thanks though

[Johan Commelin]

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]

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]

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]

The PR that depends on a smaller one can include the changes from the small one.

[Johan Commelin]

I guess if you don't, then CI will throw a bunch of errors.

[Johan Commelin]

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]

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]

Honestly, I hadn't thought that far ahead. I guess we'll discuss our plans at the meeting tomorrow.

[Kevin Buzzard]

Quintic hasn't been done in any theorem prover??

[Johan Commelin]

It's still open on Freek's list

[Kevin Buzzard]

I had it in my head that it was just silly things like FLT which were still open.

[Kevin Buzzard]

That's very much an accessible goal for us now

[Johan Commelin]

16. Insolvability of General Higher Degree Equations

[Thomas Browning]

We're going to go for it!

[Thomas Browning]

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

wow, fast work

[Thomas Browning]

well, we basically already had that result, except with the K's replaced by F(a).

[Patrick Lutz]

I just merged abel-ruffini with galois_definition to incorporate that change

[Jordan Brown]

what would be the best way to state that the commutator of normal subgroups is normal?

[Jordan Brown]

as an instance of normal_subgroup?

[Patrick Lutz]

Yeah, I think so

[Jordan Brown]

I don't think I have permission to push changes to abel-ruffini

[Jordan Brown]

also, I'm not sure which file the definition of solvability should go into

[Thomas Browning]

@Jordan Brown Send a message like this one: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Access.20to.20Mathlib

[Thomas Browning]

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]

@Thomas Browning Should we update abel-ruffini every time galois_definition is changed?

[Thomas Browning]

doesn't need to be every time, but whenever it's convenient, I think

[Johan Commelin]

At least whenever a PR is merged (or marked as ready to merge).

[Patrick Lutz]

@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 $P$ is some property of intermediate fields of $E/F$, $E = F(a_1,\ldots, a_n)$ and for each intermediate field $K$ such that $P$ holds of $K$ and each $a_i$, $P$ holds of $K(a_i)$. Then $P$ holds of $E$

[Patrick Lutz]

(And assume $P$ holds for $F$ of course)

[Patrick Lutz]

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]

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 $P$ is some property of intermediate fields of $E/F$, $E = F(a_1,\ldots, a_n)$ and for each intermediate field $K$ such that $P$ holds of $K$ and each $a_i$, $P$ holds of $K(a_i)$. Then $P$ holds of $E$

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]

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]

is it okay to push things to the branch if they still have sorrys?

[Jordan Brown]

I stated that the commutator of two normal subgroups is normal in the abelianization file but haven't proved it

[Jordan Brown]

I could just take it out and push the definition of solvability

[Patrick Lutz]

Jordan Brown said:

is it okay to push things to the branch if they still have sorrys?

Sure.

[Patrick Lutz]

Jordan Brown said:

I could just take it out and push the definition of solvability

No, definitely leave it in

[Thomas Browning]

@Jordan Brown sorries are totally fine. Just make sure that it compiles.

[Patrick Lutz]

@Jordan Brown Did you push your changes yet?

[Patrick Lutz]

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]

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

But when I pulled the latest changes to the branch, something broke in the proof of alg_hom_adjoin_integral_equiv

[Patrick Lutz]

wait, nevermind

[Patrick Lutz]

I now ran leanproject get-cache and the problem is gone

[Patrick Lutz]

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]$, right? Which we don't currently have?

[Patrick Lutz]

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]

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]

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]

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]

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]$, 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]

@Patrick Lutz I can take care of this lemma

[Thomas Browning]

oh actually, I see what issue you're running into

[Thomas Browning]

passing from E/bot to E/F

[Patrick Lutz]

Yeah, and likewise from top/F to E/F

[Thomas Browning]

it seems like there really should be some sort of "isomorphism of field extensions"

[Thomas Browning]

E/F isomorphic to E'/F'

[Patrick Lutz]

Yeah, that's probably the right way to do this

[Thomas Browning]

it might be a ring isomorphism taking F to F'

[Patrick Lutz]

and we would need to show that things like separability and normality are preserved by isomorphism

[Thomas Browning]

yeah

[Patrick Lutz]

and galois-ness

[Patrick Lutz]

Thomas Browning said:

it might be a ring isomorphism taking F to F'

It also needs to preserve algebra structure

[Thomas Browning]

maybe it's a pair of ring isomorphisms E -> E' and F -> F'?

[Patrick Lutz]

Sounds reasonable

[Thomas Browning]

where would such a thing be defined?

[Patrick Lutz]

I don't know

[Thomas Browning]

it would have to be below separable.lean and normal.lean, I think

[Patrick Lutz]

what does below mean?

[Thomas Browning]

in the file structure

[Patrick Lutz]

yeah but does below mean "depends on" or "is depended on"?

[Thomas Browning]

depends on

[Patrick Lutz]

I think it should be independent of separable and normal

[Thomas Browning]

oops

[Patrick Lutz]

and then separable and normal should have lemmas saying they are preserved by isomorphism

[Thomas Browning]

yeah

[Thomas Browning]

that's what I meant

[Patrick Lutz]

ohh

[Patrick Lutz]

maybe one of us should ask some questions on the outside zulip about this

[Thomas Browning]

yeah, we should

[Patrick Lutz]

like where it should go, how best to state it

[Thomas Browning]

I can do that

[Patrick Lutz]

sounds good

[Patrick Lutz]

btw, https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20Together.202021

[Patrick Lutz]

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]

It's asked in #maths

[Thomas Browning]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Isomorphism.20of.20Field.20Extensions

[Jordan Brown]

I just pushed the changes!

[Jordan Brown]

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]

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

well, the generating set is closed under conjugation

[Patrick Lutz]

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]

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

https://leanprover-community.github.io/mathlib_docs/deprecated/subgroup.html#group.normal_closure.is_normal?

[Thomas Browning]

The problem is that Jordan is take closure, not normal_closure

[Patrick Lutz]

The definition of normal closure in mathlib is group closure of the set of conjugates of a set

[Thomas Browning]

oh, that might make it not too bad

[Patrick Lutz]

yeah, it would require unfolding the definition of normal_closure a bit but that should work I think

[Thomas Browning]

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

@Thomas Browning Do you know if mathlib knows that the top subgroup of a group has the same cardinality as the group?

[Patrick Lutz]

If you don't know, I can ask in one of the main streams

[Patrick Lutz]

I assume it would be enough to know that there is an isomorphism between (\top : subgroup G) and G

[Thomas Browning]

I'd assume so, because of an isomorphism like that, but I don't know exactly

[Patrick Lutz]

Yeah, the problem is I can't find such an isomorphism in mathlib right now

[Jordan Brown]

ah okay, that does reduce it to something a lot more manageable

[Jordan Brown]

also, mathlib is telling me that continuous integration failed on Lint style and Build mathlib; what should I do about this?

[Thomas Browning]

in this case, it's just complaining that you used sorry

[Thomas Browning]

https://github.com/leanprover-community/mathlib/runs/1344650495

[Thomas Browning]

it's worth checking what went wrong, but if it's just sorries then there's nothing to worry about

[Patrick Lutz]

and the lint is complaining that some lines have more than 100 characters

[Patrick Lutz]

to fix that, just insert newlines in reasonable places so that the lines are less than 100 characters

[Patrick Lutz]

VSCode should display a helpful vertical line showing where 100 characters is

[Patrick Lutz]

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

no worries, it's an interesting discussion

[Thomas Browning]

although I don't think that the automation will solve the immediate problem at hand

[Patrick Lutz]

lol, I agree. At least not this year

[Patrick Lutz]

@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)$ are exactly $F$ then $E/F$ is Galois

[Patrick Lutz]

To be fair, this is a place where it would be pretty reasonable to just talk about subfields

[Patrick Lutz]

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]

@Jordan Brown I pushed a few style changes to abelianization.lean. I didn't add/change any of the content though

[Patrick Lutz]

@Thomas Browning If $E$ and $E'$ are equivalent as $F$ algebras then one way to conclude $E/F$ is Galois if you know $E'/F$ is Galois is to show that $F \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]

Note that this strategy wouldn't work for the case where $E/F$ is equivalent to $E/F'$

[Patrick Lutz]

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]

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]

actually, I don't think that's quite enough

[Thomas Browning]

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]

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]

yeah, I had originally imagined having some kind of result about transferring Galois from $E/F$ to $E/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]

did you push the changes you made btw?

[Patrick Lutz]

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]

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]

Patrick Lutz said:

Thomas Browning If $E$ and $E'$ are equivalent as $F$ algebras then one way to conclude $E/F$ is Galois if you know $E'/F$ is Galois is to show that $F \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]

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]

Thomas Browning said:

Patrick Lutz said:

Thomas Browning If $E$ and $E'$ are equivalent as $F$ algebras then one way to conclude $E/F$ is Galois if you know $E'/F$ is Galois is to show that $F \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]

actually, we could use the galois.tower_top thing in one place: if we know that $E/F$ is Galois then we can conclude that $E$ is Galois over (\bot : intermediate_field F E)

[Patrick Lutz]

although I guess I'm not sure if we ever need to do that now that I think about it

[Patrick Lutz]

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]

I think we only have it for a single element

[Jordan Brown]

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]

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]

@Jordan Brown I think it's missing

[Johan Commelin]

Should be a 3-line PR (-;

[Jordan Brown]

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]

also, Patrick, have you pushed the cases reduction for the normal commutator proof yet?

[Thomas Browning]

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

Do you guys meet in person?

[Patrick Lutz]

@Kevin Buzzard No, on zoom. Actually the majority of us are not even physically in Berkeley right now.

[Patrick Lutz]

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]

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]

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]

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

E.g. show that normal_closure is idempotent, show that it is always bigger than the subgroup closure, etc

[Patrick Lutz]

I can do those myself later today. Or you can do them if you want

[Patrick Lutz]

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]

just for convenience

[Thomas Browning]

it's not

[Thomas Browning]

the commutator subgroup can contain non-commutators

[Patrick Lutz]

Thomas Browning said:

the commutator subgroup can contain non-commutators

oh, lol, nevermind then.

[Patrick Lutz]

well, at least a lemma saying that for commutator we don't need to use normal_closure

[Patrick Lutz]

which should follow from commutator_eq_general_commutator_top_top

[Kevin Buzzard]

You could prove that normal closure and forgetful functor form a Galois insertion between normal subgroups and subsets

[Kevin Buzzard]

Is this not all already there though?

[Kevin Buzzard]

normal_closure is defined in group_theory.subgroup and there's a ton of lemmas about it

[Kevin Buzzard]

but the Galois insertion fact doesn't seem to be proved

[Patrick Lutz]

Kevin Buzzard said:

Is this not all already there though?

I don't see it

[Patrick Lutz]

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]

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]

also what are you going to talk about?

[Patrick Lutz]

just out of curiosity

[Thomas Browning]

Patrick Lutz said:

also what are you going to talk about?

Lean!

[Patrick Lutz]

maybe I should go

[Thomas Browning]

You're certainly welcome, although you probably won't learn anything new

[Patrick Lutz]

are you going to advertise the "Berkeley Lean seminar" (maybe a misleading name at this point)?

[Patrick Lutz]

https://github.com/leanprover/lean4/commit/cf7779936419085093ab0ea20f4738dd08030f90 btw

[Patrick Lutz]

unrelated

[Thomas Browning]

I think I'll mention what we've been doing in Galois theory

[Patrick Lutz]

we could consider offering to help newcomers

[Patrick Lutz]

who are working through tutorials or w/e

[Patrick Lutz]

not that there will necessarily be very many

[Patrick Lutz]

or any

[Kevin Buzzard]

You're right, they've proved the basics but they didn't prove it was a Galois insertion

[Kevin Buzzard]

There is some abstract thing called a closure operator

[Kevin Buzzard]

Which satisfies some axioms, which are presumably the ones they prove

[Patrick Lutz]

wouldn't a closure operator be idempotent?

[Kevin Buzzard]

Normal closure of normal closure is normal closure, right?

[Patrick Lutz]

yeah, but that's not proved in mathlib I think

[Kevin Buzzard]

Oh well clearly whoever did it did a shoddy job :-) I think I've even seen closure operators axiomatised somewhere -- Wikipedia?

[Patrick Lutz]

I mean it's also possible that it's already in mathlib and I just can't find it

[Patrick Lutz]

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)$ is a Galois connection then $f \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]

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]

@Patrick Lutz You can look at field_theory/adjoin.lean for how to quickly prove Galois insertions

[Kevin Buzzard]

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]

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]

A Galois connection is a pair of adjoint functors between preorders.

[Kevin Buzzard]

A Galois insertion is a pair of adjoint functors such that one of the two compositions is the identity map.

[Kevin Buzzard]

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]

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]

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]

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]

I propose we redefine subgroup.normal as follows

[Patrick Lutz]

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]

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]

It would be nice to know why it was changed

[Patrick Lutz]

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]

just pushed a commit showing that abelian groups are solvable.

[Patrick Lutz]

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]

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]

They said it was really annoying

[Thomas Browning]

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

@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/F$ and $K/F$ are both field extensions and $L$ is an intermediate field of $E/F$ then there is an equivalence between maps of $E$ into $K$ which fix $F$ and pairs of maps the first of which maps $L$ into $K$ fixing $F$ and the second of which maps $E$ into $K$ as an $L$-algebra (using the first map to think of $K$ as an $L$-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]

Are the types of x and y different?

[Kevin Buzzard]

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]

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]

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]

This is the kind of question which Mario, Reid and Chris are good at

[Kevin Buzzard]

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]

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]

If it doesn't then you might need to call for help.

[Kevin Buzzard]

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]

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]

eq_mpr_heq might be a better approach. eq.recs are hard to get rid of.

[Patrick Lutz]

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]

They are not equal by rfl

[Patrick Lutz]

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]

Also it's definitely possible that there's a better way to go about this

[Kevin Buzzard]

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]

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]

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]

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φ, 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]

okay, let me look at it a bit and then I'll ask in one of the bigger streams

[Patrick Lutz]

thanks for the help

[Kevin Buzzard]

no problem

[Kevin Buzzard]

You're all PhD students/post-docs, right?

[Kevin Buzzard]

I have a lot of time for people like you

[Patrick Lutz]

there aren't very many of us any more. But we're all PhD students I guess

[Patrick Lutz]

although I hope to be a postdoc soon

[Kevin Buzzard]

yeah, you can go and spread the word elsewhere :-)

[Patrick Lutz]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Dealing.20with.20heq.20and.20Sigma.20types

[Thomas Browning]

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]

doesn't that show that they are definitionally equal pointwise?

[Thomas Browning]

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]

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]

and not by rfl

[Patrick Lutz]

Yeah, the problem is that definitional equality means something much stronger than what we normally think of as "mathematical objects being equal"

[Patrick Lutz]

it means they are equal for purely syntactic reasons

[Patrick Lutz]

literally it means that they can be beta reduced to the same term

[Patrick Lutz]

and this is causing problems here because f is being used in the specification of the type of g

[Patrick Lutz]

Reid has solved the problem

[Thomas Browning]

I saw, although I'm having trouble coming up with the analog of have : f = λ s, φ s.1, sorry,

[Kevin Buzzard]

Oh lol, you accused me of making the lambda <a, b> sin :-)

[Kevin Buzzard]

I see that you inserted the sin and then claimed it was due to me :-)

[Kevin Buzzard]

NB i don't care :-)

[Kevin Buzzard]

In your case, you want to prove that the algebra maps are the same before you do the subst

[Patrick Lutz]

I didn't realize it was a sin when I inserted it

[Kevin Buzzard]

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]

yeah, that makes sense

[Kevin Buzzard]

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]

yeah, the subst thing seems really helpful here

[Patrick Lutz]

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]

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]

I guess maybe the problem is that you want to subsitute a term for f that contains f?

[Patrick Lutz]

which would lead to an infinite loop of substitutions

[Patrick Lutz]

no, actually that doesn't seem to be the issue

[Patrick Lutz]

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]

I get the same error where Lean says that the thing I want to substitute is not of the form x = t

[Thomas Browning]

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]

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]

we really want to actually replace f with a term that doesn't involve f

[Patrick Lutz]

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]

but that also didn't work

[Patrick Lutz]

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]

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]

No, I guess not.

[Patrick Lutz]

Oh, I think I sort of see why it's happening

[Patrick Lutz]

the problem is that I'm trying to substitute \phi for a term that depends on \phi

[Patrick Lutz]

but in the second example this dependence is hidden in a sneaky way

[Patrick Lutz]

the type of psi depends on phi

[Patrick Lutz]

and I'm trying to substitute a term that uses psi

[Patrick Lutz]

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]

Can you just rewrite instead?

[Patrick Lutz]

instead of subst?

[Kevin Buzzard]

Yeah, subst is just rewrite

[Patrick Lutz]

Lean tells me "motive is not type correct"

[Kevin Buzzard]

But rewrite wouldn't mind changing x to f(x)

[Kevin Buzzard]

Try simp only this

[Patrick Lutz]

Lean tells me "invalid simplification lemma"

[Patrick Lutz]

assuming by h you meant this

[Kevin Buzzard]

Right

[Kevin Buzzard]

So was my example bad? It didn't capture this repetition of f?

[Patrick Lutz]

it didn't capture that the type of g depends on f I think

[Patrick Lutz]

in your example you can separate out the function

[Patrick Lutz]

and forget about the condition on g which is the only thing that depends on f

[Patrick Lutz]

maybe that's possible here too

[Patrick Lutz]

let me try

[Kevin Buzzard]

Failing that you can always go back to the same thread with a better example

[Kevin Buzzard]

It's just that saying "I have a problem on this branch of mathlib" is much less likely to get a response

[Patrick Lutz]

yeah, I think I might be able to come up with a better example

[Patrick Lutz]

like foo_map above but a little more complex

[Patrick Lutz]

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φ, 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]

we need something similar here: a way to get the raw function E -> K from psi I think

[Patrick Lutz]

but for some reason Lean complains at me if I try to do psi.to_fun

[Patrick Lutz]

because it can't remember that K is an L algebra??

[Patrick Lutz]

even when I use haveI to give it that instance

[Patrick Lutz]

okay, I think I've almost figured it out

[Patrick Lutz]

I just need to get Lean to let me write

have q : E -> K := psi.to_fun,

[Patrick Lutz]

which it won't let me do because it's very confused about K being an L-algebra??

[Patrick Lutz]

okay, I did it

[Patrick Lutz]

  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]

didn't realize I could use rintros that way

[Patrick Lutz]

the haveI is unnecessary btw

[Patrick Lutz]

although the sorries look a bit annoying

[Thomas Browning]

(deleted)

[Thomas Browning]

(deleted)

[Thomas Browning]

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]

the commutes' sorry is giving me trouble. I can prove it, but then subst breaks again!

[Thomas Browning]

wait what?

[Thomas Browning]

replacing sorry with a proof breaks that subst?

[Thomas Browning]

what's your proof?

[Patrick Lutz]

      λ x, by {simp *, rw ← f.commutes' x,
        exact h5 (algebra_map F L x),}

[Patrick Lutz]

actually the first simp is unnecessary

[Patrick Lutz]

wait, I think I can fix it

[Patrick Lutz]

  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]

woah

[Patrick Lutz]

  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]

golfed a little

[Thomas Browning]

so is the moral just: intro as much stuff as you can, and hopefully things will get de-tangled?

[Patrick Lutz]

I guess so

[Patrick Lutz]

at the level of raw functions the situation is basically the same as Kevin's example

[Patrick Lutz]

pushed

[Patrick Lutz]

https://github.com/leanprover-community/mathlib/commit/85fdd5f6a3b2cbff07e40a3f76b6d6408a07d39f :open_mouth:

[Thomas Browning]

there was another one too! https://github.com/leanprover-community/mathlib/commit/0c4f7deb1e2573484e3069e342f35eaabdef59cc

[Thomas Browning]

Couldn't figure out how to golf alg_hom_compose though

[Thomas Browning]

@Jordan Brown #4982

[Patrick Lutz]

we should've been faster I guess

[Patrick Lutz]

well, plenty of other PRs for us to do anyway

[Patrick Lutz]

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]

@Thomas Browning @Jordan Brown https://github.com/ImperialCollegeLondon/group-theory-game/blob/39b4e9c474490a4cf78bb023d44ff0ced3e07310/src/subgroup/basic.lean#L28

[Patrick Lutz]

bundled normal subgroups in an Imperial repo

[Patrick Lutz]

@Thomas Browning We don't currently have that if $[E : F]$ is finite then every element of $E$ is integral over $F$ right?

[Patrick Lutz]

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]

that might take more work though I guess

[Aaron Anderson]

Patrick Lutz said:

Thomas Browning We don't currently have that if $[E : F]$ is finite then every element of $E$ is integral over $F$ right?

This is mostly is_integral_of_noetherian, no?

[Thomas Browning]

Patrick Lutz said:

Thomas Browning We don't currently have that if $[E : F]$ is finite then every element of $E$ is integral over $F$ right?

@Patrick Lutz This might follow from results in the algebraic.lean file (namely: finite_dimensional implies algebraic, algebraic implies integral)

[Patrick Lutz]

Aaron Anderson said:

Patrick Lutz said:

Thomas Browning We don't currently have that if $[E : F]$ is finite then every element of $E$ is integral over $F$ right?

This is mostly is_integral_of_noetherian, no?

You're right. I just didn't know that theorem was in mathlib

[Patrick Lutz]

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]

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]

subgroup yes: by induction H^(n) <= G^(n)

[Patrick Lutz]

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]

at least it can't infer it automatically

[Thomas Browning]

sounds like you need a lift from subgroup (H : subgroup G) -> subgroup G

[Patrick Lutz]

I agree. Though right now I'm going the lazy way and working at the level of sets instead

[Patrick Lutz]

a little annoying though

[Patrick Lutz]

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

okay, it's finished

[Patrick Lutz]

though probably not very clean

[Patrick Lutz]

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 $G_1$ to $G_2$ then there is a surjection from $[G_1, G_1]$ to $[G_2, G_2]$

[Jordan Brown]

does anyone know why simp will not prove for me that bottom is less than or equal to top in a group

[Jordan Brown]

it seems like there are lemmas for bottom being a least element and top being a maximal element, both tagged with simp

[Thomas Browning]

it should just be a special case of "bot_le" or "le_top"

[Thomas Browning]

simp works for me: example : (⊥ : subgroup G) ≤ (⊤ : subgroup G) := by simp

[Jordan Brown]

okay, so my computer is just being weird

[Jordan Brown]

that's what I thought

[Patrick Lutz]

@Jordan Brown what happens when you try to use simp?

[Jordan Brown]

it just says that the tactic failed to simplify

[Patrick Lutz]

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]

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]

I guess the weird part is that simp is doing something different for Jordan than for Thomas and me

[Patrick Lutz]

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

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]

Surely bot_le and le_top have been in mathlib since forever though? Since they're just theorems about lattices or something

[Patrick Lutz]

and git blame shows that the complete_lattice instance for subgroup G was last touched 6 months ago

[Kevin Buzzard]

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]

There was some missing lemma which was accidentally dropped when subgroups were bundled.

[Johan Commelin]

I think it was the lemma that top (or bot) is normal

[Kevin Buzzard]

Aah, so this sounds like it is unlikely to have made a difference

[Thomas Browning]

@Patrick Lutz I've proved the theorem, modulo the induction lemma

[Patrick Lutz]

Nice! Tomorrow I'll think about proving the induction principle

[Thomas Browning]

@Patrick Lutz I actually just did it. There's a finset lemma at the top of adjoin.lean that is in #5087

[Thomas Browning]

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

yeah

[Kevin Buzzard]

convert key works for me

[Kevin Buzzard]

oh no I spoke too soon.

[Patrick Lutz]

yeah it says goals accomplished but then also says either deterministic timeout or excessive memory consumption

[Patrick Lutz]

it's done both to me now

[Kevin Buzzard]

key

[Kevin Buzzard]

goal

[Kevin Buzzard]

oh crap they are identical!

[Patrick Lutz]

well the problem seems to be entirely on the fintype.card (↥F⟮α⟯ ≃ₐ[F] ↥F⟮α⟯) side

[Patrick Lutz]

if I rearrange the order of rws that's the part that never works

[Patrick Lutz]

actually I'm not so sure

[Kevin Buzzard]

so in fact the problem is somewhere else.

[Patrick Lutz]

also why is it so slow?

[Kevin Buzzard]

because of the real problem

[Kevin Buzzard]

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]

the goals accomplished coexisting with deterministic timeout is pretty crazy

[Kevin Buzzard]

The problem is when Lean's kernel then tries to verify the proof which all the tactics have put together

[Kevin Buzzard]

It's not the exact key timing out, it's something else.

[Patrick Lutz]

so there's some extra goal hanging around which the infoview isn't showing you?

[Patrick Lutz]

because maybe Lean thinks it can be solved by the type inference engine or something?

[Patrick Lutz]

but which actually can't

[Kevin Buzzard]

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]

like a tactic that thinks it solved some goal but actually didn't?

[Kevin Buzzard]

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]

I think the problem is in one of the subproofs

[Patrick Lutz]

specifically the replace h_splits proof

[Patrick Lutz]

when I replace that with sorry everything works fine

[Kevin Buzzard]

Oh good catch!

[Patrick Lutz]

something to do with ext1 I think

[Kevin Buzzard]

Putting sorry after ext1 and it still compiles.

[Kevin Buzzard]

I think the problem is the exact (iso.symm.commutes x).symm line.

[Patrick Lutz]

how can exact cause a problem?

[Kevin Buzzard]

If you change it to convert then you get the timeout again.

[Patrick Lutz]

also when I replace ext1 with ext something funny happens

[Patrick Lutz]

I think Lean might be trying to prove that E = F(a)

[Kevin Buzzard]

⊢ ⇑(iso.symm) (⇑(algebra_map F E) x) = ⇑(iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E)) x

[Kevin Buzzard]

Lean is managing to prove this with refl and then the kernel seems to reject the proof.

[Patrick Lutz]

Yeah I tried rwing (iso.symm.commutes x).symm and got that goal

[Patrick Lutz]

which then simp hint and tidy couldn't figure out

[Patrick Lutz]

and refl works but causes the previous problems. So does exact rfl

[Kevin Buzzard]

unfold_coes seems to hang Lean

[Kevin Buzzard]

Maybe convert is being too clever.

[Patrick Lutz]

congrand refl and exact rfl all cause the same problem

[Patrick Lutz]

oh I misunderstood what you said

[Kevin Buzzard]

I've never seen unfold_coes hang Lean before.

[Kevin Buzzard]

This goal has somehow been corrupted. Perhaps by the convert.

[Kevin Buzzard]

Tactics can do that. They can literally make goals which don't make any sense.

[Patrick Lutz]

yeah I think you're right that the convert is probably to blame

[Kevin Buzzard]

So maybe it is the ext after all.

[Patrick Lutz]

lol

[Kevin Buzzard]

I don't know which

[Kevin Buzzard]

did you say you fiddled with the ext?

[Kevin Buzzard]

algebra_map F ↥F⟮α⟯ = iso.symm.to_alg_hom.to_ring_hom.comp (algebra_map F E)

[Kevin Buzzard]

What does that mean mathematically?

[Patrick Lutz]

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]

I see. iso is some isomorphism $F(\alpha)\to E$

[Patrick Lutz]

yes, established earlier in the proof

[Kevin Buzzard]

so the goal seems to make sense mathematically, and ext certainly seems like the next step.

[Patrick Lutz]

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]

even though it works after the convert for the same goal in the original proof

[Patrick Lutz]

so I think convert is probably the culprit

[Kevin Buzzard]

show_term {ext1} says it's applying ring_hom.ext

[Kevin Buzzard]

     apply ring_hom.ext,
     intro x,
     unfold_coes,

works after the convert, so that's a way of unfolding the coes

[Patrick Lutz]

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]

but now rw (iso.symm.commutes x).symm, is failing for me.

[Patrick Lutz]

hmm it works for me but then causes the same problems as before

[Patrick Lutz]

so now I think you're right and ext really is the problem

[Kevin Buzzard]

lol

[Kevin Buzzard]

I was about to say "I think you're right, the problem must be with the convert

[Patrick Lutz]

but there's no more convert anywhere

[Patrick Lutz]

this proof works fine

  cases field.exists_primitive_element h.1 with α hα,
  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),
    {
      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]

this proof has all the same problems as the original

  cases field.exists_primitive_element h.1 with α hα,
  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),
    {
      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]

It's just apply ring_hom.ext.

[Patrick Lutz]

yeah but there's literally no more converts in the proof

[Kevin Buzzard]

annoyingly, extract_goal doesn't give you a failing example.

[Patrick Lutz]

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]

maybe it's the refl that's the problem??

[Kevin Buzzard]

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)
  (hα : 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]

I used extract_goal to get exactly what we thought the problem was.

[Patrick Lutz]

this is bizarre

[Kevin Buzzard]

If we could minimise we could ask a much better question.

[Patrick Lutz]

yeah

[Patrick Lutz]

I just ran into a weird thing where dsimp does something and squeeze_dsimp suggests dsimp only but dsimp only fails

[Kevin Buzzard]

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 α hα,
  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]

ohh I didn't try that

[Kevin Buzzard]

I think this is just an indication that we're looking in the wrong place.

[Patrick Lutz]

I tried putting sorry in both

[Patrick Lutz]

yeah I agree

[Patrick Lutz]

so a sorry anywhere in the proof makes it work??

[Kevin Buzzard]

no

[Patrick Lutz]

this works:

lemma foo [finite_dimensional F E] [h : is_galois F E] (α : E) (hα : 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 α hα,
  have iso := foo F E α hα,
  -- 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]

so I think iso is somehow causing problems

[Patrick Lutz]

I conjecture that replacing iso with a term mode proof will fix the problems

[Patrick Lutz]

it fails again when I fill in foo with a tactic mode proof

[Kevin Buzzard]

Your lemma should be a def

[Kevin Buzzard]

let iso : F⟮α⟯ ≃ₐ[F] E,

[Patrick Lutz]

ohh

[Kevin Buzzard]

unfortunately this doesn't fix it :-(

[Kevin Buzzard]

You shouldn't be proving this in tactic mode

[Patrick Lutz]

yeah, see my conjecture

[Kevin Buzzard]

This is the problem

[Kevin Buzzard]

I mean, this is _a_ problem

[Thomas Browning]

Just saw this thread. Is the consensus that tactic-mode iso is likely the only culprit?

[Kevin Buzzard]

The proof of iso should be to beef up h\alpha to an isomorphism and then to apply transitivity of isomorphisms.

[Kevin Buzzard]

Lean is getting stuck on the eq.rec which the rw is inserting.

[Kevin Buzzard]

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]

how can I say very concisely in Lean that if A = B then A \equiv B?

[Patrick Lutz]

I can't find any lemma to that effect in mathlib

[Patrick Lutz]

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]

That's a definition, not a lemma.

[Patrick Lutz]

well I can't find that definition either

[Kevin Buzzard]

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

Not the one you want, but it looks like we're looking for of_eq

[Thomas Browning]

If the algebra version is not in mathlib, we can just add it, right?

[Kevin Buzzard]

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]

There's no alg_equiv.comp?

[Kevin Buzzard]

oh it's trans

[Patrick Lutz]

yeah but I'm having a hard time using it

[Patrick Lutz]

the types of things don't quite match up

[Kevin Buzzard]

How do I turn an intermediate_field into a subalgebra?

[Kevin Buzzard]

h\alpha is an equality of intermediate_fields

[Patrick Lutz]

.to_subalgebra

[Kevin Buzzard]

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]

lol

[Kevin Buzzard]

So perhaps we're getting closer to the heart of the problem

[Kevin Buzzard]

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]

okay, good night

[Patrick Lutz]

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) (hα : 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]

Try convert bar _

[Kevin Buzzard]

although again you shouldn't be using convert in a definition.

[Patrick Lutz]

also this gives me a very weird error

    have := bar hα,

[Patrick Lutz]

type mismatch at application
  bar hα
term
  hα
has type
  F⟮α⟯ = ⊤
but is expected to have type
  ?m_1 = ?m_2

[Kevin Buzzard]

And you shouldn't be sorrying the definition of bar. Sorrying definitions can lead to trouble.

[Patrick Lutz]

I'm just trying to figure out what's going on

[Kevin Buzzard]

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]

But I do introduce an eq.subst in the definition, which is already a bit hairy.

[Kevin Buzzard]

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]

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]

oh I see

[Kevin Buzzard]

I cannot see how to avoid eq.subst or eq.rec here.

[Kevin Buzzard]

Why not just ask how to construct F⟮α⟯ ≃ₐ[F] E from F⟮α⟯ = ⊤? That sounds like a reasonable question.

[Kevin Buzzard]

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]

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]

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]

Yeah I think I can figure out how to ask a reasonable version of this question

[Kevin Buzzard]

We had exactly the same sort of problem, a proof which should have been refl but was instead a big time-out.

[Kevin Buzzard]

Sorry I couldn't solve it. I'm still learning when it comes to technical issues like this.

[Patrick Lutz]

lol no problem. I think we understand much better now what's going on

[Kevin Buzzard]

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 α hα,
  have hα' : F⟮α⟯.to_subalgebra = ⊤, rw hα, 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]

this compiles and the only sorrys are props.

[Kevin Buzzard]

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 α hα,
  have hα' : F⟮α⟯.to_subalgebra = ⊤, rw hα, 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]

oh nice

[Kevin Buzzard]

I bet if you fill in those sorries it will compile.

[Kevin Buzzard]

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]

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 α hα,
  let iso : F⟮α⟯ ≃ₐ[F] E := {
    to_fun := λ e, e.1,
  inv_fun := λ e, ⟨e, begin rw hα, 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]

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 α hα,
  let iso : F⟮α⟯ ≃ₐ[F] E := {
    to_fun := λ e, e.1,
  inv_fun := λ e, ⟨e, begin rw hα, 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]

:D

[Kevin Buzzard]

It's amazing how stopping for 5 minutes and doing something else can inspire you.

[Kevin Buzzard]

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]

yeah I also just arrived at that proof

[Patrick Lutz]

the intermediate_field.mem_top was a little tricky

[Kevin Buzzard]

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]

unfortunately I can no longer go to Euclid for dinner :'(

[Kevin Buzzard]

Patrick Lutz said:

yeah I also just arrived at that proof

Yeah the entire process was collaborative.

[Patrick Lutz]

or Evans

[Kevin Buzzard]

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]

I can't figure out why trivial didn't do the intermediate_field.mem_top thing. I also got stuck there.

[Patrick Lutz]

I've heard so many stories of the days of usenet

[Patrick Lutz]

but I was born at the end of the eternal september

[Kevin Buzzard]

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]

But you have to put this into context -- my supervisor couldn't even have that.

[Kevin Buzzard]

s.m.r. gave you access to experts. It was a game-changer.

[Kevin Buzzard]

Before email you asked your advisor and if they couldn't help you were _stuck_.

[Kevin Buzzard]

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]

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

Then mathoverflow came, and now we have things like this.

[Kevin Buzzard]

In my academic lifetime I've seen several revolutions. And you kids just think it's all normal :-)

[Kevin Buzzard]

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]

She's engrossed in something else in the next room :-)

[Kevin Buzzard]

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]

lemma mem_top {x : E} : x ∈ (⊤ : intermediate_field F E) :=
subfield.subset_closure $ or.inr trivial

o_O

[Kevin Buzzard]

I think top : intermediate_field F E must be defined as the closure of univ!

[Patrick Lutz]

yeah I guess so

[Patrick Lutz]

I think the problem might be that the lattice structure comes from a galois insertion between adjoin and the forgetful functor

[Patrick Lutz]

but I don't really know what I'm talking about

[Patrick Lutz]

so \top in intermediate fields is really something like F adjoin (\top in sets)

[Patrick Lutz]

and adjoin is defined using subfield.subset_closure

[Kevin Buzzard]

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]

wait, isn't that basically what I just said?

[Kevin Buzzard]

Yes, but I hadn't read what you were typing, I was too busy typing it myself :D

[Patrick Lutz]

lol, happens to me sometimes too

[Kevin Buzzard]

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]

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]

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]

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]

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]

Congratulations!!! You did it!

[Johan Commelin]

I hope the reviewing process wasn't too much of a pain.

[Johan Commelin]

But you can be proud of the end result!

[Thomas Browning]

It's great to have this PRed. Thanks so much to you and @Anne Baanen for the help!

[Kevin Buzzard]

Yes this is a great step forward

[Johan Commelin]

Are you going to talk about this at LT2021?

[Kevin Buzzard]

It's been something I've been wanting to see in mathlib for years

[Kevin Buzzard]

Not least because I was teaching it when I got into lean :-)

[Johan Commelin]

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]

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]

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]

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]

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]

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]

and

general_nth_commutator : Π (G : Type u) [_inst_1 : group G], subgroup G → ℕ → subgroup G

[Jordan Brown]

so I'm not quite sure what the issue is @Patrick Lutz @Thomas Browning

[Patrick Lutz]

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]

Like why are you using the top subgroup of H rather than just H itself (considered as a group)

[Patrick Lutz]

also btw G and H are probably already declared in the file and you don't need to declare them again

[Patrick Lutz]

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]

but then Lean expects the other side to be a subgroup of H as well, which it's not

[Patrick Lutz]

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]

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]

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]

but yes, the restatement fixes the problem; I don't know why I forgot how the arguments to nth_commutator work

[Jordan Brown]

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]

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]

It also might be helpful to prove that if (K : subgroup H) then K.lift \leq H

[Patrick Lutz]

which I didn't do either

[Patrick Lutz]

the proofs should be somewhat similar to mem_lift or eq_bot_iff_lift_eq_bot

[Patrick Lutz]

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]

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]

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

I am fully intending on writing up the formalisation of schemes and I haven't started yet either

[Patrick Lutz]

@Thomas Browning Does mathlib know about the compositum of two intermediate_fields?

[Patrick Lutz]

I think probably not

[Thomas Browning]

I think it must, because of the lattice stuff proved in adjoin.lean

[Patrick Lutz]

Thomas Browning said:

I think it must, because of the lattice stuff proved in adjoin.lean

ohh, you must be right

[Patrick Lutz]

so the compositum of L and K is probably adjoin F (K \cup L)?

[Patrick Lutz]

if you unroll the definitions?

[Patrick Lutz]

@Jordan Brown https://github.com/leanprover-community/mathlib/commit/b26d7940d757038d9e61db257f017e0a952a8bcb

[Thomas Browning]

I guess so, but it's also probably got specific notation (join or meet?)

[Patrick Lutz]

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]

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]

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]

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. $S_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 $F^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 $F^t$ is galois over F, has solvable galois group and contains a
11. There is an irreducible polynomial (over $\mathbb{Q}$ maybe) whose galois group is $S_5$
12. Let $a$ be a root of this polynomial in $\mathbb{C}$. Suppose solvable_by_radicals a is nonempty. Let t be a term. Then $F^t$ contains a and is galois over F hence contains the splitting field of the minimal polynomial of a. The galois group of $F^t$ is solvable and contains the galois group of the polynomial as a subgroup hence that group ($S_5$) is also solvable.
13. Contradiction.

[Patrick Lutz]

All the parts look doable at this point, though steps 7 and 11 look annoying

[Johan Commelin]

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

Pro tip: If you format the points using - [ ] then github automatically turns them into checkboxes

[Patrick Lutz]

https://github.com/leanprover-community/mathlib/issues/5258

[Patrick Lutz]

@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 $F^t$ is galois over F. But is that even true? I actually no longer think so. But maybe it's not necessary?

[Patrick Lutz]

But I think we do want $F^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]

I guess maybe we should modify the definition of $F^t$ to make sure it is Galois?

[Patrick Lutz]

we never defined Galois closure right?

[Thomas Browning]

We could prove inductively on t that F^t is Galois over F

[Thomas Browning]

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]

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 $F^t$ right? Edit: no, actually see the next comment

[Patrick Lutz]

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]

that's the whole problem right?

[Thomas Browning]

ah, good point

[Thomas Browning]

let me look up the proof in D&F

[Patrick Lutz]

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]

yeah, looks like it

[Thomas Browning]

we might be able to avoid Galois closure though

[Thomas Browning]

rather than just adjoining the nth roots of a, can you just also adjoin the nth roots of any conjugate of a?

[Patrick Lutz]

Patrick Lutz said:

that's the whole problem right?

Actually an example I found on math SE is helpful: $\mathbb{Q}(\sqrt{2})$ is galois over $\mathbb{Q}$ and $\mathbb{Q}(\sqrt{1 + \sqrt{2}})$ is galois over $\mathbb{Q}(\sqrt{2})$ but not over $\mathbb{Q}$. And it is exactly the field that would be constructed as $F^t$

[Patrick Lutz]

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]

but this avoids talking about Galois closure, just look at the orbit of a under the Galois group that we already have

[Patrick Lutz]

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]

ah, yes

[Thomas Browning]

I guess we would have to use an ambient Galois extension

[Patrick Lutz]

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]

we don't, but it might follow from the (L/F Galois iff subgroup is normal)

[Thomas Browning]

which we'll prove at some point

[Patrick Lutz]

Thomas Browning said:

I guess we would have to use an ambient Galois extension

or algebraically closed field

[Thomas Browning]

but don't we need the extension E/F to be finite in order to use our Galois theory?

[Patrick Lutz]

hmm, well maybe not?

[Patrick Lutz]

it would be nice to be able to eventually state things for $\mathbb{C}$ over $\mathbb{Q}$

[Thomas Browning]

also, I'm wondering whether it might be easier to mostly work on the subgroup side

[Thomas Browning]

because then compositum is just intersection

[Patrick Lutz]

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]

this business about "adjoining all of the Galois conjugates" is just taking the intersections of the conjugates of a subgroup

[Patrick Lutz]

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]

Like we still need to know that we are getting a galois extension

[Thomas Browning]

Actually, I think working with fields is fine

[Thomas Browning]

Can we work inside of the splitting field of p(x)*(x^(big)-1) ?

[Thomas Browning]

Then we can use the Galois correspondence.

[Thomas Browning]

Actually, would it make sense to show that Gal(splitting(p(x) * (x^(big) - 1) / Q) is solvable?

[Patrick Lutz]

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]

I also just think it would be nice to be able to say stuff about $\mathbb{C}/\mathbb{Q}$

[Thomas Browning]

That's true

[Patrick Lutz]

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]

If we ever need a finite Galois closure, we could use PET + splitting field of that polynomial

[Patrick Lutz]

because a lot of times we are just dealing with $F^t/F$ which is finite dimensional. There's only a few places we need to talk about the ambient field

[Thomas Browning]

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]

is that true?

[Patrick Lutz]

wait, do you mean containing K/F?

[Patrick Lutz]

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]

Yes, I meant K/F

[Thomas Browning]

To take a compositum, do we need to be working inside an ambient field?

[Thomas Browning]

I would assume so

[Kevin Buzzard]

When I lectured this I defined algebraic closures early on and would always work in the alg closure of the base field

[Kevin Buzzard]

It just made things much easier

[Kevin Buzzard]

I'm not sure if it makes formalisation easier though

[Kevin Buzzard]

The other approach is to define normal closure of a finite extension

[Kevin Buzzard]

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]

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]

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]

There's a notion of "solvable" for a finite separable extension, which is "Galois closure is solvable"

[Patrick Lutz]

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]

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]

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]

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]

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]

Adjoining n'th root is solvable

[Kevin Buzzard]

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]

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]

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]

I don't know if you need to go that far though. The proof isn't hard

[Patrick Lutz]

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]

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]

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]

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

sure

[Patrick Lutz]

@Thomas Browning just an fyi, I'm speaking at JMM on January 7th, which might conflict with Lean Together 2021

[Thomas Browning]

thanks for the heads up

[Patrick Lutz]

Okay, I have a new idea for the abel-ruffini strategy

[Patrick Lutz]

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]

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]

Ooh, I really like this approach of using the splitting field of the minimal polynomial of the solvable_by_radicals element

[Patrick Lutz]

yeah, the hairy part will basically all be in part 2.2 I think

[Patrick Lutz]

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]

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]

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]

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 $\mathbb{Z}/n\mathbb{Z}$

[Patrick Lutz]

so I guess we can maybe show that the galois group embeds into the galois group of p over F times $\mathbb{Z}/n\mathbb{Z}$

[Patrick Lutz]

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]

wait, now I'm starting to doubt some of the stuff I'm saying

[Patrick Lutz]

I think the galois group of $p(X^n)$ may be a little complicated to describe

[Thomas Browning]

well, it should still be true that p(X^n) has solvable Galois group, right?

[Patrick Lutz]

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]

but I have a new idea

[Patrick Lutz]

wait, no I don't

[Patrick Lutz]

I'm having trouble finding anything describing the galois group of a composition of polynomials

[Patrick Lutz]

but it's maybe a wreath product

[Patrick Lutz]

well, maybe we can express this using short exact sequences instead

[Thomas Browning]

You need to show that Gal(split(p(X^n))/split(p(X))) is solvable

[Patrick Lutz]

Thomas Browning said:

You need to show that Gal(split(p(X^n))/split(p(X))) is solvable

yeah, that's true

[Patrick Lutz]

which should somehow follow from adding roots of unity and then adding roots one at a time

[Patrick Lutz]

I guess

[Patrick Lutz]

maybe just an ugly induction

[Patrick Lutz]

Okay, I think I now understand better what's going on. The key is that if $F = K_0 \le K_1 \ldots \le K_n = E$ is a sequence of field extensions such that $E$ is Galois over $F$ and each $K_{i + 1}$ is Galois over $K_i$ with solvable Galois group then the Galois group of $E$ over $F$ is solvable. The tricky thing is that you prove this by backwards induction on $i$. I.e. prove by induction on $j$ that the Galois group of $E$ over $K_{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(X^n)(X^n - 1)$ is contained in the field you get by starting with $F$, going to the splitting field of $p$, adjoining roots of unity and then adjoining roots of equations of the form $X^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,$ but that doesn't matter.

[Kevin Buzzard]

If you define this generalised solvable to mean "Galois closure is solvable" then this follows from transitivity of generalised solvable

[Patrick Lutz]

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]

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]

How about L/K is presolvable if there exists E/L Galois over K with solvable Galois group?

[Patrick Lutz]

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 $F \le L \le K \le E$ where $E$ is algebraically closed or something and $L/F$ and $K/L$ are both Galois. How easy is it to show that there is a galois extension of $F$ that contains $L$ and which is solvable?

[Kenny Lau]

as easy as the maths proof

[Patrick Lutz]

Kenny Lau said:

as easy as the maths proof

which proof?

[Kenny Lau]

as in, it will be equally as easy or as hard as the maths proof, if there is one.

[Kenny Lau]

or, phrased in another way: do you have the maths proof?

[Patrick Lutz]

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]

the proof of abel-ruffini that I outlined above proves basically a special case of this where $K/L$ has a special form (adjoining a root of $X^n - a$ for some $a$ in $K$)

[Kevin Buzzard]

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]

the group-theoretic version of the argument is: if $\Gamma$ is a big ambient group, and if $A$ is a normal subgroup with $\Gamma/A$ solvable and if $B$ is a normal subgroup of $A$ with $A/B$ solvable, then conjugating by all the elements of $\Gamma$ gives you a bunch of subgroups $B'=gBg^{-1}$ with $A/B'$ solvable (because isomorphic to $A/B$), so if $C$ is the intersection of the $B'$ then $A/C$ is solvable and hence $\Gamma/C$ is solvable.

[Thomas Browning]

#5342 #5343 #5344 #5345 #5346 #5347 and then we'll have separable splitting field implies galois

[Patrick Lutz]

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]

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]

A couple of things on the list have already been done I think

[Patrick Lutz]

though for some of them, we may need a slightly different version

[Patrick Lutz]

Also, maybe obvious, but the different items on the list are definitely not all of equal difficulty

[Kevin Buzzard]

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]

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]

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]

The one part which isn't clear to me is how this backwards induction works in the last but one bullet point

[Kevin Buzzard]

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]

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]

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]

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]

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 $\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]

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]

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]

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]

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]

also I don't think you need to show $K_j$ is galois and solvable over $K_i$ for all $i$. Just that $K_{i + 1}$ is galois and solvable over $K_i$. And that $K_m$ is galois over each $K_i$ which comes from galois_tower_top or something like that.

[Patrick Lutz]

but yes, I agree that lemmas are needed.

[Patrick Lutz]

I just wasn't sure which ones are needed yet.

[Patrick Lutz]

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]

@Jordan Brown FWI, we won't be meeting tomorrow

[Thomas Browning]

@Patrick Lutz Have you been following this thread: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/

[Patrick Lutz]

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]

I guess I never really fully understood the significance of subsingleton in the first place

[Patrick Lutz]

and I don't know why this PR would break things

[Thomas Browning]

It seems like simp is not handling subsingleton instances correctly

[Patrick Lutz]

yeah, but I don't know why that would be

[Patrick Lutz]

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]

Was this lemma for talking about the trivial group?

[Patrick Lutz]

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]

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]

I'm still not sure what the best way to talk about the trivial group is

[Patrick Lutz]

if an algebra is trivial then its automorphism group is trivial

[Thomas Browning]

bot = top doesn't seem like the best way

[Patrick Lutz]

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]

Thomas Browning said:

bot = top doesn't seem like the best way

fair enough

[Thomas Browning]

Is the notion of an algebra being trivial discussed in mathlib?

[Patrick Lutz]

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]

which is one way of saying an algebra is trivial

[Patrick Lutz]

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]

On the plus side, mathlib might get a major performance increased when this is fixed

[Thomas Browning]

@Patrick Lutz Surjectivity is coming: #5960

[Thomas Browning]

@Patrick Lutz I've merged the surjectivity stuff into the abel-ruffini branch, and cleaned up the compositum proof a bit

[Thomas Browning]

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]

@Patrick Lutz

[Patrick Lutz]

You may be right. Let me spend a bit more time thinking about it in the morning.

[Patrick Lutz]

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 $a^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 $a$ divides $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]

@Thomas Browning

[Thomas Browning]

I like this, it sidesteps a lot of the issues that I was worried about

[Thomas Browning]

in particular, it's nice that everything is a splitting field over F

[Patrick Lutz]

I kind of feel like we even discussed this approach at some point

[Patrick Lutz]

but I either lost the paper where I wrote it down or I didn't write it down

[Thomas Browning]

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]

that seems like one of the less bad parts to me

[Patrick Lutz]

because you can evaluate things in E

[Patrick Lutz]

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]

Actually, here's a better way of stating (3)

[Patrick Lutz]

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]

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]

That last one shouldn't be bad at all

[Patrick Lutz]

yeah

[Patrick Lutz]

(4) looks a bit tricky

[Thomas Browning]

By the way, are we treating is_solvable as an instance or a ordinary hypothesis?

[Patrick Lutz]

it's a type class

[Patrick Lutz]

so it should be an instance by default but sometimes it can't be I guess

[Patrick Lutz]

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]

so should solvable_prod be an instance?

[Patrick Lutz]

Thomas Browning said:

so should solvable_prod be an instance?

yeah, is it not?

[Thomas Browning]

lemma solvable_prod {G' : Type*} [group G'] (h : is_solvable G) (h' : is_solvable G') :
  is_solvable (G × G') :=

[Patrick Lutz]

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]

but yeah it should be I think

[Patrick Lutz]

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]

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]

@Patrick Lutz Does this look true to you?
example : p.splits (algebra_map F (p.comp q).splitting_field) :=

[Thomas Browning]

(the idea is that applying q to the roots of p.comp q gives you roots of p)

[Thomas Browning]

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]

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]

but we don't actually need to construct a map from p.splitting_field to (p.comp (X^n)).splitting_field

[Patrick Lutz]

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]

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]

oh, wait, no it does

[Patrick Lutz]

because b is a root of p.comp q

[Thomas Browning]

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]

I guess it is a nice thing to prove. But the proof I gave might be a bit annoying in Lean

[Patrick Lutz]

although maybe actually not so bad

[Kevin Buzzard]

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]

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]

@Patrick Lutz I proved it:
example (hq : q.nat_degree ≠ 0) : p.splits (algebra_map F (p.comp q).splitting_field) :=

[Thomas Browning]

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

now the real fun begins!

[Kevin Buzzard]

You can embed the Galois group into a semidirect product of abelian groups

[Kevin Buzzard]

So you can write down a map to an abelian group with abelian kernel

[Thomas Browning]

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]

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]

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]

They wrote a paper for Exp.Math. right?

[Kevin Buzzard]

Oh maybe!

[Patrick Lutz]

@Thomas Browning I think I can't make it to the meeting tomorrow (just for this week). Sorry for the short notice.

[Thomas Browning]

No worries. Thanks for letting me know.

[Thomas Browning]

@Jordan Brown Do you want to meet this week, or skip until next week?

[Jordan Brown]

I think skipping until next week is fine -- I don't have anything I think we desperately need to talk about

[Thomas Browning]

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

Did you guys look at the Coq work? Do they set things up substantially differently?

[Thomas Browning]

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]

All the sorries are gone! (for SBR implies solvable)

[Thomas Browning]

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