Zulip Chat Archive

Stream: new members

Topic: Derivations


view this post on Zulip Nicolò Cavalleri (Jul 10 2020 at 11:10):

With the search methods I know I did not find any definition of derivation in Mathlib. There is not any right? In case not should I start from scratch or is there some more general structure that I can get derivations as a particular case or some non obvious structure I can extend (with obvious I mean the ones one would clearly think about by looking at Wikipedia's definition)? I did not really work with anything in the algebra section so it'd be cool to listen to some tips before beginning

view this post on Zulip Patrick Massot (Jul 10 2020 at 11:15):

I think @Shing Tak Lam did something in this direction.

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:15):

@Kenny Lau wrote some code on Zulip about a year ago but never made a PR

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:16):

Shing did partial derivatives of multivariate polynomials and I'm pretty sure this got PRed

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:17):

But this is definitely something which could be in mathlib. Module of Kaehler differentials and its universal property would be really nice to do

view this post on Zulip Shing Tak Lam (Jul 10 2020 at 11:26):

Patrick Massot said:

I think Shing Tak Lam did something in this direction.

I guess there's this?

view this post on Zulip Patrick Massot (Jul 10 2020 at 11:26):

Oh this is already specialized to polynomials :sad:

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:27):

That's because Shing is a schoolkid so I thought that leaping into the general theory of modules and derivations might not have been appropriate :rolling_on_the_floor_laughing:

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:28):

Kenny's code did the general case and will be findable by someone (eg by me once I get to a computer)

view this post on Zulip Shing Tak Lam (Jul 10 2020 at 11:28):

This is the thread Kevin's talking about btw

view this post on Zulip Shing Tak Lam (Jul 10 2020 at 11:32):

If I remember correctly, the code in the original thread is (very) broken with recent mathlib

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 11:35):

Every code written a year ago is very broken


Last updated: May 17 2021 at 21:12 UTC