Email Gateway (Aug 22 2022 at 19:37): Email Gateway (Aug 22 2022 at 19:37):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
Dear list,
is there some type class of algebraically closed fields in Isabelle/HOL?
Since such fields are an important and widely used concept I'd be
surprised if not, but a quick search in the library+AFP did not reveal
anything ...
Of course I could easily introduce a suitable type class myself, but I
just wanted to avoid duplicate work.
Best regards,
Alexander
Email Gateway (Aug 22 2022 at 19:37):From: Manuel Eberl <eberlm@in.tum.de>
I don't think there is. As far as I know, the visible Isabelle universe
only contains two concrete instances of algebraically closed fields,
namely the complex numbers (in HOL) and the algebraic complex numbers
(in the AFP entry Algebraic_Numbers). The latter are, I think, more
technically interesting and not so much for abstract mathematical
developments.
It is not necessarily bad to introduce a typeclass that has only one
instance – especially when it coincides with a standard mathematical
concept (as is the case here). However, it also doesn't have much
immediate payoff, which is probably why no one has done it so far. Feel
free to do so!
There is also a HOL-Algebra development by former students of
Larry/Anthony (much of it still in a private repository) that could be
used to make a generic "alg_closure" type constructor. Not sure how
useful that is though – it might be interesting when reasoning about
things like Galois fields or also for generic proofs involving fields,
because it allows you to suddenly go to the algebraic closure for a
proof and then back.
Another interesting instance would be formal Puiseux series. They've
been on my long-term potential to-do list. If anyone feels like having a
go at them (e.g. in analogy to the existing formal power series/Laurent
series in HOL-Compuational_Algebra), please do. :)
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 19:38):From: Alexander Maletzky <alexander.maletzky@risc.jku.at>
Dear Manuel,
thanks for your useful answer.
It is not necessarily bad to introduce a typeclass that has only one
instance – especially when it coincides with a standard mathematical
concept (as is the case here). However, it also doesn't have much
immediate payoff, which is probably why no one has done it so far. Feel
free to do so!
I will do so; should be no problem.
There is also a HOL-Algebra development by former students of
Larry/Anthony (much of it still in a private repository) that could be
used to make a generic "alg_closure" type constructor. Not sure how
useful that is though – it might be interesting when reasoning about
things like Galois fields or also for generic proofs involving fields,
because it allows you to suddenly go to the algebraic closure for a
proof and then back.
I was also thinking of something like that, although this does not have
immediate priority for me. Actually, I only want to have algebraically
closed fields for formalizing Hilbert's Nullstellensatz in the most
general setting (i.e. not restricted to complex numbers), which I'm
working on right now.
Best regards,
Alexander
Another interesting instance would be formal Puiseux series. They've
been on my long-term potential to-do list. If anyone feels like having a
go at them (e.g. in analogy to the existing formal power series/Laurent
series in HOL-Compuational_Algebra), please do. :)Cheers,
Manuel
On 08/04/2019 16:18, Alexander Maletzky wrote:
Dear list,
is there some type class of algebraically closed fields in Isabelle/HOL?
Since such fields are an important and widely used concept I'd be
surprised if not, but a quick search in the library+AFP did not reveal
anything ...Of course I could easily introduce a suitable type class myself, but I
just wanted to avoid duplicate work.Best regards,
Alexander
Email Gateway (Aug 22 2022 at 19:38):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear Alexander,
having a type-class for alg.-closed fields would definitely be something nice.
For instance, then one can also generalize the existence of a Jordan-Normal-Form
to alg.-closed fields.
Moreover, I hope in the long run that there will be at least to instances:
complex numbers and complex algebraic numbers.
Best,
René
Last updated: Nov 21 2024 at 12:39 UTC