the power basis of a conjugate

Stream: maths

[Eric Rodriguez]

I'm currently trying to define power_basis.map_conjugate, which would take a power-basis to the power-basis of one of its minpoly conjugates. I'm struggling a couple things, and would love people's thoughts:

• In what generality is this true? Standard results tell us it's true for a field extension and equal minimal polynomials, but Anne suggested that maybe it suffices to just have that each element is a root of each others' minimal polynomial, which is more convenient to work with. And I don't see any reason it shouldn't hold for domains, either.
• How do we actually write the proof? The standard proof for this is based on splitting fields being isomorphic, which doesn't sound fun to work with in Lean. I've spent all day trying to think of some alternative way, but I've drawn a complete blank. Furthermore, this limits us to fields completely, which doesn't seem the correct generality.

Any ideas much appreciated!

[Johan Commelin]

What should the resulting type of power_basis.map_conjugate be? An algebra automorphism?

[Kevin Buzzard]

If you have a precise maths question can you just ask it in LaTeX? A maths MWE?

[Eric Rodriguez]

if $\alpha, \beta$ are two elements in a ring $S$ which is an $R$-algebra, such that $m_\alpha (\beta) = m_\beta(\alpha) = 0$, how do I prove that $1, \beta, \beta^2 \ldots \beta^k$ is a basis if $1, \alpha, \alpha^2, \ldots, \alpha^k$ is a basis? and what conditions do we need on $R, S$?

[Eric Rodriguez]

(deleted)

[Eric Rodriguez]

Sorry I wasn't very clear originally, when I spend too long thinking about a problem I end up forgetting not everyone else has.

[Riccardo Brasca]

Note that the minimal polynomial over a ring is not the same as the minimal polynomial over the fraction field, so you need to be careful: take $\frac{1+\sqrt{5}}{2}$: the minimal polynomial over $\mathbf{Z}[\sqrt{5}]$ (yes, I mean the one not integrally closed) is $x^2-x-1$, but over $\mathbb{Q}(\sqrt{5})$ is just $x - \frac{1+\sqrt{5}}{2}$.

[Riccardo Brasca]

This is not a problem if the ring is integrally closed, so one can use Gauss lemma. Mathlib knows this in the more restrictive case of a gcd_monoid or something like that, in practice for PID in the number field case.

[Riccardo Brasca]

So if you take $R = \mathbb{Z}[\sqrt{5}]$ and $\alpha = \frac{1+\sqrt{5}}{2}$, then the minimal polynomial of $\alpha$ is of degree $2$, but $R[\alpha]$ is not free over $R$, it has no basis. I am afraid the theory over non integrally closed domains will be a mess...

[Eric Rodriguez]

Right, but that's fine, I think? Because $R[\alpha]$ has no basis at all - I'm only considering the cases when we already have one of the conjugates being a basis, and essentially want to transfer that over.

[Kevin Buzzard]

So what is the definition of $m_\alpha$? There's some assumption on $\alpha$ and $\beta$ that they satisfy some monic polynomial with coefficients in $R$? And $m_\alpha$ is what -- just some random monic polynomial of minimal degree? Are there any missing assumptions? You don't want any integral domain or anything? Is this really the MWE?

[Kevin Buzzard]

Oh this isn't a well-defined question yet? You want me to supply the assumptions? You don't have a well-defined theorem statement?

[Riccardo Brasca]

I mean that minimal polynomial over non integrally closed domains can be strange.

[Riccardo Brasca]

@Kevin Buzzard in mathlib a minimal polynomial of an integral element is any monic polynomial of minimal degree that has the element as root.

[Eric Rodriguez]

Kevin, the case I know is for $S/R$ as a field extension, and this comes from splitting fields being isomorphic. This isn't a fun proof to Lean, so I'm looking for another proof, mainly, and a generalization of the statement seems natural from that idea. I guess things will be domains, and Riccardo is pointing out that if things aren't integrally closed things get painful too

[Riccardo Brasca]

In particular it doesn't divide monic polynomials with that element as root (it does of course over a field).

[Riccardo Brasca]

In my previous example take $x^2-x-1 + 2*(x-\frac{1+\sqrt{5}}{2})$.

[Riccardo Brasca]

Both are minimal polynomials. It is a mess...

[Eric Rodriguez]

but doesn't that example only work in $\mathbb{Q}(\sqrt{5})$, where the minpoly is uniquely $(x-\frac{1+\sqrt{5}}{2})$?

[Riccardo Brasca]

I have to teach now, but I meant over R. Certain results can very well hold in general, but I see this as an indication that the notion is not very interesting.

[Riccardo Brasca]

Note that I multiply by 2, so the polynomial has coefficients in R.

[Anne Baanen]

My thinking at the moment: suppose we have an equivalence f sending α to β, so we also have an inverse g sending β to α. To have f well-defined as an alg-hom, β should be a root of minpoly R α, vice versa for g we need that α is a root of minpoly β. To have f injective means that a_0 + a_1 β + ... + a_(n-1) β^(n-1) = 0 implies a_0 + a_1 α + ... + a_(n-1) α^(n-1) = 0: so the set of polynomials for which α is a root needs to be the same as the set of polynomials for which β is a root. I don't think that that follows from α and β being the root of each others' minimal polynomial, unless we're in an integrally closed domain.

[Kevin Buzzard]

The min poly feels to me like a red herring in this generality. The point of the min poly of x is that it's useful when it's the canonical generator of the ideal of all polys which vanish at x. I would guess that any statement involving some crazy definition of min poly in a situation where it does not have that property is unlikely to be useful. Anne is saying that we should be demanding that every polynomial has the property that it kills alpha iff it kills beta.

[Riccardo Brasca]

I agree with Kevin. Even if certain result hold, math is telling us to avoid this notion...

[Eric Rodriguez]

oh! and I see how this links into the maths - if we make the ideal generated by all of these polynomials that are killed, then this isn't necessarily principal - unless $R[X]$ is a PID ↔ $R$ is a field!

[Eric Rodriguez]

and because things are integrally closed, this can be lifted from the field of fractions. so it's seeming to me that the field result really is the canonical result, and everything comes from there, unless I can figure out a way to work with this ideal...