Cotangent Bundle as a Manifold

Stream: Is there code for X?

[Dominic Steinitz]

I have found that the tangent bundle has an instance as a manifold but not for the cotangent bundle; indeed I couldn’t even find a ChartedSpace instance.

[Sébastien Gouëzel]

Given two bundles, we have ways to construct new bundles (endowed automatically with their manifold structure). The cotangent bundle is the bundle of continuous linear maps from the tangent space to the real line (seen as a trivial bundle), so it fits in this framework.

[Dominic Steinitz]

That’s great - where should I look for more information?

[Kevin Buzzard]

One possible future answer to this could be "in Imperial's course notes" but I am not competent to write the code myself. My vision for the course notes is that they become a collection of examples of how to state undergraduate-level mathematics in Lean (and I was certainly taught about cotangent bundles for finite-dimensional smooth real manifolds as an undergrad).

[Dominic Steinitz]

I didn’t mean the cotangent bundle mathematically - I also learnt that as an undergraduate and even that one can construct it without the existence of the tangent bundle (a fun fact) - what I meant was the Lean documentation that tells one how to construct a new bundle from old with its corresponding IsManifold instance

[Kevin Buzzard]

Right, and that's what I mean too -- the Imperial repo would love to contain Lean code which explains how to do this mathematical construction in Lean (and also tensor products of finite-dimensional vector bundles over a finite-dimensional smooth manifold).

[Michael Rothgang]

I'll be teaching a class on differential geometry in Lean in January. Perhaps I'll have time for vector bundles also, and then this could also live there. (And of yourse, you're welcome to steal these, Kevin. Or tell me everything that could be improved there, so I can also improve those!)

[Sébastien Gouëzel]

Here is a snippet showing that typeclass inference founds by itself the manifold structure on the total space on the cotangent bundle, and how to express the fact that a section of the cotangent bundle is smooth.

import Mathlib

open Manifold Bundle
open scoped ContDiff Topology

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n n' : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
  [IsManifold IB ∞ B]

#synth IsManifold (IB.prod 𝓘(ℝ, EB →L[ℝ] ℝ)) ∞
    (TotalSpace (EB →L[ℝ] ℝ) (fun (b : B) ↦ (TangentSpace IB b →L[ℝ] ℝ)))

lemma foo (g : Π (x : B), TangentSpace IB x →L[ℝ] ℝ) :
    ContMDiff IB (IB.prod 𝓘(ℝ, EB →L[ℝ] ℝ)) ∞
      (fun b ↦ TotalSpace.mk' (EB →L[ℝ] ℝ) b (g b)) := by
  sorry

@Michael Rothgang, I couldn't get the nice elaborators to work here, possibly because it's just impossible to guess everything there.

[Sébastien Gouëzel]

Note that this would already be enough to define, say, the curvature of a Riemannian manifold (as a bilinear map into the endomorphisms of the tangent space) and to state that this is a smooth map:

variable [RiemannianBundle (fun (x : B) ↦ TangentSpace IB x)]
  [IsContMDiffRiemannianBundle IB ∞ EB (fun (x : B) ↦ TangentSpace IB x)]
  [EMetricSpace B] [IsRiemannianManifold IB B]

def curvature (b : B) : TangentSpace IB b →L[ℝ] TangentSpace IB b →L[ℝ]
    (TangentSpace IB b →L[ℝ] TangentSpace IB b) := sorry

theorem contMDiff_curvature :
    ContMDiff IB (IB.prod 𝓘(ℝ, EB →L[ℝ] EB →L[ℝ] EB →L[ℝ] EB)) ∞
      (fun (b : B) ↦ TotalSpace.mk'
      (E := fun (b : B) ↦ TangentSpace IB b →L[ℝ] TangentSpace IB b →L[ℝ]
        (TangentSpace IB b →L[ℝ] TangentSpace IB b))
      (EB →L[ℝ] EB →L[ℝ] EB →L[ℝ] EB) b (curvature b)) := sorry

[Sébastien Gouëzel]

(This is quite a mouthful to state as Lean is a little bit confused by the complexity of the objects, so one has to help it through additional type information, but hopefully we will get more robust elaborators that will hide all this behind notation)

[Michael Rothgang]

About the elaborators: indeed, that is not supported yet. In the following code, you get an error "Failed with error: Having a TotalSpace as source is not yet supported" - i.e., this is simply not implemented yet. Help is welcome, as always! (The other error might be everything being hard to guess: in the snippet I provided lots of type information so there should be no more ambiguity left.)

Code with diagnostic output

import Mathlib

open Manifold Bundle
open scoped ContDiff Topology

variable
  {EB : Type*} [NormedAddCommGroup EB] [NormedSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n n' : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
  [IsManifold IB ∞ B]

#synth IsManifold (IB.prod 𝓘(ℝ, EB →L[ℝ] ℝ)) ∞
    (TotalSpace (EB →L[ℝ] ℝ) (fun (b : B) ↦ (TangentSpace IB b →L[ℝ] ℝ)))

set_option trace.Elab.DiffGeo.MDiff true

lemma foo (g : Π (x : B), TangentSpace IB x →L[ℝ] ℝ) :
    CMDiff ∞
      ((fun b ↦ TotalSpace.mk' (EB →L[ℝ] ℝ) b (g b)) : B → TotalSpace (EB →L[ℝ] ℝ) fun b => TangentSpace IB b →L[ℝ] ℝ) := by
  sorry