Constructible numbers - initial idea

[tirix]

@savask Here is an initial version for the scratchpad file for constructible numbers, as discussed in #4246 .
This is a separate file to it should be extremely easy to review and even edit directly on GitHub.

This brings no new proofs, only a few definitions.

I think a theorem like fldextdgirred might be important, both to prove that the extensions are quadratic, and to prove that the non-constructible numbers lead to cubic extensions, by exhibiting irreductible polynomials.

I'm thinking this might be the most difficult part; I think the rest should be more easily filled in.

[savask]

Thierry, thank you making the effort and writing down the initial draft! I'll comment on everything in one message, instead of starting a review.

We then proceed by showing that those two sets are equal.

It would be nice to prove that they are equal, but actually it suffices to show that Constr C_ ConstrAlg.

$c /FldExt2 $.

I'm not a huge fan of special notation for extensions of degree 2. My impression was that we try to avoid new definitions in set.mm like the plague, even if they look natural. df-extdf seems to assume that if ( e [:] f ) then e /FldExt f, so this assumption can be removed from the definition of /FldExt, and hence the whole definition boils down to

df-fldext2 $a |- /FldExt2 = { <. e , f >. | ( e [:] f ) = 2 } $.

which isn't worth the hassle, in my opinion.

In the comment to constrtow2 you write:

If an algebraically constructible point A ...

But the assumption is A e. Constr, i.e. A is geometrically constructible. There's, in fact, no definition of algebraically constructible numbers in the file right now, but looking at your definition via a chain, maybe we don't need a special symbol ConstrAlg for this definition, and we can simply make do with a $e hypothesis defining algebraically constructible points. Of course, I believe we will require some intermediate results involving fldGen which I tried to outline in the original issue #4246 .

I think a theorem like fldextdgirred might be important, both to prove that the extensions are quadratic, and to prove that the non-constructible numbers lead to cubic extensions, by exhibiting irreductible polynomials.

I was hoping to avoid this for the proof of imp2cube and use a custom argument for the polynomial x^3 - 2, but if you want, you could prove a general result like fldextdgirred first. Stefan O'Rear has done some work on minimal polynomials, but it's deprecated and applies to complex polynomials only.

[tirix]

It would be nice to prove that they are equal, but actually it suffices to show that Constr C_ ConstrAlg.

Yes, that's what ~ constrtow2 attempts to do, actually. I should update the comment.

[tirix]

I'm not a huge fan of special notation for extensions of degree 2. [...]

Yes, you're right, in general we want to avoid it, and it's good to note that it can be much shorter. There is an even shorter version without free variable, namely ( `' [:] " { 2 } ), i.e. the preimage of the singleton {2} by the degree operation. This will yield all possible pairs <. e , f >. of fields which extension is 2, which is the relation we want, but it's kind of hard to read.

Instead, I could use a "local" definition wih a class variable and repeat it in each theorem where it is used.

[tirix]

I was hoping to avoid this for the proof of imp2cube and use a custom argument for the polynomial x^3 - 2, but if you want, you could prove a general result like fldextdgirred first. Stefan O'Rear has done some work on minimal polynomials, but it's deprecated and applies to complex polynomials only.

I think if the general result exists and can be used, it's great because then it can serve as a foundation for more advanced things later. Here it will already be used 3 times. I'm wondering if I need a condition that the polynomial M is monic?

[savask]

Instead, I could use a "local" definition wih a class variable and repeat it in each theorem where it is used.

Sounds good (I hope we have enough class variables...).

I think if the general result exists and can be used, it's great because then it can serve as a foundation for more advanced things later. Here it will already be used 3 times. I'm wondering if I need a condition that the polynomial M is monic?

I don't think monicity is required in fldextdgirred. Also, correct me if I'm wrong, but in

fldextdgirred.m $e |- M = ( Poly1 ` F ) $.

you consider polynomials over F, while we need polynomials over the subfield K. I think there should be some condition that all coefficients of P lie in K.

If you want to show a proper result like fldextdgirred, then it's best to define minimal polynomials (which will have to be monic) and prove

1. If x in F has a minimal polynomial of degree k over the subfield K, then |K(x) : K| >= k. This should be relatively easy, since 1, x, ..., x^(k-1) are linearly independent.
2. If x in F is a root of an irreducible polynomial of degree k over the subfield K, then the degree of its minimal polynomial is also k. This is also not super hard.
3. If x in F is a root of some polynomial of degree k over the subfield K, then K(x) = K[x] and |K(x) : K| <= k. The first part, saying that the field generated by K and x consists of values of polynomials at x is the most tricky one in my opinion. It requires showing that dividing by a polynomial can be replaced by multiplication, using the Euclidean algorithm, hence K[x] is a field.

[avekens]

Very long and complicated! Would it be helpful to have separate definitions for "set of intersections of two lines", "set of intersections of a line and a circle" and "set of intersections of two circles"?

[tirix]

We try to limit the number of definitions - do you think it would be wise to add them? I don't know about any other use.

BTW, do you think we could reuse any of the theorems of the ~ inlinecirc02p family?

[avekens]

We try to limit the number of definitions - do you think it would be wise to add them? I don't know about any other use.

OK, maybe we can provide theorems instead which show the three kinds of construction explicitly.

BTW, do you think we could reuse any of the theorems of the ~ inlinecirc02p family?

Maybe, but the definitions are too different at the moment. Maybe we need a mapping of the different representations first.

[savask]

OK, maybe we can provide theorems instead which show the three kinds of construction explicitly.

I have suggested some theorems in this post which decompose the definition into three subgoals. We don't have the algebraic definition of constructible numbers with towers yet, so they can't be used as is, but maybe we could restate those only in terms of fields. For example, for a line, given by two points, and a circle, given by three points, if these points lie in some subfield of C, then the intersection also lies in quadratic extension of that subfield.

I think we unfortunately can't use inlinecirc02p since we need to keep track of the subfield we are working in.

[tirix]

With this latest submission I'm adding a definition of algebraic numbers, and of minimal polynomials, as discussed in this comment.

This includes a proof of the existence of a monic polynomial, the second step would be to prove its unicity.

This also includes a definition for algebraic numbers in a field extension, which could be useful for @metakunt's #4554 .

The definition of minimal polynomial is not yet used, so it might still change.

I've included the new definitions directly in set.mm and not in the constr.mm file, because I'm using Yamma which does not support included files yet.

This is a larger change with several theorems moved to main, and some hopefully useful theorems added, so I hope it can be merged before I'm going on.

Two interesting new theorems are:

• evls1fpws which gives the expansion of the evaluation function for a univariate polynomial; I'm surprised this was not
• ressply1evl which states that the subring polynomial evaluation function is a restriction of the "main ring" polynomial evaluation function

I was surprised none of those existed yet.

[savask]

Nice work! The definitions are too technical for me, so I've been able to spot only one small inconsistency in comments, and have no other remarks.

[metakunt]

Ah cool, how would we define the algebraic closure with this definition?

[avekens]

A space character is missing at the end.

[avekens]

"for a scalar" or "for scalars"

[avekens]

"nonzero polynomials" (p e. ( dom O \ { Z } ))?

Maybe it should be explicitly made clear that the idiom ( ` ' ( O ` p ) " { .0. } ) must be "translated": by ~fniniseg2, it is { x e. ( Base ` E ) | ( ( O ` p ) ` x ) = .0. }, which matches the description in the comment.

Proposal:

The algebraic numbers over a field F within a field E . That is, the numbers x which are roots of nonzero polynomials p ( x ) with coefficients in ( Base ` F ) . This is expressed by the idiom ( ` ' ( O ` p ) " { .0. } ), which can be translated into { x e. ( Base ` E ) | ( ( O ` p ) ` x ) = .0. } by ~fniniseg2 .