Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
@Anonymous: Do you have a reference where such a definition appears? I find it very interesting.
also, moving query boxes to the nForum
+– {: .query} I might want to switch out derivatives with shift operators, since the definition involving the derivatives only work for commutative rings with characteristic zero. =–
+– {: .query} J-B: Do you know the notion of Hasse-Schmidt derivative? Maybe it could work in positive characteristic.
With one indeterminant $x$, it is defined for every $k \ge 0$ by $D^{k}(x^{n+k}) = \binom{n+k}{k} x^{n}$ and I think that we then have for all $P:R[x]$, $deg(P) = min \{i \ge 0, \forall l \ge i, D^{l}(P) = 0 \}$ (or something similar). =–
Anonymous
I have made adjustments to the wording in the beginning (here) of the Definition-section. Mostly just for readability, such as to reduce frequent repetitions, but also concerning one minor technical point:
I moved this claim from before to after the informal motivation (now here):
In the following, we work in dependent type theory with excluded middle:
But I am not sure what this comment is really doing: The material that follows does not look like it uses dependent type theory much at all. (?)
The only relevant comment I see is that rings of polynomials are advertized as “higher inductive types”. At that point it seems you really want to invoke a universal property
I’ve replaced all the instances of the nonce word ‘indeterminant’ with ‘indeterminate’ (Wiktionary and the sites that scrape it know the first word, but the second word has actual attestations and can be found in dictionaries.
Anonymous
1 to 15 of 15