poly whose roots are the products of the roots of polys

Stream: maths

[Kevin Buzzard]

This is presumably some classical construction? If I have two monic polynomials $f$ and $g$ in $k[X]$ of degrees $a,b$ and with roots $(x_i)$ and $(y_j)$ in some algebraic closure, then there's a monic polynomial of degree $ab$ also in $k[X]$ whose roots are the products $(x_iy_j)$ ("proof by Galois theory" or whatever, probably some issues in char p).

The reason I'm interested in it is the following extract from Bourbaki (Alg Comm ch V, \S 2, no 2, theorem 2 part (ii)):
bourb.png
which refers to Bourbaki Alg but I can't find what they're referring to (there doesn't seem to be a Prop 9 (EDIT: in my copy!)). The claim is (something like): if B/A are integral domains with fields of fractions L/K then to check L/K is normal (which they call quasi-Galois) it suffices to just check that every element of B is the root of a monic poly with coeffts in A and all roots in B. This feels like something we must have already in mathlib somehow. A normal extension is one where every element upstairs has the property that it's a root of a poly downstairs which splits upstairs, but we don't seem to have this predicate on elements themselves. Let's call such an element normal. I was going to knock off a proof of the Bourbaki claim myself, and my plan was "reciprocal of a normal element is normal, product of two normal elements is normal, so done" but to prove the product of two normal elements is normal I need the (presumably classical) construction above (isn't this how the ancient sages proved that integers of number fields were rings, for example?). Does it have a name? Is it in mathlib somewhere? Presumably I don't need Galois theory to write down the definition! Maybe there's some trick using tensor products of matrices and the matrix which is mostly 0's and then 1's on the off-diagonal and the coefficients of the polynomial down one row (I don't know what matrix is called either!)

[Daniel Weber]

You mean the companion matrix?

[Michael Stoll]

The simplest construction goes via the resultant, I think. (I don't know if we have it in Mathlib, though.)

[Michael Stoll]

$\operatorname{Res}_y(f(y), y^{\deg g} g(x/y))$.

[Michael Stoll]

It doesn't look like Mathlib knows about the resultant :frown: Adding it (+ API) might be a nice project for somebody...

[Antoine Chambert-Loir]

The footnote on the page you quote seems to indicate that they refer to the first edition of Algebra, where “extensions normales” were not yet called “extensions quasi-galoisiennes”.

[Antoine Chambert-Loir]

(In the second edition, the definition of extensions quasi-galoisiennes is in §9, while it apparently was in §6 in the first edition.) I don't have a copy of the first edition.

[Antoine Chambert-Loir]

The statement that is given seems to follow from the top of page V.54 (second edition) which says that the extension obtained by adding all conjugates of some elements is quasi-galoisienne. In your case, those elements are those of $A'/\mathfrak p'$, and the extension is $k'$.

[Antoine Chambert-Loir]

You can probably devise an argument using resultants, but Bourbaki gives a Galois theoretic proof of that statement in their proposition 3 (or corollary 1), two pages above.

[Kevin Buzzard]

Thanks! And sorry for wasting your time -- I had not understood that there were two editions.

[Antoine Chambert-Loir]

Worse, the correspondence between the French and English editions is not one to one…