Email Gateway (Aug 19 2022 at 13:26): Email Gateway (Aug 19 2022 at 13:26):From: Markus Schmetkamp <m.schmetkamp@gmx.de>
Hi people,
I'm trying to prove, that for every univariate polynomial has a
splitting field i.e. a field where the polynomial factors completely
into linear factors. At first it's okay, if this field isn't the
smallest field with that property.
I'm using the HOL/Algebra library (and version Isabelle2013-1) and have
already proved several useful lemmas. I defined term "field extension"
this way
locale field_extension =
fixes L::"('a, 'n) ring_scheme" (structure) and K::"('b, 'm) ring_scheme"
and iota::"'b => 'a"
assumes field_L[intro, simp]: "field L"
and field_K[intro, simp]: "field K"
and hom[intro, simp]: "iota ? ring_hom K L"
furthermore I could prove this theorem
theorem extension_with_zero:
fixes K::"'b ring" and p
assumes "field K"
and "p ? carrier (UP K)"
and "deg K p ~= 0"
shows "?(L?(nat ? 'b) set ring). ?iota. ?x ? carrier L. field_extension
L K ? ? eval K L iota x p = zero L"
That shows that you can find a field in which the polynomial has at
least one root. Next you could use long division to reduce the
polynomial and repeat the process until you have a field which contains
every root of the polynomial. That would be a solution...
Now the problem:
Isabelle forces me to specify the type of the object which existence I
want to show. Unfortunately the field I get from the theorem from above
has another "bigger" type than the field I'm starting with. If you want
to repeat the process you had to know the number of repetitions you
make, but that varies with the polynomial.
Has anyone an idea or a solution?
Best wishes
Markus
and a happy new year :-)
Email Gateway (Aug 19 2022 at 13:27):From: Tobias Nipkow <nipkow@in.tum.de>
I don't think field extensions have been formalized in Isabelle before. I
suspect you first have to define a new type that is big enough to contain all
the extension you will need and then work within that. But that is just a rough
guess.
Tobias
Last updated: Nov 21 2024 at 12:39 UTC