Zulip Chat Archive

Stream: maths

Topic: Definition for differential forms


Dylan Ede (May 14 2021 at 17:42):

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 (May 14 2021 at 23:20):

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 (May 14 2021 at 23:22):

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

Adam Topaz (May 14 2021 at 23:24):

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 (May 14 2021 at 23:25):

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 (May 14 2021 at 23:27):

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 (May 14 2021 at 23:46):

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 (May 15 2021 at 13:37):

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 (May 15 2021 at 13:51):

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

Dylan Ede (May 15 2021 at 14:23):

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.


Last updated: Dec 20 2023 at 11:08 UTC