# Zulip Chat Archive

## Stream: maths

### 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