# Zulip Chat Archive

## Stream: maths

### Topic: Differential Rings

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

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

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

#### 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)`

?

#### 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`

)

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

#### Adam Topaz (Nov 23 2020 at 22:12):

Model theorists do sometimes consider multiple commuting derivations.

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

#### Adam Topaz (Nov 23 2020 at 22:18):

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

#### Eric Wieser (Nov 23 2020 at 22:18):

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

#### Adam Topaz (Nov 23 2020 at 22:20):

Just in case you want a reference:

https://arxiv.org/abs/1212.5838

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

#### Adam Topaz (Nov 23 2020 at 22:21):

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

#### Eric Wieser (Nov 23 2020 at 22:21):

Yep, I just wanted a link I could click on

#### Eric Wieser (Nov 23 2020 at 22:22):

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

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

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

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

#### Eric Wieser (Nov 23 2020 at 22:27):

Rather than generalizing to an arbitrary codomain

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

#### Aaron Anderson (Nov 23 2020 at 22:38):

I suppose I don't know either.

#### Adam Topaz (Nov 23 2020 at 22:48):

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

#### Eric Wieser (Nov 23 2020 at 22:48):

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

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

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

#### 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`

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

#### Aaron Anderson (Dec 01 2020 at 06:01):

which seems like a sensible definition of a derivative

#### 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`

...

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

#### Aaron Anderson (Dec 01 2020 at 23:08):

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

?

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

#### Aaron Anderson (Dec 02 2020 at 02:16):

Bizarre, once that's done, it all builds

#### Aaron Anderson (Dec 02 2020 at 02:18):

Ah, but now we have the issue of `derivation`

s not being defined on noncommutative semirings.

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

#### 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`

#### Kevin Buzzard (Dec 02 2020 at 02:23):

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

?

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

#### Reid Barton (Dec 02 2020 at 02:29):

Yeah, the coefficients still commute with `X`

#### 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`

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