Definition for differential forms

Stream: maths

[Dylan Ede]

Hi, I'm pretty new to Lean. I've worked through all the exercises in the current version of Mathematics in Lean and that's about it.

With that out of the way, I'm mostly interested in differential geometry in Lean (partially to aid in my learning of DG), and I thought I'd have a go at defining cotangent spaces and bundles, and differential forms. Specifically, do these extra definitions for geometry.manifold.basic_smooth_bundle look about right?

After the definition of tangent_space:

@[nolint unused_arguments, derive [has_coe_to_fun, semi_normed_group, semi_normed_space 𝕜, normed_group, normed_space 𝕜]]
def cotangent_space (x : M) : Type* := normed_space.dual 𝕜 E

def differential_form := Π (x: M), exterior_algebra 𝕜 (cotangent_space I x)

After the definition of tangent_bundle:

@[nolint has_inhabited_instance, reducible] -- is empty if the base manifold is empty
def cotangent_bundle := Σ (x : M), cotangent_space I x

[Dylan Ede]

My definition of differential_form looks like this now:

@[derive [inhabited, semiring, ring, algebra 𝕜]]
def differential_form := Π (x: M), exterior_algebra 𝕜 (cotangent_space I x)

In order for this to be useful, do I now need to wrap all of the results in linear_algebra.exterior_algebra so that they apply to differential_form?

[Adam Topaz]

I don't think this definition of differential_form is correct.

[Adam Topaz]

All this is saying is that to each point x you assign some element (with no restrictions whatsoever!) in the exterior algebra of the dual of the tangent space at x.

[Adam Topaz]

I'm an algebraic geometer so my inclination is to define things as sections of some sheaf, but I hope that someone who is more familiar with the manifolds library should be able to direct you to a better definition.

[Dylan Ede]

OK, I thought there might be a problem since I was struggling with the definition of section to use. I was basing things on https://ncatlab.org/nlab/show/differential+form and https://mathworld.wolfram.com/BundleSection.html

[Adam Topaz]

As a toy example, perhaps it's worthwhile to write down the definition of a vector field as a section to the tangent bundle

[Dylan Ede]

I've done a bit more reading, and it seems like the main (only?) thing missing is that some definitions require the section/map to be continuous. Indeed, that is what the Wikipedia definition requires. I had previously found a definition that suggested that sometimes you don't want to require that a differential form is continuous, but now I can't find it.

[Adam Topaz]

If you're working with $C^p$ manifolds, you would want to require the section to be $C^p$. So when p is 0, that's continuity, and when p is infinity, that means smooth

[Dylan Ede]

OK, thanks, I think I see what I need to do now. I think differential_form needs to look something like

def differential_form_bundle := Σ (x: M), exterior_algebra 𝕜 (cotangent_space I x)
def differential_form := C^∞⟮I, M; I, differential_form_bundle I M⟯

But of course that means that I need to implement all the necessary type classes on differential_form_bundle, and contangent_bundle as well, probably with definitions of differential_form_bundle_core and cotangent_bundle_core to help with that.