Re: [isabelle] Prooving the existence of a splitting field

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


On 02/01/2014 17:48, Markus Schmetkamp wrote:
> 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 :-)

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.