!4#5074 FieldTheory.IsAlgClosed.AlgebraicClosure

Stream: mathlib4

[Riccardo Brasca]

The next big boss seems to be !4#5074 (at least it is short...). In particular I am stuck with Step.isIntegral, that timeouts. I have an horribly slow proof, that works with set_option maxHeartbeats 5000000 in .

I think that one of the culprit is the use of RingHom.toAlgebra, but I am not sure.

[Riccardo Brasca]

I am currently looking for a slightly different proof

[Sebastien Gouezel]

Not directly related to the PR, but I can see that AlgebraicClosure is not marked as irreducible, which means that the gory details of the construction are available to the kernel whenever one uses it. Wouldn't it make sense to make it irreducible?

[Chris Hughes]

There are various smul diamonds that only commute for SplittingField and TensorProductif they are not irreducible I believe. The same may be true of algebraic closure, although I believe it wasn't constructed with as much care so they might not commute anyway.

[Riccardo Brasca]

I am wondering if we should change the definition, following what you did with SplittingField.

[Chris Hughes]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Nontrivial.20typeclass.20def-eqs is an example for TensorProduct

[Chris Hughes]

Riccardo Brasca said:

I am wondering if we should change the definition, following what you did with SplittingField.

I think the definition AdjoinMonic in the current file is the algebraic closure and satisfies the nice def-eqs because it is a quotient of MvPolynomial. Kenny couldn't be bothered to prove this was algebraically closed and carried on adding all the roots and taking some direct limit to make a field that was easier to prove was algebraically closed, but I think proving AdjoinMonic is algebraically closed is the best construction.

[Riccardo Brasca]

I don't mean to change the mathematical construction, but the way it is written in Lean. Currently, the real this is AdjoinMonic, used to define stepAux. Then no instance are added to stepAux, but we define Step = stepAux.1 and we add the various instance.

Now, the prof that Step k n is algebraic is essentially an induction on n, as follows: the case n=0 is easy, and we split the n+1 case via the tower k → Step k n → Step k (n+1). The first morphism is algebraic by induction hypothesis and the second because of the properties of AdjoinMonic. The problem is that Lean has troubles in understanding that the second morphism is the one given by AdjoinMonic

[Riccardo Brasca]

I tried to unfold manually Step, and things seem to be faster, but then all the instances (for example Algebra k stepAux``) are missing

[Riccardo Brasca]

But I am done for today :(

[Riccardo Brasca]

I've pushed the proof I have, with two sorry that makes it working without increasing the hearbeats. I tried to use RingHom.IsIntegral to have more control on the algebra instances.

[Nikolas Kuhn]

I got a somewhat faster version (only 700000 Heartbeats) by separating out some things. I'll push it for now - everything compiles, but some proofs are still slow (max. is 900 k further down in the file).

[Nikolas Kuhn]

I'll open it up for review, but please take another look whether you like it @Riccardo Brasca !

[Riccardo Brasca]

I will have a look tomorrow, thanks!

[Junyan Xu]

Chris Hughes said:

I think the definition AdjoinMonic in the current file is the algebraic closure and satisfies the nice def-eqs because it is a quotient of MvPolynomial. Kenny couldn't be bothered to prove this was algebraically closed and carried on adding all the roots and taking some direct limit to make a field that was easier to prove was algebraically closed, but I think proving AdjoinMonic is algebraically closed is the best construction.

Just a note that this is now done in #19853.

[Patrick Massot]

Is there a specific reason to follow that note by K. Conrad instead of https://kconrad.math.uconn.edu/blurbs/galoistheory/algclosureshorter.pdf?

[Junyan Xu]

This looks great! I recall having seen such a proof, but I've forgotten about it. I wonder why K. Conrad doesn't point to the existence of a shorter version in the longer version. Formalizing this proof will probably allow us to cut down imports, especially those introduced in #19853. This proof is different in that you adjoin all roots of each polynomial, rather than one root of each polynomial, so you need to adjust the argument, not just reducing an infinite iteration to a single step. The key lemma to conclude the proof has been added in #18431, and the splitting field argument is already there.

[Junyan Xu]

#20295 switches to the construction in algclosureshorter.pdf. The reduction in imports is not very impressive: 7 files see a ~30 import reduction.

[Thomas Browning]

Does this mean that we can finally reverse the dependence between splitting fields and algebraic closure? There's been an idea floating around for a while that the algebraic closure should be defined abstractly, and then we get splitting fields just by adjoining roots inside an algebraic closure.

[Junyan Xu]

The proof still uses the splitting field to show the span of the coefficients is not everything. It seems the diamond issues around SplittingField has been solved, so there may not be much motivation to reverse the dependency. (Is there expected performance gain from changing SplittingField to a Subalgebra in AlgebraicClosure? I think subobjects rather causes performance issues?)

If you really want to define SplittingField in terms of AlgebraicClosure, I guess you have to either (1) revive the Zorn's lemma approach and ensure no diamond happens with the instances on the resulting AlgebraicClosure; (2) change the current SplittingField to SplittingFieldAux and only use it in the proofs for AlgebraicClosure; after we finish the proof we can then define the actual SplittingField that will be used across Mathlib.

[Thomas Browning]

Ah right. I do want to play around with (2), and see how it changes things.

[Junyan Xu]

That has always been an option; if you do it now, the dependencies of SplittingField would increase from 1254 to 1319 (according to #trans_imports, not GitHub bot). With #20295 they only increase to 1284.

[Thomas Browning]

Oh, yes, #20295 definitely seems worthwhile either way. I just want to play with using SplittingFieldAux in your toSplittingField, instead of SplittingField.

[Junyan Xu]

Okay, my last comment was just because the dependencies of the eventual public-facing SplittingField would be a consideration whether this refactor should be accepted to Mathlib.