Bennett Chow

Stream: new members

[Bennett Chow]

Hello! I am new to Lean and my interests are in Differential Geometry and especially Ricci flow. I have no previous programming experience but I am eager to learn. I would like to know what has been done so far to formalize differential geometry. Is there a group doing this? Thanks! - Ben

[Bryan Gin-ge Chen]

Welcome! Differential geometry is being actively worked on; Riemannian manifolds were added to mathlib just a few weeks ago. Maybe @Michael Rothgang, @Patrick Massot or @Sébastien Gouëzel can say a little bit more.

[Matthew Ballard]

It would be amazing to have more PDEs, especially geometric PDEs.

[Michael Rothgang]

Welcome! I'm really happy to see more people interested in formalising differential geometry: while quite some foundations are already there, there's a lot left to do, and we can use many more helping hands!

[Michael Rothgang]

Let me give you a short overview where we stand currently and what is being worked on.

mathlib has a lot of basics already: smooth manifolds (real, complex or p-adics, without and with boundary, including Banach manifolds), smooth maps, smooth vector bundles (including the direct sum, pullback and hom bundle). There is the Lie bracket of vector field fields and the Lie algebra of a Lie group. We have Riemannian manifolds (and vector bundles) very recently. On the analysis side, we also have Gronwall's lemma and the local existence of flows, as well as Lipschitz-ness in the initial conditions.

Some basic objects are still missing (and being worked on):

• Patrick Massot and I have defined affine connections/covariant derivatives. We have proven the classification of connections over trivial bundles, and are working towards the connection to Ehresmann connections. (The local/trivial bundle case is already proven, and we have a plan for the rest.) A next step could be constructing the pullback connection and the geodesic flow of a connection.
• We also defined the Levi-Civita connection and have mostly proven its existence and uniqueness. (Finishing this should take a few days, i.e. is not far away.) All of this is in a branch of mathlib, though --- i.e., not merged yet.
• I am working on defining smooth immersions and submersions, and using that to define embedded submanifolds. (The basic strategy seems solid, but a bunch of work remains in completing all the loose ends.)

• I also have a branch developing (smooth unoriented) bordism theory: defining the bordism groups and proving are a group. (In particular, this means a way to work with the interior and boundary of a manifold.)
  Getting this merged into mathlib will require merging immersions and submersions.

• Winston Yin (building on lots of previous work by Yury Kudryashov) is working on flows of vector fields: proving the local existence of flows (#26395), being C^n (#26393) as well as the global existence of flows on compact manifolds without boundary (#26395) are all quite close to getting merged. They are working on proving smooth dependence on the initial conditions now.

[Michael Rothgang]

If you'd like to work on differential geometry, there are many ways you can get involved:

• we're still missing the inverse function and regular value theorem. (I have a branch on the former, and might supervise a student doing the latter (not certain yet).)
• we're also missing quotients of manifolds, e.g. the quotient of a smooth manifold by a proper discrete action being smooth again.
• if you like gluing, a great project would be to add gluing of two manifolds. (As in, attaching a handle, or gluing two manifolds along a common collar. This may require some work on the topology side at first; I can provide references/point you to previous, unmerged, work if needed.)
• for a big and more tedious project: we have the classification of 0-manifolds, but not of 1-manifolds.

[Michael Rothgang]

On the analysis side: as Matthew mentions, there's plenty of room for ODE and PDE theory (the latter is basically missing). I don't think there's much active work on this, so contributions are extremely welcome!

If you like hard analysis: @Filippo A. E. Nuccio and I are working towards defining Sobolev spaces --- building on prior work of @Anatole Dedecker and @Luigi Massacci Give us a few months, then hopefully things should be ready on a branch. Mathlib has the Sobolev inequality already (by @Floris van Doorn and @Heather Macbeth); deducing the Sobolev embedding theorem from that is a natural next step.

[Michael Rothgang]

I hope that was not too long. In summary:

• there is active work on many items, and many more can use help!
• on the differential geometry side, useful projects could be quotients of manifolds, gluing and the regular value theorem
• we are getting lots of prerequisites for talking about smooth flows on manifolds (most of it is waiting on review)
• on the analysis side, ODE and PDE theory can use some love

Personally, I have to be mindful with my time (I have too many ideas already), but I'm very excited about new differential geometry work. I'm happy to help you get started or if you're stuck. (And if you like to work on gluing, I'm happy to discuss more; I need that for my bordism theory project also.)

[Michael Rothgang]

To answer your final question: there's no "formalising differential geometry group" at the moment.
Floris van Doorn, Sébastien Gouezel, Yury Kudryashov, Heather Macbeth, Patrick Massot, Oliver Nash and Winston Yin all have made big contributions, but we're currently all in different places. (And some (not all) are very busy with their day job/teaching/supervision/administration work.)

[Bennett Chow]

Thank you for the messages! I didn't see them until now. I will read them with interest. I only read my direct messages; lol.

[Bennett Chow]

Since the Levi-Civita connection $\nabla$ is almost done, is it possible that next the Riemann curvature tensor $\mathrm{Rm}$ can be formalized without further prerequisite notions (since Lie bracket is done)? And then the Ricci tensor $\mathrm{Ric}$ and scalar curvature $R$?

[Bennett Chow]

I thought, for Ricci flow $\partial_t g = - 2 \mathrm{Ric}$, it would be cool if after the basic definitions, and say developing covariant differentiation $\nabla$ on tensor bundles $\bigotimes^r T^*M \otimes \bigotimes^s TM$ and the associated commutator formulas $\nabla^2_{X,Y}-\nabla^2_{Y,X}$ (or in indices, $\nabla_i \nabla_j-\nabla_j\nabla_i$), one could develop the tensor calculus so that one can start to derive basic evolution equations, e.g., the scalar curvature satisfies the heat-type equation $\partial_t R = \Delta R + 2 |\mathrm{Ric}|^2$.

[Bennett Chow]

My general impression of Ricci flow is that PDE theory is used in rather limited cases, such as short time existence, where hopefully we can treat short time existence (for the time being) as a black box. It seems that one can go reasonably far just using the maximum principle (first and second derivative tests from multivariable calculus: at a spatial maximum of $f$, $\nabla f=0$ and $\Delta f \leq 0$), integration by parts (via Stokes's/divergence theorem), and the Arzela--Ascoli theorem.

[Bennett Chow]

It would be nice to develop variation formulas. E.g., suppose that $g(s)$ is a $1$-parameter family of Riemannian metrics and denote $v := \partial_s|_{s=0} g(s)$ (which can be any symmetric $2$-tensor). Show that the corresponding variation of the scalar curvature is given by: $\partial_s|_{s=0} R(s) = - \Delta (\mathrm{tr} (v) ) + \mathrm{div} (\mathrm{div} (v) ) - \langle v , \mathrm{Ric} \rangle$. The evolution of the scalar curvature under Ricci flow follows directly from taking $v= - 2\mathrm{Ric}$ and the second contracted Bianchi identity $\mathrm{div}(\mathrm{Ric}) = \tfrac{1}{2}\nabla R$.

[Bennett Chow]

This brings up another naive question --- can the foundations be developed in parallel (or to what extent)? E.g., formalize the variation of scalar curvature formula at the same time or before the second Bianchi identity (and its contracted version) is formalized?

[Bennett Chow]

One could then aim to compute the variation formulas for Perelman's $\mathcal{F}$-energy and $\mathcal{W}$-entropy. This would require considering, instead of $(M^n,g)$, the triple $(M^n,g,f)$, where $f$ is a function on $M$ for the $\mathcal{F}$-energy, and for the $\mathcal{W}$-entropy adding a constant $\tau$. The derivations of the variation formulas just require (mainly) the variation of scalar curvature (mentioned above), the variation of volume form (based on the variation of a determinant of a positive-definite (symmetric) matrix), and the variation of $|\nabla f|^2$ (Dirichlet energy density/gradient norm squared).

[Dominic Steinitz]

You can get the $\LaTeX$ to render by using $$

[Bennett Chow]

Thanks! I will make the edits $ -> $$.

[Bennett Chow]

Instead of continuing to babble naive thoughts, I will put them here: https://mathweb.ucsd.edu/~bechow/LeanOnMe/NaiveThoughts.html

[Michael Rothgang]

To answer the last question from your list: no, there's no Lie derivative of tensors yet. (Some lemmas I have for Levi-Civita are the 0-form case, i.e. smooth functions. If you'd like to work on that, I'll make a PR so you can re-use them.)

[Bennett Chow]

Sorry, I didn't see your message until now! If you make a PR request, then anyone can use it? I am new to all of this, and just wanted to make sure that if I don't work on it myself, someone else can. Thanks!

[Kenny Lau]

@Bennett Chow a PR is a "request to change mathlib". if it is accepted, then the definition will be added to a newer version of mathlib, which anyone can download.

[Bennett Chow]

Thanks @Kenny Lau for the explanation. Dear @Michael Rothgang , Yes that would be great to create a PR for Lie derivative of tensors. In general, it would be great to develop in Lean: 1. Riemannian geometry, 2. Ricci flow, 3. eventually verify the proof of the Poincare conjecture. For this, I can give my two cents on what things I think would be nice to develop in the theory of smooth manifolds, basics of Riemannian geometry, fundamentals of Ricci flow, to get things going toward the eventual goal.