Topic: riemannian geometry
Johan Commelin (Jan 24 2020 at 18:35):
@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 (Jan 24 2020 at 19:46):
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 (Jan 24 2020 at 20:44):
I see. I was thinking of the first approach, because I don't know this second construction. How does that work?
Reid Barton (Jan 24 2020 at 21:48):
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 (Jan 24 2020 at 21:56):
Yes, this is the math version. The question is rather the Lean version :)
Sebastien Gouezel (Jan 24 2020 at 21:59):
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.
Last updated: May 11 2021 at 15:12 UTC