Defining polynomials

[pierrecagne]

Writing the basics of polynomial rings, I am scratching my head about a good definition of such.

The first idea that comes to mind is to define R[X] as the sum over n:N of Rn[X], where the latter type is a wrapped copy of finite sequences of length n+1 of elements of R whose last element is non-zero (except when n=0, where it is just a copy of R). Then I'm a bit worried about defining addition in R[X]: in classical mathematics, one defines the degree of P+Q by case analysis with special care when deg(P) = deg(Q) and the leading coefficient of P is the opposite of the leading coefficient of Q. This can not be done in our constructive setting if R does not have decidable equality. Any hack?

Another definition could be to define it as an inductive type of some sort. Then I guess it really depends the kind of inductive types one allows in our foundations.

A last option to avoid the issue of option 1 would be to define R[X] as a set quotient of all finite sequences of elements of R (the equivalence relation being the deletion of trailing 0s). But then the issue seems to be that the degree function is not definable for any R.

Any other natural definition that would avoid all of these issues?

[bidundas]

The only definition I know is by the universal property {f:R[x]->A | R-alg homo} = underlying set of A Is it bad?

Bjorn

On Mar 2, 2021, at 13:18, Pierre Cagne notifications@github.com wrote:

Writing the basics of polynomial rings, I am scratching my head about a good definition of such.

The first idea that comes to mind is to define R[X] as the sum over n:N of Rn[X], where the latter type is a wrapped copy of finite sequences of length n+1 of elements of R whose last element is non-zero (except when n=0, where it is just a copy of R). Then I'm a bit worried about defining addition in R[X]: in classical mathematics, one defines the degree of P+Q by case analysis with special care when deg(P) = deg(Q) and the leading coefficient of P is the opposite of the leading coefficient of Q. This can not be done in our constructive setting if R does not have decidable equality. Any hack?

Another definition could be to define it as an inductive type of some sort. Then I guess it really depends the kind of inductive types one allows in our foundations.

A last option to avoid the issue of option 1 would be to define R[X] as a set quotient of all finite sequences of elements of R (the equivalence relation being the deletion of trailing 0s). But then the issue seems to be that the degree function is not definable for any R.

Any other natural definition that would avoid all of these issues?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[UlrikBuchholtz]

Well, we want the universal property that Hom_R(R[X],S) = S for any R-algebra S. This suggests an inductive definition, such as this one by Felix in cubical Agda. Then if you know more about R, you can prove this is equivalent to some other representations.

[DanGrayson]

The main novelty of our book is its treatment of groups. Maybe we can just depend on students knowing what polynomials are, and not worry about giving a constructive type-theoretic definition of them. In the Euclidean geometry chapter, I don't intend to construct the real numbers or define vector spaces and inner product spaces, either.

[UlrikBuchholtz]

To Dan's point, I think it's fine to do everything for rings and fields with decidable equality. If someone feels very energetic, they can then add the complications in the margin. :)

[pierrecagne]

@bidundas Yes of course, but can we really just postulate the existence of such a R-algebra ? That is what I had in mind with the inductive definition option.

@UlrikBuchholtz Thanks for the link, I checked UniMath and Hott-Coq but did not think about cubical Agda. I am not used to Agda and I don't see where the elimination rule is defined... (that was the point I was worried about in making an inductive definition: up until now, our inductive type are eliminating into any type, where here we would have to restrict to only R-algebra).

@DanGrayson Fair point. I might take that option for now, and see later if something is better with a type-theoretic definition.

[bidundas]

Given that we have geometric access to the tensor product we only need a geometric definition of the integral case Z[x].

Bjørn

On Tue, 2 Mar 2021 at 14:00, Pierre Cagne notifications@github.com wrote:

@bidundas https://github.com/bidundas Yes of course, but can we really just postulate the existence of such a R-algebra ? That is what I had in mind with the inductive definition option.

@UlrikBuchholtz https://github.com/UlrikBuchholtz Thanks for the link, I checked UniMath and Hott-Coq but did not think about cubical Agda. I am not used to Agda and I don't see where the elimination rule is defined... (that was the point I was worried about in making an inductive definition: up until now, our inductive type are eliminating into any type, where here we would have to restrict to only R-algebra).

@DanGrayson https://github.com/DanGrayson Fair point. I might take that option for now, and see later if something is better with a type-theoretic definition.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/98#issuecomment-788890905, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKO2SK65K4GADGRT5OL2UR3TBTOONANCNFSM4YO3VWYA .

[bidundas]

On that note, Z[x] appears much more geometrically accessible as a graded ring (eg as the cohomology of BBZ, but other options could be better on a practical level). Do we have a good grasp of how to forget grading?

Bjørn

On Tue, 2 Mar 2021 at 14:12, Dundas (please reply to dundas@math.uib.no) < bjorn.dundas@gmail.com> wrote:

Given that we have geometric access to the tensor product we only need a geometric definition of the integral case Z[x].

Bjørn

On Tue, 2 Mar 2021 at 14:00, Pierre Cagne notifications@github.com wrote:

@bidundas https://github.com/bidundas Yes of course, but can we really just postulate the existence of such a R-algebra ? That is what I had in mind with the inductive definition option.

@UlrikBuchholtz https://github.com/UlrikBuchholtz Thanks for the link, I checked UniMath and Hott-Coq but did not think about cubical Agda. I am not used to Agda and I don't see where the elimination rule is defined... (that was the point I was worried about in making an inductive definition: up until now, our inductive type are eliminating into any type, where here we would have to restrict to only R-algebra).

@DanGrayson https://github.com/DanGrayson Fair point. I might take that option for now, and see later if something is better with a type-theoretic definition.

— You are receiving this because you were mentioned.

Reply to this email directly, view it on GitHub https://github.com/UniMath/SymmetryBook/issues/98#issuecomment-788890905, or unsubscribe https://github.com/notifications/unsubscribe-auth/AKO2SK65K4GADGRT5OL2UR3TBTOONANCNFSM4YO3VWYA .

[DanGrayson]

Forgetting the grading of a graded ring amounts to taking the direct sum of a family of abelian groups. The way I implemented direct sum of abelian groups in UniMath is by generators and relations.

[UlrikBuchholtz]

@pierrecagne

@UlrikBuchholtz Thanks for the link, I checked UniMath and Hott-Coq but did not think about cubical Agda. I am not used to Agda and I don't see where the elimination rule is defined... (that was the point I was worried about in making an inductive definition: up until now, our inductive type are eliminating into any type, where here we would have to restrict to only R-algebra).

This is cubical Agda and the definition is a native HIT-definition, so there's no explicit eliminator defined, although one could derive that by pattern matching. The constructors include the R-algebra operations and equations, and that's why you can only really eliminate into R-algebras.

But it really shouldn't be necessary to use a HIT for this: it should be equivalent, at least in the one-variable case, to the quotient of List R modulo the equivalence relation generated by appending zeros.

Felix' definition is nice because in the multi-variable case it builds in equivariance under the symmetric group. It doesn't even require I to have decidable equality! Handling this just in terms of lists and quotients would be tricky.