(Pseudo) Riemannian metric

Stream: general

[Matteo Cipollina]

I have been making some attempts on and off over the last months, with an initial goal of implementing an InnerProductspace on a Riemannian metric .

This has been PR'd to PhysLean here https://github.com/HEPLean/PhysLean/pull/501:

https://github.com/HEPLean/PhysLean/blob/caf4d53e75b3fac17a7c2799e6575029188e2ee9/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Defs.lean

https://github.com/HEPLean/PhysLean/blob/caf4d53e75b3fac17a7c2799e6575029188e2ee9/PhysLean/Mathematics/Geometry/Metric/Riemannian/Defs.lean

The files can also be found here (i've tried them on latest stable mathlib 4.18):
PseudoRiemannian+Riemannian.lean

I've tried a pragmatic approach aimed at development within PhysLean. I'm aware the ideal formalization would be as a section of tensor bundles and would like to generalise it in that direction at some point (or even better if someone else could do it), but wanted to avoid, at first, an escalation of complications like those mentioned in previous discussions.

I thought this could first be a PR to PhysLean, which is the natural context where I would like to build over this framework, but would be happy of course, if this at some point could be fit for Mathlib.

A first revision came after reading @Sébastien Gouëzel in this post (#new members > Don't understand TangentBundle & sections and a second came after realizing the need to add a constraint for constant index, after a closer reading of O'Neill 'SemiRiemannian Geometry with applications to Relativity'.

I'd greatly appreciate critical feedback and hope this could, at least in the short term, fill a gap and trigger further development. :)

Previous discussions:
#mathlib4 > Extend manifold smoothness
#Is there code for X? > Tensor product vector bundle
#Is there code for X? > Riemannian manifolds
#mathlib4 > Topology on sets with manifold structure
#new members > Formalizing Riemannian geometry
#maths > Fiber bundles
#maths > [help needed] how to synthesis the inner from TangentSpace

[Kevin Buzzard]

+1 for the comprehensive list of links to previous discussions!