riemannian geometry

Stream: maths

[Johan Commelin]

@Sebastien Gouezel How far are we from being able to define a Riemannian manifold? It seems to me that almost all the ingredients are in place. If so, that sounds like a pretty nice milestone!

[Sebastien Gouezel]

Not so close. The main missing block is to define the bundle of metrics. Two possible choices: define it by hand, or define a general mechanism associating to a vector bundle and a functor a new vector bundle. The general version would be better, but I have never played with the category theory library...

[Johan Commelin]

I see. I was thinking of the first approach, because I don't know this second construction. How does that work?

[Reid Barton]

If you have a functor, say, from (Vect, isos) to (Vect, isos), and it is continuous on Hom-sets in an appropriate sense, then given a vector bundle, you choose a trivialization, apply the functor to the fiber over each piece and to the transition maps, and use the resulting data to glue together a new vector bundle.

[Sebastien Gouezel]

Yes, this is the math version. The question is rather the Lean version :)

[Sebastien Gouezel]

For instance, if you have the tangent bundle with fibers T_x M, then the bundle with fiber (T_x M ⊗ T_x M)^* comes directly out of this construction, and this is the one in which a metric lives.

[Ruizhe Wan]

I see there are constructions on vector bundles including direct product and pullback. Have we defined the tensor product and the dual space of vector bundles yet? I think this is our last step before we could define the riemann metric.

[Heather Macbeth]

I think we should make metrics as sections of $\operatorname{Hom}(TM,\operatorname{Hom}(TM, \mathbb{R}))$ rather than as sections of $T^*M\otimes T^*M$, because tensor products of infinite-dimensional Banach spaces are a can of worms.

[Heather Macbeth]

But yes, @Floris van Doorn and I have written PRs for those things, though we (or rather I) haven't pushed them through review yet.

[Ruizhe Wan]

I think we could construct the pointwise tensor products of the tangent space and the cotangent space, so to avoid infinite dimension. Just like how we create the direct sum of two vector bundles, but we are using tensor product instead of direct product.

[Heather Macbeth]

I don't understand your comment. Are you proposing restricting to finite dimension? I do think it would be worth developing a parallel, finite-dimensional theory of differential geometry eventually, but that will take time and it's easier for now to remain in general (possibly infinite) dimension.

Or if you are asking what the subtleties are with tensor products in infinite dimension, you can read Yury and Sébastien's responses to the first question I posted on this message board.

[Trebor Huang]

A can of norms

[Ruizhe Wan]

Oh I see the problem of tensor product of infinite dimension. Thanks for the link.