(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!

[Michael Lee]

Nice! Wow, it's been a couple of years since I last looked at this. I'd love to resurrect @Heather Macbeth's proof-of-concept branch. Will see if I can work on porting it to Lean 4 in the next couple of weeks and try to fill in the sorrys (e.g. show that every smooth manifold admits a Riemannian metric... I know the earlier discussion said to do this with partitions of unity, but it would be nice to cheat and use the strong Whitney embedding theorem if it were actually available...). I appreciate your generalization to pseudo-Riemannian metrics as well, will have to add that in.

[Michael Rothgang]

Ages ago, I tried porting that branch myself (and didn't get very far). In case that helps, feel free to look at branch#MR-hr-RiemannianMetric (lots of errors) and branch#MR-Riemannian-metric (no errors, but didn't get far).

[Dominic Steinitz]

Michael Lee said:

Nice! Wow, it's been a couple of years since I last looked at this. I'd love to resurrect Heather Macbeth's proof-of-concept branch. Will see if I can work on porting it to Lean 4 in the next couple of weeks and try to fill in the sorrys (e.g. show that every smooth manifold admits a Riemannian metric... I know the earlier discussion said to do this with partitions of unity, but it would be nice to cheat and use the strong Whitney embedding theorem if it were actually available...). I appreciate your generalization to pseudo-Riemannian metrics as well, will have to add that in.

I'm guessing Mathlib has partitions of unity then?

[Kevin Buzzard]

Continuous ones at least: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/PartitionOfUnity.html

[Dominic Steinitz]

Although for the existence of a Riemannian metric, a smooth one is needed.

[Patrick Massot]

It also has smooth partitions of unity.

[Ben Eltschig]

In this file, I assume? https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Manifold/PartitionOfUnity.html

[Patrick Massot]

And this is really the way to prove existence of Riemannian metrics. Morally it has nothing to do with embedding results.

[Patrick Massot]

We simply need a version of docs#exists_smooth_forall_mem_convex_of_local for non-trivial vector bundles.

[Dominic Steinitz]

Patrick Massot said:

And this is really the way to prove existence of Riemannian metrics. Morally it has nothing to do with embedding results.

Excellent news and I agree it would be going against the grain to use an embedding.

[Patrick Massot]

Note that docs#exists_smooth_forall_mem_convex_of_local and its variants are on of my favorite examples of wonderful statements that I learned from formalized mathematics and don’t exist in the real world. It really says what partitions of unity will do for you instead of simply repeating endlessly the same argument.

[Patrick Massot]

And here for instance it really points out the difference between Riemannian and semi-Riemannian cases. The key is that positive definite bilinear products form a convex set, whereas this isn’t true for other signatures.

[Matteo Cipollina]

I've added a new file
PseudoRiemannian/Chart.lean at
https://github.com/HEPLean/PhysLean/blob/21f522bea68644a7c500ffb3aeb9104792d9de7d/PhysLean/Mathematics/Geometry/Metric/PseudoRiemannian/Chart.lean
which defines the components of a pseudo-Riemannian metric in local chart coordinates (chartMetric g e y). The main result is chartMetric_coord_change, proving tensor transformation law under coordinate changes: chartMetric g e (e x) = pullback (chartMetric g e' (e' x)) (mfderiv I I (e.symm.trans e') (e x)). This builds on the Defs.lean for pseudo-Riemannian metrics and several helpers lemmas that I could not find in Mathlib and that have grouped in hypothetical Mathlib modules: Analysis.ContDiff; LinearAlgebra.BilinearForm; Geometry.Manifold.PartialHomeomorph; Geometry.Manifold.Chart.Utilities, Smoothness, BilinearSmoothnes, CoordinateTransformations).
https://github.com/HEPLean/PhysLean/pull/501/commits/21f522bea68644a7c500ffb3aeb9104792d9de7d#
Thanks @Michael Lee , it would be great to join efforts and work in parallel on the old proof of concept (thanks @MichaelRothgang for sharing it, I couldn't find it anywhere), connect it to this level and prove the existence of the Riemannian metric via partitions of unity at some point

[Michael Lee]

Michael Rothgang said:

Ages ago, I tried porting that branch myself (and didn't get very far). In case that helps, feel free to look at branch#MR-hr-RiemannianMetric (lots of errors) and branch#MR-Riemannian-metric (no errors, but didn't get far).

branch#michaellee94/riemannian should at least get us to parity with Heather's branch. I'll work on filling in the sorrys soon (my wife and I are moving house in a couple of days, so things might be hectic for a minute, but I'm determined to finish this!).

[Jens Lindekamp]

My 2 cents as a lean newbie having some background in Riemannian Geometry (though that is a few years ago, I made my PhD in 2002 ;-)): I think we need to introduce tensor bundles in the form of multilinear maps from k factors of TM and l factors of T*M to k (or R/C) to really make a step forward.

In general, we need the tensor bundles to define:

1. Metrics as (2,0) tensors
2. The Riemmanian curvature as (3,1) tensor
3. Ricci curvature as (2,0) tensor
4. Torsion of an affine connection as (2,1) tensor (this is necessary to introduce the Levi-Civita connection which is torsion-free and the basis for (Pseudo-) Riemannian Geometry.
5. Differential forms as alternating (k,0) tensors. (And go to deRham cohomology from there....)

And potentially a few more, but that's more than enough....

I thought of defining a VectorBundleCore with a subtype of MultiLinearMap as fibres based on the TangentBundle. The construction could be done based on any vector bundle, but in practice, we would only need multilinear maps / tensors on the tangent bundle.

One could also introduce a general notion of general tensor products for vector bundles, but that's probably much more complex, and probably not needed at all for differential geometry.

Based on this, we could consider metrics "just" as a special case (k = 2, l = 0) of the tensor bundle.

Maybe it's only slightly more complex to create such a tensor bundle instead of the cotangent bundle as bundle of linear maps to k, metrics as bilinear maps to k etc.

Having said that - I'm not yet able to deal with VectorBundleCore, so I'm probably (surely) missing subtle details of the implementation....

[Joseph Tooby-Smith]

If one restricts to finite dimensions, does anyone know if the complications of defining tensor products of vector bundles go away?

[Floris van Doorn]

Joseph Tooby-Smith said:

If one restricts to finite dimensions, does anyone know if the complications of defining tensor products of vector bundles go away?

Working with vector bundles in Mathlib right now is currently doable but definitely not easy. I don't think that assuming finite-dimensionality will make it easier to work with them.

[Joseph Tooby-Smith]

c.f. @Jens Lindekamp's last comment:

I for one would be very interested in seeing the ability of general tensor products for vector bundles, since it would allow for lots of applications in PhysLean (GR and tensor products of fields in particle physics etc.). In particular one could generalize in the mathematically correct way to do index notation from tensors to tensor fields.

[Joseph Tooby-Smith]

Floris van Doorn said:

Joseph Tooby-Smith said:

If one restricts to finite dimensions, does anyone know if the complications of defining tensor products of vector bundles go away?

Working with vector bundles in Mathlib right now is currently doable but definitely not easy. I don't think that assuming finite-dimensionality will make it easier to work with them.

I guess I'm not asking from the point of view of Mathlib, but rather the point of view of the maths in developing the theory further.

I guess I'm asking the following:
Is there an "easy" definition of the tensor product of vector bundles in the finite dimensional case that we could develop and work with in e.g. PhysLean, until Mathlib has the completely general case.

Reading #Is there code for X? > Tensor product vector bundle , it seems like the origin of the difficulties is really down to the infinite dimensional case, but I could be missing something from the mathematical point of view here.

[Sébastien Gouëzel]

To define a Riemannian metric, one should really not use tensor product of bundles: a metric on a vector space E is a continuous bilinear map E →L[ℝ] E →L[ℝ] ℝ which turns out to be symmetric and positive. Given a vector bundle (for instance the tangent bundle), we already have in mathlib the vector bundle of continuous linear maps, so iterating we already have the E →L[ℝ] E →L[ℝ] ℝ vector bundle. Identification with a tensor bundle is not useful here, and even a little bit misleading as it makes things more complicated: E →L[ℝ] E →L[ℝ] ℝ is a much simpler object than E* ⊗ E* (for instance, it has a canonical norm, it is complete whenever Eis, and so on).

[Jens Lindekamp]

To define a Riemannian metric, one should really not use tensor product of bundles...

Sorry for causing confusion - this is what I actually meant. Reading my post again, I understand that this wasn't clear...

In https://github.com/leanprover-community/mathlib4/tree/michaellee94%2Friemannian, the CotangentSpace is defined using the TangentSpace. Does anybody have an opinion about similar constructions on slightly more arbitrary vector bundles? I think of normal bundles of immersed submanifolds, for example the second fundamental form for an immersed submanifold, which maps two vectors to a normal vector. This could be a bilinear map E →L[ℝ] E →L[ℝ] E' at each point, where E is the tangent space of the sub-manifold and E' the normal bundle (probably seen as pullback bundle using the immersion, but haven't thought about it long enough).

Thinking about differential forms: would they be defined inductively using ContinousLinearMap (plus conditions on being alternating)?
If so, any ideas how one would formulate something like α(v1, v2, ..., vk) = -α(v2, v1, ...., vk)?

[Sébastien Gouëzel]

Differential forms would be defined not by induction, but as a bundle of docs#ContinuousAlternatingMap. When you have a vector bundle, there are a bunch of constructions you can make, like bundles of continuous linear maps, but also bundles of multilinear maps, and so on.

[Jens Lindekamp]

So, would differential forms on a manifold be formalized similar to Bundle.ContinuousLinearMap, but based on ContinousAlternatingMap?

[Jens Lindekamp]

Pushing the concept a bit: if we want to formalize the Riemannian curvature tensor R(X,Y)Z for vectors X,Y,Z with values in TM, would this be a similar construction, but using ContinousMultiLinearMap?

[Sébastien Gouëzel]

I think the curvature tensor would rather be formalized using linear maps, as E →L[ℝ] E →L[ℝ] E →L[ℝ] E, because curried variants are easier to use in this form. But essentially yes, this is the same thing as a multilinear map in three vectors.

[Michael Lee]

Agreed that this is the correct formulation, but this notation seems a bit tortured. Is it possible to define an abbrev for an (m, n) tensor type that curries the maps an appropriate number of times?

[Sébastien Gouëzel]

One will just need to write this type once, when defining the tensor. Then, when applying it, you will just write riemannTensor u v w (and you can introduce a local notation to be able to write R u v w).

[Jens Lindekamp]

What about other notions like covariant derivatives of (m, n) tensors or the Lie derivative of (m, n) tensors? Like the exterior derivative, which takes a k form to a k + 1 form, the other two derivatives can be defined on (m, n) tensors and take a (m, n) tensor to a (m + 1, n) tensor.

If we define tensors (in the sense of multilinear maps...) in a case-by-case way, this might be difficult to formulate.

Some examples:

The Levi-Civita connection induces (like any connection) a connection on (3,1) tensors. When applied to the curvature tensor, this connection gives rise to the second Bianchi identity. And when it is 0, the Riemannian manifold is actually a symmetric space.

The Levi-Civita connection of a metric is per definition 0, i.e. we may want to have the notion of an induced connection on (2,0) tensors to define it.

A vector field is a Killing field iff the Lie derivative of the metric (as a (2,0) tensor) is 0.

It would be nice to find a way to have the notational simplicity of using linear maps, but at the same time being able to talk about (m, n) tensors in general and the induced derivatives and other notions like contractions.

Otherwise we would need to define the derivative of a metric and then the derivative of a curvature tensor and so on.

[Sébastien Gouëzel]

I think there will have to be some amount of duplication, because formalized maths is not as fluid as paper maths for identifications. For instance, in paper maths, $\R$ and $\R^1$ are the same thing. And $\R \times \R$ and $\R^2$ are the same thing. It's not the same when formalizing: $\R^n$ is the space of functions from Fin nto $\R$, so the two identifications above fail. In the same way, if you define (m, n) tensors as $E^{\otimes m} \otimes (E^*)^{\otimes n}$, then a vector is not a (1, 0) tensor, a metric (in the sense of a bilinear map) is not a (0, 2) tensor, and so on. So developing the theory for general (m, n) tensors would not contain the theory for the usual objects...

[Dominic Steinitz]

Jens Lindekamp said:

My 2 cents as a lean newbie having some background in Riemannian Geometry (though that is a few years ago, I made my PhD in 2002 ;-)): I think we need to introduce tensor bundles in the form of multilinear maps from k factors of TM and l factors of T*M to k (or R/C) to really make a step forward.

In general, we need the tensor bundles to define:

1. Metrics as (2,0) tensors
2. The Riemmanian curvature as (3,1) tensor
3. Ricci curvature as (2,0) tensor
4. Torsion of an affine connection as (2,1) tensor (this is necessary to introduce the Levi-Civita connection which is torsion-free and the basis for (Pseudo-) Riemannian Geometry.
5. Differential forms as alternating (k,0) tensors. (And go to deRham cohomology from there....)

And potentially a few more, but that's more than enough....

I thought of defining a VectorBundleCore with a subtype of MultiLinearMap as fibres based on the TangentBundle. The construction could be done based on any vector bundle, but in practice, we would only need multilinear maps / tensors on the tangent bundle.

One could also introduce a general notion of general tensor products for vector bundles, but that's probably much more complex, and probably not needed at all for differential geometry.

Based on this, we could consider metrics "just" as a special case (k = 2, l = 0) of the tensor bundle.

Maybe it's only slightly more complex to create such a tensor bundle instead of the cotangent bundle as bundle of linear maps to k, metrics as bilinear maps to k etc.

Having said that - I'm not yet able to deal with VectorBundleCore, so I'm probably (surely) missing subtle details of the implementation....

I'd much rather follow Cartan and define connections via a principal G-bundle and then curvature is a Lie Algebra-valued 2-form.

I haven't thought about this as much but torsion probably ought to be done via a soldering form.

But I don't know the work on forms is progressing.

[Michael Rothgang]

I believe Sam Lindauer is working these (in a project depending on mathlib) - and Yury Kudryashov has gradually been upstreaming some of the prerequisites. There's still a significant gap between these.

[Michael Lee]

Patrick Massot said:

We simply need a version of docs#exists_smooth_forall_mem_convex_of_local for non-trivial vector bundles.

Would really appreciate if you took a glance here at the results I've added for this:

https://github.com/leanprover-community/mathlib4/blob/2d586707a31447b0735008e808232bd5f4b21892/Mathlib/Geometry/Manifold/PartitionOfUnity.lean#L628-L756

I'm happy to raise this as a PR on its own to break the reviewing effort up if you approve.

[Michael Rothgang]

At first glance, that looks like a useful statement - please make a PR!

[Michael Lee]

Michael Rothgang said:

At first glance, that looks like a useful statement - please make a PR!

Done!

https://github.com/leanprover-community/mathlib4/pull/24966

[Michael Lee]

If you'd like, I can also redo the proof of docs#exists_contMDiffOn_forall_mem_convex_of_local to show that it's a special case.

[Michael Rothgang]

Thanks for making the PR! I was about to ask you for that - there's no need to duplicate the same proof twice.

[Michael Lee]

@Michael Rothgang Replied to your PR comment, there's now a golfed proof of exists_contMDiffOn_forall_mem_convex_of_local that uses exists_contMDiffOn_section_forall_mem_convex_of_local directly. Thanks again!

[Dominic Steinitz]

Here's a small step on the way to the Ehresmann connection (https://github.com/leanprover-community/mathlib4/pull/23426)

import Mathlib.Analysis.Normed.Ring.Basic
import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Topology.FiberBundle.Basic
import Mathlib.Geometry.Manifold.ChartedSpace
import Mathlib.Geometry.Manifold.IsManifold.Basic
import Mathlib.Geometry.Manifold.Algebra.LieGroup
import Mathlib.LinearAlgebra.UnitaryGroup
import Mathlib.Topology.FiberBundle.Basic


open Matrix Bundle Manifold

structure GBundleCore (ι : Type*) (B : Type*) [TopologicalSpace B]
  (F : Type*) [TopologicalSpace F]
  (G : Type*) [Group G] [MulAction G F] extends FiberBundleCore ι B F where
  coordChange_structure_group :
    ∀ i j, ∀ x ∈ baseSet i ∩ baseSet j, ∃ g : G, ∀ v : F, coordChange i j x v = g • v

open RightActions

class SmoothLeftGAction
{𝕜 : Type*} [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞)
{E_G : Type*} [NormedAddCommGroup E_G] [NormedSpace 𝕜 E_G]
{E_M : Type*} [NormedAddCommGroup E_M] [NormedSpace 𝕜 E_M]
{H_G : Type*} [TopologicalSpace H_G] (I_G : ModelWithCorners 𝕜 E_G H_G)
{H_M : Type*} [TopologicalSpace H_M] (I_M : ModelWithCorners 𝕜 E_M H_M)
(G : Type*) [TopologicalSpace G] [ChartedSpace H_G G] [Group G] [LieGroup I_G n G]
(M : Type*) [TopologicalSpace M] [ChartedSpace H_M M]
[MulAction G M]
[IsManifold I_G n G]
[IsManifold I_M n M] : Prop where
  (smooth_smul : ContMDiff (I_G.prod I_M) I_M ⊤ (fun p : G × M => p.1 •> p.2))

class SmoothRightGAction
  {𝕜 : Type*} [NontriviallyNormedField 𝕜] (n : WithTop ℕ∞)
  {E_G : Type*} [NormedAddCommGroup E_G] [NormedSpace 𝕜 E_G]
  {E_M : Type*} [NormedAddCommGroup E_M] [NormedSpace 𝕜 E_M]
  {H_G : Type*} [TopologicalSpace H_G] (I_G : ModelWithCorners 𝕜 E_G H_G)
  {H_M : Type*} [TopologicalSpace H_M] (I_M : ModelWithCorners 𝕜 E_M H_M)
  (G : Type*) [TopologicalSpace G] [ChartedSpace H_G G] [Group G] [LieGroup I_G n G]
  (M : Type*) [TopologicalSpace M] [ChartedSpace H_M M]
  [MulAction (MulOpposite G) M]
  [IsManifold I_G n G]
  [IsManifold I_M n M]
  : Prop where
  smooth_smul : ContMDiff (I_M.prod I_G) I_M ⊤ (fun p : M × G => p.1 <• p.2)

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {n : WithTop ℕ∞}
variable {E_G E_M : Type*} [NormedAddCommGroup E_G] [NormedAddCommGroup E_M]
variable [NormedSpace 𝕜 E_G] [NormedSpace 𝕜 E_M]
variable {H_G H_M : Type*} [TopologicalSpace H_G] [TopologicalSpace H_M]
variable {G : Type*} [TopologicalSpace G] [ChartedSpace H_G G] [Group G]
variable {M : Type*} [TopologicalSpace M] [ChartedSpace H_M M]
variable {I_G : ModelWithCorners 𝕜 E_G H_G}
variable {I_M : ModelWithCorners 𝕜 E_M H_M}
variable [LieGroup I_G n G]
variable [IsManifold I_G n G] [IsManifold I_M n M]
variable [MulAction G M] [SmoothLeftGAction n I_G I_M G M]

open MulOpposite

instance mulAction_op_of_left [Group G] [MulAction G M] : MulAction (Gᵐᵒᵖ) M where
  smul g m := (unop g)⁻¹ • m
  one_smul := by
    intro b
    have h1 : (1 : G) • b = b := MulAction.one_smul b
    have h3 : unop (1 : Gᵐᵒᵖ)⁻¹ •> b = b := by rw [<-inv_one] at h1; exact h1
    exact h3

  mul_smul := by
    intro g₁ g₂ m
    have h1 : (unop (g₁ * g₂))⁻¹ •> m = (unop g₁)⁻¹ • ((unop g₂)⁻¹ • m) := by
      calc
      (unop (g₁ * g₂))⁻¹ •> m
        = (unop g₂ * unop g₁)⁻¹ •> m       := by rw [unop_mul]
      _ = ((unop g₁)⁻¹ * (unop g₂)⁻¹) •> m := by rw [_root_.mul_inv_rev]
      _ = (unop g₁)⁻¹ • ((unop g₂)⁻¹ • m)  := by rw [MulAction.mul_smul]
    exact h1

instance SmoothRightGAction_of_Left
  [MulAction G M]
  [LieGroup I_G ⊤ G]
  [ IsManifold I_M ⊤ M]

  [SmoothLeftGAction ⊤ I_G I_M G M] :
  SmoothRightGAction ⊤ I_G I_M G M where

  smooth_smul := by
    let f : M × G → G × M := fun (p, g) => (g⁻¹, p)
    have hf : ContMDiff (I_M.prod I_G) (I_G.prod I_M) ⊤ f := by
      apply ContMDiff.prodMk
      · exact ContMDiff.comp (contMDiff_inv I_G ⊤) contMDiff_snd
      · exact contMDiff_fst
    exact ContMDiff.comp (SmoothLeftGAction.smooth_smul ⊤) hf

universe uK uB uF uH uI uG uP

structure PrincipalBundleCore
  (ι : Type uP)
  {𝕜 : Type uK} [NontriviallyNormedField 𝕜]
  {n : WithTop ℕ∞}
  {E_B : Type uB} {E_F : Type uF} {E_G : Type uG}
  [NormedAddCommGroup E_B] [NormedSpace 𝕜 E_B]
  [NormedAddCommGroup E_F] [NormedSpace 𝕜 E_F]
  [NormedAddCommGroup E_G] [NormedSpace 𝕜 E_G]
  {H_B : Type uH} {H_F : Type uI} {H_G : Type uG}
  [TopologicalSpace H_B] [TopologicalSpace H_F] [TopologicalSpace H_G]
  {I_B : ModelWithCorners 𝕜 E_B H_B}
  {I_F : ModelWithCorners 𝕜 E_F H_F}
  {I_G : ModelWithCorners 𝕜 E_G H_G}
  (B : Type uB) [TopologicalSpace B] [ChartedSpace H_B B] [IsManifold I_B n B]
  (F : Type uF) [TopologicalSpace F]
  [TopologicalSpace G] [ChartedSpace H_G G] [Group G] [LieGroup I_G n G]
  (core : FiberBundleCore ι B F)
  [MulAction (MulOpposite G) (TotalSpace F (core.Fiber))]
  [ChartedSpace (ModelProd H_B H_F) (TotalSpace F core.Fiber)]
  [IsManifold (ModelWithCorners.prod I_B I_F) n (TotalSpace F core.Fiber)]
  [SmoothRightGAction n I_G (ModelWithCorners.prod I_B I_F) G (TotalSpace F core.Fiber)]
  where
  (respects_fibres : ∀ (p : TotalSpace F (core.Fiber)) (g : G), core.proj (p <• g) = core.proj p)
  (is_free : ∀ (p : TotalSpace F (core.Fiber)) (g : G), p <• g = p → g = 1)
  (is_transitive : ∀ (p q : TotalSpace F (core.Fiber)),
    core.proj p = core.proj q → ∃ g : G, p <• g = q)

[Sébastien Gouëzel]

I had a go at the definition of Riemannian manifolds in Mathlib, in #25347 (not designed to be merged, it's just to show the current state). It's somewhat orthogonal to the above discussion, because I'm not trying to show that a Riemannian metric exists, instead I'm trying to set up typeclasses so that one can work with Riemannian manifolds (for instance, I want the tangent spaces to be inner product spaces, but more importantly I want typeclass inference to be aware of this, to be able to use all our tools). The description of the PR in #25347 says more about the design, but let me mention a difficulty.

The tangent spaces to a manifold always have a topological structure (in fact a topological vector space structure) because we use it all the time. So if you want to work with a Riemannian manifold you can not make the usual incantations and add [∀ x, InnerProductSpace ℝ (TangentSpace I x)] because this creates a diamond, with two different topologies on the tangent spaces. Instead, I introduce a new class [RiemannianBundle (fun (b : M) -> TangentSpace I b)], containing the data of inner product spaces on the fibers (as sections of the bundle of continuous bilinear maps with positivity and symmetry conditions), compatible with the topology, and from these I register inner product structures on the tangent spaces, without introducing diamonds. And on top of this I add Prop-valued classes registering whether the inner product varies continuously, or smoothly, with the base point.

The design is a little bit complicated, and it is not battle-tested because I haven't proved nontrivial results with these definitions. But still, it looks pretty sound to me, and useful. I'm happy to take comments and suggestions! If people like it, I could even start PRing some bits.

[Matteo Cipollina]

This is truly a gift, thanks @Sébastien Gouëzel :)

If I'm not wrong, this sets up the ultimate typeclass infrastructure for Riemannian manifolds, and the diamond problem for InnerProductSpace on tangent spaces with RiemannianBundle.

I'm not sure you had a chance to look at my PR (#564 in PhysLean https://github.com/HEPLean/PhysLean/tree/master/PhysLean/Mathematics/Geometry/Metric
https://github.com/HEPLean/PhysLean/pull/564
), where I've tried to define the metric as a concrete data structure:

• PseudoRiemannianMetric: val (family of bilinear forms), symm, nondegenerate, smooth_in_charts' (smoothness of components in local charts), and negDim_isLocallyConstant.
• RiemannianMetric: Extends PRM with pos_def'.
• I also provide local InnerProductSpace structures on TangentSpace I x via TangentSpace.metricInnerProductSpace g x, requiring letI in practice.

It seems my RiemannianMetric structure could potentially provide the data for your ContMDiffRiemannianMetricconstructor. The bridge would likely be showing that smooth_in_charts' implies the ContMDiff of the metric section you use, and showing that the topology is compatible (the isVonNBounded condition).

Am I on the right track thinking these are complementary? Or do you see a different integration path? or none?

[Sébastien Gouëzel]

Yes, these have definitely the same kind of flavor, especially the data to construct the metric. There are some subtleties, though: pointwise smoothness, as you require, is not equivalent to full smoothness in general, and also nondegeneracy is in general not enough to ensure that the topology defined by the inner product is the same as the original one (which is why I have to include this additional von Neumann bounded condition). However, they are equivalent when the space is finite-dimensional, which is the situation you are considering if I understand correctly!

[Sébastien Gouëzel]

A comment on your PR to PhysLean: the line

noncomputable instance (x : M) : NormedAddCommGroup (TangentSpace I x) :=
  show NormedAddCommGroup E from inferInstance

is probably not a good idea if the plan is to put inner product spaces structures on the tangent spaces, as the two instances will conflict.

[Matteo Cipollina]

Sébastien Gouëzel ha scritto:

Yes, these have definitely the same kind of flavor, especially the data to construct the metric. There are some subtleties, though: pointwise smoothness, as you require, is not equivalent to full smoothness in general, and also nondegeneracy is in general not enough to ensure that the topology defined by the inner product is the same as the original one (which is why I have to include this additional von Neumann bounded condition). However, they are equivalent when the space is finite-dimensional, which is the situation you are considering if I understand correctly!

Thanks so much for the explanation and for looking at the PhysLean PR! This is super helpful :)

[Patrick Massot]

Michael Lee said:

Michael Rothgang Replied to your PR comment, there's now a golfed proof of exists_contMDiffOn_forall_mem_convex_of_local that uses exists_contMDiffOn_section_forall_mem_convex_of_local directly. Thanks again!

I left a review that I hope will be somewhat interesting. I’m sorry about the huge delay.

[Michael Rothgang]

#28056 (still heavily work in progress) will prove that every smooth finite rank real vector bundle (over a sigma-compact Hausdorff base) admits a smooth bundle metric.