Trimming dependencies on `SplittingField`

Stream: mathlib4

[Anne Baanen]

@Alain Chavarri Villarello has been doing some nice work in Lean 3 that we might want to start porting to Lean 4, but it depends transitively on splitting fields. We definitely need ring_theory.integrally_closed which imports splitting_field, and probably also ring_theory.ideal.norm. Any objections to me splitting these files to remove the splitting field dependency?

[Riccardo Brasca]

I am also having a look at splitting that remove dependencies on splitting_field (for example in #19130). I think they're very good, especially if they make sense mathematically.

[Anne Baanen]

From your "for example" I assume you are working on more than just #19130. I couldn't find any open PRs related to this, so are they already merged?

[Anne Baanen]

Anyway, I'll get started with integrally_closed now, that certainly shouldn't know about splitting fields...

[Riccardo Brasca]

I am porting the file for the moment, I plan to had another look at mathlib3 later.

[Riccardo Brasca]

I had a quick look at integrally closed, and the only problem is docs#integral_closure.mem_lifts_of_monic_of_dvd_map

[Riccardo Brasca]

The theorem really needs splitting_field

[Riccardo Brasca]

Mathematically it can reasonably be moved to something about Gauss' Lemma (it is in the same spirit)

[Anne Baanen]

It is only used in eq_map_mul_C_of_dvd and that is only used in gauss_lemma.lean, so I propose to move those two to that file.

[Riccardo Brasca]

Nice, this confirms my intuition that this is a "Gauss lemma style" result, so it can definitely be moved there.

[Ruben Van de Velde]

Probably you're already further along, but this is what I was looking at a while ago: https://github.com/leanprover-community/mathlib/pull/new/split-split

[Anne Baanen]

Ah, I am keeping splitting_field.lean intact and instead split the dependencies, so hopefully we can be parallel here :)

[Riccardo Brasca]

Something else we can do is create a folder ring_theory/root_of_unity with files basic and minpoly (the current ring_theory/root_of_unity file is almost 1200 lines long) in such a way that ring_theory/root_of_unity/basic would not depend on splitting fields.

[Riccardo Brasca]

If you think it is reasonable I can do it

[Riccardo Brasca]

#19144

[Heather Macbeth]

@Riccardo Brasca splitting_field is still showing as having 92 dependencies dependents at #port-status; do you know if there is a second path importing splitting_field in most of roots_of_unity's dependents, or if #port-status isn't updating?

[Riccardo Brasca]

roots_of_unity.basic should be ready to port

[Riccardo Brasca]

The rest I think really depends on splitting fileds

[Johan Commelin]

I don't see the 92 dependencies...

[Johan Commelin]

Oooh, sorry, you meant dependents, I guess.

[Yaël Dillies]

"dependents" is what Heather meant, I guess?

[Johan Commelin]

You can see here https://github.com/leanprover-community/mathlib-port-status/actions/workflows/pages.yml that #port-status last updated 26 mins ago

[Johan Commelin]

So the next version should start building in ~ 3 mins

[Heather Macbeth]

Riccardo Brasca said:

The rest I think really depends on splitting fileds

I see, so it's really only roots_of_unity and not any of its dependents which are made port-able by the split?

[Riccardo Brasca]

For example ring_theory.polynomial.cyclotomic.basic now doesn't depends on splitting fields. I am afraid this is the only one.

[Chris Hughes]

Also worth noting that field_theory.adjoin only depends on is_splitting_field and not the existence of a splitting field.

[Michael Stoll]

Why does ring_theory.polynomial.gauss_lemma import field_theory.splitting_field?
On its face, Gauß' lemma should not require splitting fields. (I didn't check what is actually done in the file, though.)

[Ruben Van de Velde]

I suggest you look at the code; that's what anyone else would need to do to answer your question anyway

[Michael Stoll]

OK; I see that the very first lemma uses the splitting field of g to show that if g : K[X] (monic) divides f : R[X] (monic), its coefficients are integral over R. It doesn't feel necessary to use the splitting field here, but I don't have a "better" proof right now.

[Michael Stoll]

(This is the only lemma whose proof depends on splitting fields (but many other results depend on this lemma); the only other complaint I got after removing the splitting fields import can be fixed by importing field_theory.minpoly.basic.)

[Michael Stoll]

The idea of the proof seems to be to say that the roots of g are also roots of f, which are integral over R as witnessed by f, so the coefficients of g, which are polynomials with integral coefficients in the roots of g, are themselves integral over R.

[Michael Stoll]

A possible alternative route could be to show that the $n$ th coefficients of all monic divisors of degree $d$ of f satisfy a polynomial whose coefficients are polynomials with integral coefficients in the coefficients of f, via the theory of symmetric polynomials. This may be somewhat painful, though...

[Michael Stoll]

(The reason I've been looking at this is that uncoupling gauss_lemmafrom splitting_field would open up for porting some more files on the way to quadratic_reciprocity. But there is still a part of the graph that depends on splitting_field via a different route.)

[Riccardo Brasca]

Well at some point we will need splitting fields. We should not spend a lot of time trying to avoid it, but rather to fixing it (I am still trying to understand what the problem really is, and I think it goes back to adjoin root)

[Michael Stoll]

Agreed. I was just wondering about this non-obvious dependence.

[Riccardo Brasca]

Chris Hughes said:

Also worth noting that field_theory.adjoin only depends on is_splitting_field and not the existence of a splitting field.

I thought a little bit more about this observation and there is actually a split that maybe worth: we can separate is_splitting_field from splitting_field, and unblock field_theory.adjoin, field_theory.normal, field_theory.fixed and maybe even field_theory.galois (I didn't check carefully). I gave it a try in #19154

[Riccardo Brasca]

If people think this is a sensible thing to do I can finalize the splitting (probably creating a folder splitting_field with files is_splitting_field and existence, or something like that)

[Eric Rodriguez]

I'd prefer splitting_field.construction

[Riccardo Brasca]

Is there a way of seeing the dependents of a file? I see that for splitting_field they're 92 but I don't see a list.

[Riccardo Brasca]

Well, it's not that important, renaming splitting_field will force me to fix the import line

[Michael Stoll]

BTW, I have found a proof that shows that the coefficients of $g$ are integral over $\mathbb{Z}[f_1,\ldots,f_n]$, where $f = X^n + f_1 X^{n-1} + \dots + f_n$, without using splitting fields. (This would imply a stronger version of the lemma, without the assumption that K is a field.) It is, however, fairly involved and combinatorial, and so maybe it's not really worth while trying to formalize it.

The idea is that when $g = X^k + g_1 X^{k-1} + \dots + g_k$ divides $f$, the the matrix (how to get LaTeX displays here?) whose first row is $(1 \; f_1 \; f_2 \; \cdots \; f_n)$ and whose $n-k+1$ further rows are $(0 \cdots 0 \; 1 \; g_1 \; \cdots \; g_k \; 0 \cdots 0)$ (with $0, 1, ..., n-k$ zeros in front) does not have full rank. Picking suitable minors, one can show that one can express all monomials of the $g_j$ of degree $n-k+1$ over $\mathbb{Z}[f_1, \ldots, f_n]$ in terms of monomials of smaller degree...

[Riccardo Brasca]

Riccardo Brasca said:

Chris Hughes said:

Also worth noting that field_theory.adjoin only depends on is_splitting_field and not the existence of a splitting field.

I thought a little bit more about this observation and there is actually a split that maybe worth: we can separate is_splitting_field from splitting_field, and unblock field_theory.adjoin, field_theory.normal, field_theory.fixed and maybe even field_theory.galois (I didn't check carefully). I gave it a try in #19154

OK, this is not so simple, there are two declarations in field_theory.normal that use splitting_field: docs#normal.of_is_splitting_field and docs#polynomial.splitting_field.normal. I can probably remove the first dependency (it is used only in the proof), but of course not the second one. Maybe the simplest thing to do is to make the new file field_theory.splitting_field.construction import field_theory.normal and putting the result there.

[Kevin Buzzard]

@Michael Stoll click on the "?" under the box for writing posts to answer most questions of the form "how do I do X in a Zulip post". It's ```math in this case.

[Kevin Buzzard]

Back to the point, I guess it feels a little bit unnatural to me to separate splitting_field and is_splitting_field. Are we only proposing doing this so we can port stuff in a different order?

[Riccardo Brasca]

I am not sure it is the best thing to do, but I see two reasonable advantages:

• currently to do a lot of basic Galois theory, mathlib needs to know the existence of splitting fields. This seems to me a little unnatural, for example we cannot even say that a given (finite) field extension is normal without importing the file that construct the splitting field.
• All the problems of splitting_fields are (probably) in the construction, not in the characteristic predicate is_splitting_field.

Of course the first point is not completely solved by the splitting I am proposing, since to speak about normal extensions we still need the characteristic predicate.

[Kevin Buzzard]

I have taught Galois theory by doing existence of algebraic closure on day 1 and postponing splitting fields to much later.

[Riccardo Brasca]

Currently our construction of algebraic closure depends on existence of splitting fields.

[Kevin Buzzard]

Is the problem (a) splitting fields are slow or (b) splitting field files need to be reorganised?

[Kevin Buzzard]

I will try and find some time today to work on (a).

[Riccardo Brasca]

(a) is surely more important than (b) (sooner or later we will need to address it). What I am proposing just postpone the moment all algebraic number theory is blocked by splitting fields. Note that I am against moving lemmas around just to avoid splitting fields, the point is that this particular splitting makes some sense mathematically.

[Riccardo Brasca]

#19154 builds locally. I think it unblocks a non negligible amount of files to be ported. This assuming that field_theory.splitting_field.is_splitting_field can be ported without troubles.

[Michael Stoll]

Hm, thanks. I tried ```latex, but it produced a LaTeX code listing...
(This is in reply to @Kevin Buzzard's remark.)

[Johan Commelin]

That PR is now merged and the split files are listed in #port-status. But I guess we still need to wait for mathport output?

[Ruben Van de Velde]

Johan Commelin said:

That PR is now merged and the split files are listed in #port-status. But I guess we still need to wait for mathport output?

We do, yeah