!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!