Differential Rings

Stream: maths

[Aaron Anderson]

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.

[Aaron Anderson]

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.

[Aaron Anderson]

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)

[Aaron Anderson]

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)?

[Aaron Anderson]

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

[Kevin Buzzard]

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 $\oplus_{n\in\mathbb{N}}C_n$ equipped with a $d$ such that $d^2=0$, but no ring structure.

[Adam Topaz]

Model theorists do sometimes consider multiple commuting derivations.

[Adam Topaz]

@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?

[Adam Topaz]

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

[Eric Wieser]

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

[Adam Topaz]

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

[Aaron Anderson]

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

[Adam Topaz]

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

[Eric Wieser]

Yep, I just wanted a link I could click on

[Eric Wieser]

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

[Aaron Anderson]

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...

[Aaron Anderson]

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.

[Eric Wieser]

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

[Eric Wieser]

Rather than generalizing to an arbitrary codomain

[Adam Topaz]

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

[Aaron Anderson]

I suppose I don't know either.

[Adam Topaz]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

which seems like a sensible definition of a derivative

[Aaron Anderson]

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...

[Aaron Anderson]

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.

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

Bizarre, once that's done, it all builds

[Aaron Anderson]

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

[Aaron Anderson]

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?

[Aaron Anderson]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Reid Barton]

Yeah, the coefficients still commute with X

[Aaron Anderson]

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

[Aaron Anderson]

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