Zulip Chat Archive

Stream: Is there code for X?

Topic: Basis for quotient of polynomial ring


view this post on Zulip Patrick Lutz (Sep 28 2020 at 18:30):

Is there anything already in mathlib proving that the dimension of F[x]/pF[x]/p as a vector space over FF is the degree of pp (where FF is a field and pp is a nonzero polynomial over FF) or that 1,x,,xn11, x, \ldots, x^{n - 1} is a basis (where nn is the degree of pp)?

view this post on Zulip Simon Andreys (Nov 27 2020 at 15:31):

I would be interested in that too ! I'd use the basis 1,(xλ),...,(xλ)n11, (x-\lambda), ..., (x-\lambda)^{n-1}.

view this post on Zulip Kenny Lau (Nov 27 2020 at 15:37):

@Patrick Lutz @Simon Andreys docs#adjoin_root.power_basis

view this post on Zulip Simon Andreys (Nov 27 2020 at 15:40):

Great thank you !

view this post on Zulip Simon Andreys (Nov 27 2020 at 17:59):

The terminology is a bit confusing here... adjoin_root only deserves its name when p is irreducible, but the definition and theorem do not require any proof that p is irreducible so it works fine anyway.

view this post on Zulip Kevin Buzzard (Nov 27 2020 at 18:10):

Definitions and theorems in Lean are intentially formalised so that they require the bare minimum from the inputs, just enough to make sense (for example the Sup function on the reals doesn't require the set to be nonempty or bounded above, and the square root function on the reals doesn't demand that the input is nonnegative). On the other hand I think R[X]/(p(X))R[X]/(p(X)) is in some sense the universal way of adjoining a root of pp to RR.

view this post on Zulip Simon Andreys (Nov 28 2020 at 10:42):

Indeed, it was the math I was actually confused about, not the terminology ! I'm not used to consider polynomials on a ring which is not a field.

view this post on Zulip Aaron Anderson (Dec 04 2020 at 18:45):

Do we have a basis for the (mv_)polynomial ring itself?

view this post on Zulip Aaron Anderson (Dec 04 2020 at 18:46):

It wouldn't be a power_basis, because that assumes finiteness.

view this post on Zulip Aaron Anderson (Dec 04 2020 at 18:46):

I'd like to be able to define a linear_map from a polynomial ring, and one way to do that would be using is_basis.constr if we know the powers of X form a basis.

view this post on Zulip Aaron Anderson (Dec 04 2020 at 18:47):

(I'm sure other ways exist, but I'd still like to have that basis.)

view this post on Zulip Kevin Buzzard (Dec 04 2020 at 19:07):

My memory from working with mv_polynomials was that we do not have this. We have monomial s a which is aXsaX^{s} (here s : σ →₀ ℕ) and these span mv_polynomial R σ as an abelian group, which in my experience turned out to be good enough. You can of course use monomial s 1. Beware the zero ring.


Last updated: May 17 2021 at 15:13 UTC