Formalizing Riemannian geometry

Stream: new members

[Michael Lee]

I'm a former mathematician and a professional programmer (very new to Lean), and I'm hoping to make some contributions to mathlib in the way of differential geometry. I notice that there's a nice formalization already of smooth manifolds with corners, tangent bundles, and smooth sections of vector bundles. I'd like to get started formalizing a notion of Riemannian metric so that I can build out more advanced concepts. However, I'm quickly getting stuck on some kind of type inference issue. Why does the following not work?

import Mathlib.Geometry.Manifold.SmoothManifoldWithCorners
import Mathlib.Geometry.Manifold.VectorBundle.SmoothSection
import Mathlib.Geometry.Manifold.VectorBundle.Tangent

open scoped Manifold

noncomputable section

section General

namespace Riemannian

variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type _} [TopologicalSpace H]
  (I : ModelWithCorners ℝ E H)


def SmoothVectorField (M : Type _) [TopologicalSpace M] [ChartedSpace H M] [SmoothManifoldWithCorners I M] : Type _ := (SmoothSection I E (TangentBundle I M))

There's a message typeclass instance problem is stuck, it is often due to metavariables with the annotation FiberBundle E ?m.70869, but I'm not really understanding how to track down the issue. I'm using VS Code, and if I mouse over ?m.70869, I get more expressions involving metavariables, but it's pretty hard to follow where they're coming from and what condition might be unsatisfied. Thanks, all!

[Michael Lee]

Doh... of course type coercion failed. After looking closer at the definitions of SmoothSection and TangentBundle, I realized I had to do this instead:

def SmoothVectorField (I : ModelWithCorners ℝ E H) (M : Type _) [TopologicalSpace M] [ChartedSpace H M]
  [SmoothManifoldWithCorners I M] : Type _ := (SmoothSection I E (TangentSpace I : M → Type _))

[Moritz Doll]

@Heather Macbeth wrote down a formalization of the Riemannian metric not too long ago, maybe it is closer to mathlib-ready now?

[Michael Lee]

Moritz Doll said:

Heather Macbeth wrote down a formalization of the Riemannian metric not too long ago, maybe it is closer to mathlib-ready now?

Very exciting! @Heather Macbeth, I'd love to see how you've gone about implementing this, if you don't mind sharing. Maybe I could contribute to mathlib diffgeo in the future.