Doing differential geometry

Stream: Is there code for X?

[Zhangir Azerbayev]

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?

[Sebastien Gouezel]

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.

[Johan Commelin]

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

[Markus Himmel]

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?

[Zhangir Azerbayev]

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

[Yury G. Kudryashov]

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

[Patrick Massot]

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

[Yury G. Kudryashov]

If $f$ is a $C^3$ smooth function and $F(x, y) = \log\frac{f(x)-f(y)}{x-y}$, then $F$ has continuous mixed derivatives in a neighborhood of the diagonal $x=y$ and $(\mathcal Sf)(x)=6\left.\frac{\partial^2F}{\partial x\partial y}\right|_{x=y}$, where $\mathcal Sf$ is the Schwarzian derivative of $f$. 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) \approx \frac{1}{6}(\mathcal Sf)(x)(x-y)^2$. If we want to have $\frac{\partial^2F}{\partial x^2}$, then we need $f$ to be more smooth.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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