Stream: Is there code for X?
Topic: Doing differential geometry
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:
- The symmetry of mixed partials
- Enough to prove that partitions of unity exist
- 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 (Jun 30 2020 at 12:10):
- 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!
- You can have a look at the directory
roadmap/topology, where plans in this direction have been sketched.
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...
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?
Zhangir Azerbayev (Jun 30 2020 at 13:36):
Thanks for all your help. @Markus Himmel that's great! I'm applying the lemma in and I don't need a formula for the connecting homomorphism.
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 exists.
Patrick Massot (Jun 30 2020 at 21:41):
Yury, I'm curious here, do you have any specific application in mind?
Yury G. Kudryashov (Jul 01 2020 at 03:05):
If is a smooth function and , then has continuous mixed derivatives in a neighborhood of the diagonal and , where is the Schwarzian derivative of . The standard estimate used in the proof of equality of partial derivatives implies that . If we want to have , then we need to be more smooth.
Yury G. Kudryashov (Jul 01 2020 at 03:10):
BTW, this also proves some (not all) results from https://arxiv.org/abs/0710.2629v5
Yury G. Kudryashov (Jul 01 2020 at 03:11):
(in some cases with instead of )
Last updated: May 17 2021 at 16:26 UTC