Riemannian manifolds

Stream: Is there code for X?

[Winston Yin (尹維晨)]

I’ve seen @Kevin Buzzard mention at least twice now that @Heather Macbeth has formalised Riemannian manifolds in Lean. Where can I read more about that? Is it in mathlib? This is exciting!

[Kevin Buzzard]

It was in Banff and as far as I know it's not in mathlib. It was a proof of concept.

[Michael Rothgang]

The final report from the Banff meeting points to a branch containing the definition.

[Michael Rothgang]

@Heather Macbeth What is missing to make this mathlib-ready, besides the obvious things (porting to Lean 4, filling in the sorries, clean-up and relocating lemmas)? For instance,

• should the cotangent bundle be defined differently (say, as the dual bundle of the tangent bundle, or as the hom bundle of the trivial bundle)?
• should the "bicotangent space" be generalised to product bundles?
• anything deeper than I'm overlooking?

[Michael Rothgang]

I would be interested in having Riemannian metrics (even a bare definition might suffice) --- for many reasons, including defining the Lebesgue measure on a manifold. I may have time to help. But I don't know what the current status is...

[Heather Macbeth]

@Michael Rothgang @Winston Yin (尹維晨) Indeed that is the branch. At the same time, at that workshop in Banff, @Moritz Doll and @Floris van Doorn and I were working on adjusting the hom-bundle definition, see !3#19107. Then @Yury G. Kudryashov made another refactor (!3#19221). So some of the workarounds in that branch (e.g. the explicit type synonyms for the "cotangent" and "bicotangent" bundles, and all that bulky code putting trivial instances on various bundles) should hopefully not be needed now. (I haven't checked.)

[Heather Macbeth]

A good first test of the definition would be to prove (using partitions of unity) that every manifold admits a Riemannian metric. This requires a refactor of docs#SmoothPartitionOfUnity (generalizing from functions to sections of a vector bundle) but otherwise shouldn't be hard.

[Patrick Massot]

I don't understand what you mean about docs#SmoothPartitionOfUnity. Those are general enough. What needs to be generalized are lemmas like docs#exists_smooth_forall_mem_convex_of_local and its friends from the sphere eversion project.

[Yury G. Kudryashov]

I think that this is exactly what Heather meant.

[Heather Macbeth]

Yes, sorry, I looked too hastily at the file and linked the wrong lemma. The lemmas that would need to be generalized are those which are currently written for bundled smooth functions (ContMDiffMap), you'd want them for bundled smooth sections of a vector bundle (ContMDiffSection) instead.