Help wanted: notation for differential forms

Stream: mathlib4

[Yury G. Kudryashov]

In #29985 I define the exterior derivative of a differential form on a normed space. Currently, this PR does not introduce any notation for k-forms, because there are many types that compete for notation:

• bundled C^r-smooth or unbundled;
• on a normed space or on a manifold;
• k-forms or the graded module (ring if the codomain is an algebra, e.g., the base field) of all k-forms over all k

Which of the combinations should we have in Mathlib? What notation would you use?

[Sébastien Gouëzel]

First and foremost, I'd say we need the unbundled notion (i.e., no embedded smoothness) on vector spaces, and then on manifolds. I would start with k-forms (i.e., not the graded module) because all the operations really depend on k, so putting them together comes afterwards, I think.

[Sébastien Gouëzel]

Bundling is bad, because when you work with manifolds you work locally in charts, and then you never get a form which is a genuine C^k form on the whole vector space, only locally. Working with predicates works best in this kind of situation. This is what I did for vector fields, and I was really happy with the result.

[Yury G. Kudryashov]

We're going to need bundled forms, at least for infinitely smooth forms, to define de Rham cohomology.

[Sébastien Gouëzel]

Sure. But only later.

[Dominic Steinitz]

Do these notations support vector-valued forms and Lie algebra-valued forms?

[Yury G. Kudryashov]

There is no notation for now. If you're asking about definitions, then I deal with k-forms defined on a normed space taking values in a normed space for now.

[Dominic Steinitz]

I am thinking about Ω^k(M, 𝔤) which denotes a Lie algebra-valued k-form taking values in a Lie algebra 𝔤. But maybe that is not what is meant by notation here.

Why values in a normed space? I really want Lie algebra valued forms.

I still count myself as a noob so apologies if I have missed the point.

[Yury G. Kudryashov]

Why values in a normed space?

The main use case for many people is F = Real.

I really want Lie algebra valued forms.

Don't you have a normed space structure on the Lie algebra? Or only a topological vector space structure? In the latter case, we can try to generalize some parts of the theory to TVS, but it depends on a pending refactor of tangentCone.

[Dominic Steinitz]

Curvature is a Lie algebra-valued 2-form and a connection is a Lie algebra-valued 1-form. Probably one can put a normed space structure on finite dimensional Lie algebras although it would feel a bit artificial; for infinite dimensional Lie algebras I have no idea. For my purposes, I guess I can use them as they are.

[Yury G. Kudryashov]

What do you assume about the manifold & the fiber bundle when you say that these forms take values in a Lie algebra?

[Scott Carnahan]

As I understand it, G-connections live in an AddTorsor under Lie(G)-valued 1-forms, but should not be identified with 1-forms.

[Dominic Steinitz]

Yury G. Kudryashov said:

What do you assume about the manifold & the fiber bundle when you say that these forms take values in a Lie algebra?

That is a great question and one which I have been pondering myself. I don't have an answer and it may take me time to arrive at one.

EDIT: There doesn't seem to be a standard reference that says "to define smooth Foo-valued differential forms, Foo must satisfy properties X, Y, Z." It's treated as obvious/implicit (not to me though). I guess I could ask on Mathoverflow if someone wants to formulate the question more precisely.

EDIT: For reference there are some interesting hits in Mathoverflow

[Dominic Steinitz]

Scott Carnahan said:

As I understand it, G-connections live in an AddTorsor under Lie(G)-valued 1-forms, but should not be identified with 1-forms.

I don't understand your comment. Curvature as a Lie algebra-valued 2-form is fairly standard: Differential Geometry (Sharpe) or Gauge Theory and Variational Principles (Bleecker) or even Wikipedia. And curvature is derived from the Lie algebra-valued 1-form.

[Oliver Nash]

@Dominic Steinitz What Scott is saying is that the difference of two connections is a ($\mathfrak{g}$-valued) 1-form. If there is some canonical connection to act as origin e.g., a trivial bundle has the trivial connection (aka product connection) then one can view a connection as a 1-form but it's not really the correct POV. In reality, a connection is a differential operator.

OTOH, curvature is, as you say, a genuine ($\mathfrak{g}$-valued) 2-form.

[Dominic Steinitz]

I posted a question in mathoverflow.

[Dominic Steinitz]

Dominic Steinitz said:

I posted a question in mathoverflow.

which has attracted 4 downvotes :-(

[Dominic Steinitz]

But this comment at least seems useful

You could in principle take your gizmo to be practically anything, but then you don't have exterior differentiation or wedge product, or even a vector space. If you have any real vector you can talk about differential forms valued in it, and these even form a (graded) vector space. If you have a bundle 𝐴 of ℝ-algebras you can talk about the vector space of 𝐴-valued differential forms and have a wedge. It's not so much having blah-valued forms, but the real question is what algebraic structure your blah-valued forms make up.

@Yury G. Kudryashov does that help?

[David Michael Roberts]

I will interject to say that (principal) connections are differential forms (on the total space of the bundle), though the space of them isn't a vector subspace of all differential forms. They form an affine subspace of a space of differential forms, and as such are modelled on a different vector space (of forms) to the one this affine space sits inside.

[David Michael Roberts]

@Oliver Nash are you thinking of connections on vector bundles when you say they are differential operators?

[Dominic Steinitz]

https://math.stackexchange.com/questions/315235/reference-for-lie-algebra-valued-differential-forms pointed me a Loring Tu's excellent book and I am now reading the relevant section.