Zulip Chat Archive

Stream: Is there code for X?

Topic: Doing differential geometry

view this post on Zulip Zhangir Azerbayev (Jun 30 2020 at 12:04):

Hi everyone, I'm working on a summer project with @Kevin Buzzard and I'm interested in formalizing some differential geometry (differential forms, dR cohomology, etc). Three things I will end up needing are:

  1. The symmetry of mixed partials
  2. Enough to prove that partitions of unity exist
  3. The snake lemma

I'm finding the mathlib documentation for derivatives pretty hard to read. Is there a proof of 1)? If not, how hard would it be to hack one together? 2) depends on a bunch of lemmas about compact sets. For example, we need to know that an open set can be written as the countable union of nested compacts. Can mathlib do things like this yet? I know that @Markus Himmel formalized the snake lemma, can I expect it to eventually show up in mathlib?

view this post on Zulip Sebastien Gouezel (Jun 30 2020 at 12:10):

  1. is not done, but shouldn't be hard. The right way to express things would be to say that the n-th derivative (which is a multilinear map as defined in analysis/calculus/times_cont_diff) is symmetric when well defined and continuous at a point, over any field. But doing it first for the second derivative over the reals is already a good idea!
  2. You can have a look at the directory roadmap/topology, where plans in this direction have been sketched.

view this post on Zulip Johan Commelin (Jun 30 2020 at 12:19):

You can expect the snake lemma to show up, but I'm not sure how long it will take...
Also: welcome!

view this post on Zulip Markus Himmel (Jun 30 2020 at 12:27):

My hope is that the snake lemma will be in mathlib in less than a month, but I can't make any promises. @Zhangir Azerbayev, in which category do you need the snake lemma? Do you need any explicit formula for the connecting homomorphism?

view this post on Zulip Zhangir Azerbayev (Jun 30 2020 at 13:36):

Thanks for all your help. @Markus Himmel that's great! I'm applying the lemma in Vectk\mathrm{Vect}_k and I don't need a formula for the connecting homomorphism.

view this post on Zulip Yury G. Kudryashov (Jun 30 2020 at 14:55):

For the symmetry of partial derivatives I have a request to have this lemma with very weak assumptions, i.e. do not require that 2fx2\frac{\partial^2 f}{\partial x^2} exists.

view this post on Zulip Patrick Massot (Jun 30 2020 at 21:41):

Yury, I'm curious here, do you have any specific application in mind?

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 03:05):

If ff is a C3C^3 smooth function and F(x,y)=logf(x)f(y)xyF(x, y) = \log\frac{f(x)-f(y)}{x-y}, then FF has continuous mixed derivatives in a neighborhood of the diagonal x=yx=y and (Sf)(x)=62Fxyx=y(\mathcal Sf)(x)=6\left.\frac{\partial^2F}{\partial x\partial y}\right|_{x=y}, where Sf\mathcal Sf is the Schwarzian derivative of ff. The standard estimate used in the proof of equality of partial derivatives implies that F(x,x)+F(y,y)F(x,y)F(y,x)16(Sf)(x)(xy)2F(x, x) + F(y, y)-F(x, y)-F(y, x) \approx \frac{1}{6}(\mathcal Sf)(x)(x-y)^2. If we want to have 2Fx2\frac{\partial^2F}{\partial x^2}, then we need ff to be more smooth.

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 03:10):

BTW, this also proves some (not all) results from https://arxiv.org/abs/0710.2629v5

view this post on Zulip Yury G. Kudryashov (Jul 01 2020 at 03:11):

(in some cases with o()o() instead of O()O())

Last updated: May 17 2021 at 16:26 UTC