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.

[Johan Commelin]

What's the status for differential forms nowadays? How far are we from a workable definition? (In or outside of mathlib.)

[Patrick Massot]

There are have been discussion but I don’t think there is any concrete progress.

[Johan Commelin]

Aha, that's sorta what I expected.

[Dominic Steinitz]

Patrick Massot said:

There are have been discussion but I don’t think there is any concrete progress.

I was hoping to use these to define a connection on a principal bundle (where the forms are Lie algebra-valued).

[Yury G. Kudryashov]

I'm slowly pushing towards this goal, but I'm too busy at my day job.

[Kevin Buzzard]

Computing de Rham cohomology of the n-sphere would be a really nice project.

[Kevin Buzzard]

You could even imagine a top down approach.

[Yury G. Kudryashov]

Next PR towards this goal: #17200

[Norman Paskus]

The R algebra of differential forms can be a commutative differential graded algebra, but unless a connection is flat it does not satisfy the square zero condition.

We may want to decide what kind of thing the ring of differential forms is, taking cue from the work that @Floris van Doorn and @Heather Macbeth did in Lean 3.

If these are taken as R algebras (and R vector spaces for the connections) with the differential separate then this could allow one to form the full structure separately.

The rings of smooth and holo
orphic functions as R algebras could be good to start with, and then possibly Omega^1. Maybe Lambda^* for an A module as well. One could use tensor and kernel for these, and the R module for a free basis.

[Yury G. Kudryashov]

My current plan is to use a vector bundle of docs#ContinuousAlternatingMap s

[Yury G. Kudryashov]

This way the construction isn't tied to the finite dimensional case.

[Norman Paskus]

@Yury G. Kudryashov thanks for this. It seems like you and Dominic want to use vector bundles.

There’s been a lot of interest recently in getting differential forms to work. Do you have some more extensive blueprints up?

It would be really cool if the rw[] ends up producing some normal forms. I wanted to be able to do things with formal expressions vaguely like this:

4 ^ (d x) ^ (d z)

rw[pullback f]

…

so its formal algebra starting with bundles.

[Yury G. Kudryashov]

I don't have any blueprints, just some plans in my head.

[Yury G. Kudryashov]

The next step towards the wedge product is to redefine docs#AlternatingMap.domCoprod without tensor product, and probably without sticking to docs#Sum for the new index type. I think that the general definition should take 2 embeddings and a proof that their Set.ranges are IsCompl.

[Yury G. Kudryashov]

It should take a bilinear map as an argument instead.

[Yury G. Kudryashov]

Similarly to how docs#MeasureTheory.convolution is defined in Mathlib.

[Yury G. Kudryashov]

Pullback is just docs#ContinuousAlternatingMap.compContinuousLinearMap

[Eric Wieser]

What's the advantage of dropping Sum? That sounds like something the caller can translate through

[Eric Wieser]

(I can see the argument that going through TensorProduct.lift is slow and probably awkward for typeclass reasons)

[Yury G. Kudryashov]

Reason to drop TensorProduct: we don't have a topology on TensorProduct, and I want a version for ContinuousAlternatingMaps.

[Yury G. Kudryashov]

Reason for generalizing codomain: the main application in analysis is going to use Fin k, Fin l, and Fin n, n = k + l.

[Yury G. Kudryashov]

We can have a generic version domCoprodOfIsCompl and specializations to Sum and Fin.

[Antoine Chambert-Loir]

Why would you have more natural topologies on alternating maps than on tensor products?

[Yury G. Kudryashov]

For ContinuousAlternatingMaps, the natural topology comes from the topology/norm on ContinuousMultilinearMaps.

[Yury G. Kudryashov]

For the tensor product, there are multiple non-compatible topologies in the infinite dimensional space, and we haven't fixed one of them as "the main one" in Mathlib yet.

[Anatole Dedecker]

Yes really it's just that we chose a defaut topology on continuous multilinear maps (that of bounded convergence) but we didn't do such a choice (and we probably don't want to ?) on the tensor product.