Zulip Chat Archive

Stream: maths

Topic: Differential Rings


view this post on Zulip Aaron Anderson (Nov 23 2020 at 21:49):

As we have many different rings in mathlib that have their own derivatives, I think it'd be useful to have some kind of differential_ring structure.

view this post on Zulip Aaron Anderson (Nov 23 2020 at 21:51):

I'd just go ahead and make one, but it plays kind of strangely with our current definition of a derivation - right now, a derivative on a commutative ring could be seen as a particular sort of derivation, but not a noncommutative ring.

view this post on Zulip Aaron Anderson (Nov 23 2020 at 21:55):

My default idea would be to have differential_ring (or perhaps some more suitable name) be a mixin on a ring, providing the additional data of a default derivation. Then rings that would have instances would include polynomial rings, relevant rings of functions, and any sorts of power series that have or may soon have (I'd like to add Hahn series, for instance)

view this post on Zulip Aaron Anderson (Nov 23 2020 at 21:57):

But perhaps instead of a definition with use case [ring R] [differential_ring R], it'd be better to make one with use case[ring R] (D : derivative R)?

view this post on Zulip Aaron Anderson (Nov 23 2020 at 21:58):

(alternately, I could just start proving things about commutative differential algebra using our current definition of derivation)

view this post on Zulip Kevin Buzzard (Nov 23 2020 at 22:09):

Multivariable polynomials rings have lots of derivatives. In algebraic geometry I guess I'm more used to thinking about an entire module of derivations. Conversely, when we finally define a cohomology theory in Lean we might well end up with an abelian group nNCn\oplus_{n\in\mathbb{N}}C_n equipped with a dd such that d2=0d^2=0, but no ring structure.

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:12):

Model theorists do sometimes consider multiple commuting derivations.

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:13):

@Aaron Anderson there's this more general notion of rings with operators that also includes multiple operations (both differential and difference algebra are special cases). I wonder if it would be better to start by formalizing this more general thing, and later specialize?

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:18):

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:18):

docs#derivation (since I'm lazy and on mobile)

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:20):

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

view this post on Zulip Aaron Anderson (Nov 23 2020 at 22:20):

Eric Wieser said:

docs#derivation (since I'm lazy and on mobile)

Some of the ideas I proposed use this - all would prove at least some relation to it

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:21):

(sorry for the double posting... Internet is sketchy right now :frown:)

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:21):

Yep, I just wanted a link I could click on

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:22):

Sad to see that it doesn't generalize to non-commutative algebras...

view this post on Zulip Aaron Anderson (Nov 23 2020 at 22:23):

Eric Wieser said:

Sad to see that it doesn't generalize to non-commutative algebras...

Yeah, you really want to be able to scalar-multiply on the right. Which is no problem if you're working with a non-commutative ring...

view this post on Zulip Aaron Anderson (Nov 23 2020 at 22:24):

still, most of the important examples I can think of right now are commutative, so if there's any enthusiasm for implementing something like this using derivation, I wouldn't mind sticking to the commutative case for the moment.

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:27):

Ah right, for rings you're happy to work with the simpler case where the map is from R to itself

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:27):

Rather than generalizing to an arbitrary codomain

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:36):

I honestly can't think of any natural example of a noncommutative differential ring. Do you have something in mind?

I tend to think of the derivation itself as some sort of noncommutative structure

view this post on Zulip Aaron Anderson (Nov 23 2020 at 22:38):

I suppose I don't know either.

view this post on Zulip Adam Topaz (Nov 23 2020 at 22:48):

I suppose DGAs are the only example I know of...

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:48):

Right, that's basically the case I'm thinking of

view this post on Zulip Eric Wieser (Nov 23 2020 at 22:50):

But I'm not so sure that left/right modules would help much anyway, partly because I'm somewhat out of my depth

view this post on Zulip Aaron Anderson (Dec 01 2020 at 05:52):

I'm working on refactoring the derivative on polynomials to be a derivation at branch#polynomial_derivation

view this post on Zulip Aaron Anderson (Dec 01 2020 at 05:53):

So far, I've just made it a linear_map, and I'm working on modifying the import tree so that ring_theory.derivation doesn't import data.polynomial.derivative

view this post on Zulip Aaron Anderson (Dec 01 2020 at 06:00):

Separately, I want to prove some basic lemmas about derivation A R R where R is a ring

view this post on Zulip Aaron Anderson (Dec 01 2020 at 06:01):

which seems like a sensible definition of a derivative

view this post on Zulip Aaron Anderson (Dec 01 2020 at 23:01):

Aaron Anderson said:

So far, I've just made it a linear_map, and I'm working on modifying the import tree so that ring_theory.derivation doesn't import data.polynomial.derivative

Oh no... this broke is_R_or_C...

view this post on Zulip Aaron Anderson (Dec 01 2020 at 23:08):

It seems line 548 of is_R_or_C stops working, but if I replace the implicit

re_lm.mk_continuous 1 $ by { simp only [norm_eq_abs, re_lm_coe, one_mul], exact abs_re_le_abs }

with the explicit

@linear_map.mk_continuous  K  _ _ _ _ _ re_lm 1 $ by { simp only [norm_eq_abs, re_lm_coe, one_mul], exact abs_re_le_abs }

then everything is saved.

view this post on Zulip Aaron Anderson (Dec 01 2020 at 23:08):

Can anyone help me figure out what this has to do with data.polynomial.derivative?

view this post on Zulip Aaron Anderson (Dec 02 2020 at 01:17):

Actually, linear_map.mk_continuous re_lm 1 $ by { simp only [norm_eq_abs, re_lm_coe, one_mul], exact abs_re_le_abs } works

view this post on Zulip Aaron Anderson (Dec 02 2020 at 02:16):

Bizarre, once that's done, it all builds

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

Ah, but now we have the issue of derivations not being defined on noncommutative semirings.

view this post on Zulip Aaron Anderson (Dec 02 2020 at 02:21):

I'm assuming that it'd be an inconvenience if we stopped being able to define the derivative of polynomials with noncommutative coefficients, so I should define the linear map and the derivation separately?

view this post on Zulip Aaron Anderson (Dec 02 2020 at 02:22):

oh, not even on comm_semiring, yeah, I definitely want to take the derivative of a polynomial nat

view this post on Zulip Kevin Buzzard (Dec 02 2020 at 02:23):

I didn't even know we had polynomials with noncommutative coefficients. Does rX=Xr?

view this post on Zulip Kevin Buzzard (Dec 02 2020 at 02:24):

I don't know what the D-module people do, but in algebraic geometry (at least the part of it I know something about) you only seem to take derivations on commutative rings.

view this post on Zulip Reid Barton (Dec 02 2020 at 02:29):

Yeah, the coefficients still commute with X

view this post on Zulip Aaron Anderson (Dec 02 2020 at 02:41):

I'm just trying to see if there's a class that extends both semiring and add_cancel_comm_monoid that applies to nat

view this post on Zulip Aaron Anderson (Dec 02 2020 at 02:43):

Maybe this is the time to define semidomain... hmm, that probably won't do it either


Last updated: May 10 2021 at 08:14 UTC