Don't understand TangentBundle & sections

Stream: new members

[Jens Lindekamp]

Hi,

I have to admit, I'm pretty new at lean, so my question just shows that I have a lot to learn...

In Mathlib we have TangentBundle I M to denote the tangent bundle of M and we also have sections in vector bundles s: C^n(I; F, V).
I would expect that I can describe a vector field on M as a section in the tangent bundle - but instead vector fields are always defined as Π (x : M), TangentSpace I x, but never as sections in the tangent bundle.

Can someone explain this?
Can we write a vector field as X: C^n(I; F, V) with appropriate F and V?

I'm afraid I can't get my head around it...

[Michael Rothgang]

Hi and welcome! Differential geometry is one of the hardest areas in mathlib to learn - so don't be afraid to ask questions. :-)

I find your question a bit hard to parse (but it's also late on my end). Can you explain what you mean by C^n(I; F, V)? I cannot easily find such notation. As far as I can tell, there is no special notation for sections. If you compare with e.g. docs#Bundle.zeroSection, you'll find that the zero section uses the same notation.

[Michael Rothgang]

Here's a guess: do you want your notation C^n(I; F, V) to mean C^n functions F \to V, read in the model I? If so, that's weaker than sections of a vector bundle --- because the latter also require that s(x) lie in the fibre at x (mere smoothness does not).

[Michael Rothgang]

A general hint for making your questions easier to follow: it helps a lot if you post an #mwe --- i.e. give enough details that I know what e.g. F and V are. Right now, I have to guess (and either have to wait for you to clarify, or may guess wrong --- both of which is less useful to you). Make it easy to help you :-)

[Matt Diamond]

@Jens Lindekamp did you mean docs#ContMDiffSection (Cₛ^n⟮I; F, V⟯)?

[Michael Rothgang]

Thank you, now I understand the question! The answer has to do with how vector fields are defined in mathlib. Let's compare with sections of vector bundles: there, you have Π (x : B), E x (to describe continuous sections of a bundle E over base B), and you have ContMDiffSection to describe sections of a C^n vector bundle which are C^n (w.r.t. the bundle's local trivialisations). There is no separate type for continuous bundle sections, as these are already expressed as dependent functions.

For vector fields, what you wrote Π (x : B), TangentSpace I x amounts to saying "this is a section", but you're not expressing the differentiability yet.

[Michael Rothgang]

Right now, there is no type "C^n vector fields" (as that would just be a special case of "ContMDiffSection"). To see some examples of how this is handled today, see e.g. docs#ContMDiffWithinAt.mpullbackWithin_vectorField_inter (hypothesis hV says "V is a C^n vector field") and the nearby lemmas.

[Michael Rothgang]

I wonder if introducing an abbrev "smooth vector field" would make those statements easier to read and prove. @Sébastien Gouëzel You wrote the original file; would you like to elaborate on why you made that choice?

[Sébastien Gouëzel]

Note that the doc is misleading, it doesn't show the statement as it is in the file, like:

ContMDiffWithinAt I I.tangent m
      (fun (y : M) ↦ (mpullbackWithin I I' f V s y : TangentBundle I M)) (s ∩ f ⁻¹' t) x₀

Here it's taking advantage of the coercion from the tangent space to the tangent bundle, to see mpullbackWithin I I' f V s y (which is a point in TangentSpace I M) as an element of TangentBundle I M. And then it's just talking of a map from the manifold M to the manifold TangentBundle I M, and asserting that this map is smooth.

We could definitely add an abbreviation for this, but since we wouldn't build an API around it (as the API around ContMDiff is already enormous and shouldn't be duplicated), I'm not sure if we would gain much.

[Jens Lindekamp]

Great, I'm new at lean, still learn about dependent type theory and picked "one of the hardest areas in lean to learn". Anyway, challenge accepted....

To get into lean I naively thought about a small (or not so small) project:

1. Define connections on differentiable vector bundles (work in progress, actually not so bad)
2. Specialise the general connections on vector bundles to affine connections on the tangent bundle, i.e. interprete TMas a special case of a vector bundle.
3. "Along the lines, if missing": describe sections as modules over the ring of diff. functions. This would be useful to formulate statements about vector fields and tensors. Having said that - can we consider covariant derivatives as derivations over rings and modules? Off-topic...
4. Proof basic properties of connections (define the torsion of an affine connection, proof its skew symmetric, pullbacks of connection)
5. Define tensor products of the tangent bundle as vector bundles over M. This would probably mean to define tensor products of topological vector bundles first etc. Arggh....

If this could be done, we could easily define a metric on M as a section in the symmetric tensor product, we could describe the curvature tensors (Riemmanian, Ricci) as sections in tensor bundles and immediately can state theorems like "M is a symmetric space iff R is parallel, i.e. the covariant derivative of R is the zero section"

Step 2 is where my question comes from. When I make a statement about sections in general vector bundles, I want to apply it to vector fields as sections in TM.

Because vector fields and tensors play a central role in differential geometry it might be a good idea to introduce structures / classes / shortcuts for these concepts. Maybe it would be just an enhancement of the ContMDiffSection API, after all, many concepts in diff. geom.are really sections in some tensor bundle.

This is why I want to make statements for ContMDiffVectorBundles and ContMDiffSection and define a vector field as an appropriate ContMDiffSection and apply the general statements to vector fields.

[Sébastien Gouëzel]

One of the lessons we have learned when doing analysis in Lean is that working with spaces of functions with a property (say, the space of continuous functions, or the space of smooth functions) or whatever, is usually not the thing to do, because it doesn't localize well. Often, you want to say that a function is continuous on a given open set, and deduce something from this property -- and if you have proved results on the space of all continuous functions, this will be of no use, because the function you're working this is not continuous globally. It turns out to be much more flexible and efficient to work with predicates, like "this function is continuous at this point" or "this function is continuous on this set" or "this function is smooth on this set".

You can have a look at the file on Lie bracket of vector fields in manifolds, say (https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean), and see that it's developed in this way, based on a similar file on vector fields in vector spaces. And you can see here why it's important to use the predicate approach here: if you have a global smooth vector field on a manifold, and look at it in a chart, then you get a vector field in a vector space which is not globally smooth, only in the range of the chart. So if you had set up a global theory of smooth vector fields on vector fields, it would be of no use to build the theory of vector fields on manifolds!

TLDR: don't use ContMDiffSection, use a section and a predicate that it's continuous / smooth / whatever you need to prove the theorem you're working on.

[Sébastien Gouëzel]

N.B.: For 2. in your message (interpret TM as a special case of a vector bundle), there is nothing to do, TM is already a vector bundle in mathlib.

[Jens Lindekamp]

Sébastien Gouëzel schrieb:

N.B.: For 2. in your message (interpret TM as a special case of a vector bundle), there is nothing to do, TM is already a vector bundle in mathlib.

I suppose then it is just me, not fully understanding type theory. Will check it out.

[Jens Lindekamp]

Concerning your comments on locality: I understand that locality is important, but still I'm probably to much influenced by the hand-waiving pen and paper approach to talk about global concepts and only localize "under the hood" if really necessary.
One would mostly talk about global vector fields, global metrics etc. even though all these are local phenomenons.

[Sébastien Gouëzel]

Here is an illustration of the properties of the tangent bundle in current mathlib:

import Mathlib

open scoped ContDiff

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners 𝕜 E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]

example : TopologicalSpace (TangentBundle I M) := by infer_instance
example : IsManifold I.tangent ∞ (TangentBundle I M) := by infer_instance
example : VectorBundle 𝕜 E (TangentSpace I : M → Type _) := by infer_instance
example : ContMDiffVectorBundle ∞ E (TangentSpace I : M → Type _) I := by infer_instance

[Sébastien Gouëzel]

Jens Lindekamp said:

One would mostly talk about global vector fields, global metrics etc. even though all these are local phenomenons.

That's the impression one gets from the pen-and-paper approach, and it's very misleading. In practice, when you start formalizing, you see that most of the time you don't talk about global vector fields -- even if you have a statement about global vector fields, to prove it you will start to localize, and then all the lemmas you need should be in local form, not global.

[Sébastien Gouëzel]

(For Riemannian metrics, I agree that one would mostly use the global object)

[Matteo Cipollina]

I've been trying to formalize a minimal set-up for Pseudo and Riemannian metric with a pragmatic approach for use within PhysLean and was planning to share it soon for criticisms/improvements . It is a WIP aiming to get a InnerProductspace on Riemannian Metric and it does not implement the predicate approach recommended by @Sébastien Gouëzel (thanks!), but I plan to change it after reading this as have been struggling to propagate dimensions automatically throughout and to implement the last bit, the final InnerProductSpace structure:
https://github.com/HEPLean/PhysLean/pull/501

[Matteo Cipollina]

If I understood well the predicate approach, the below refinement of the definition in https://github.com/HEPLean/PhysLean/pull/501 should reflect better: smoothness defined by charts (locality) and not defined as a section type but a predicate on val

import Mathlib
variable {𝕜 : Type u} [RCLike 𝕜]
variable {E : Type v} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E]
variable {H : Type w} [TopologicalSpace H]
variable {M : Type w} [TopologicalSpace M] [ChartedSpace H M] [ChartedSpace H E]
variable {I : ModelWithCorners 𝕜 E H} {n : ℕ∞}
@[ext]
structure PseudoRiemannianMetric
    (I : ModelWithCorners 𝕜 E H) (n : ℕ∞)
    [IsManifold I (n + 1) M]
    [inst_top : TopologicalSpace (TangentBundle I M)]
    [inst_fib : FiberBundle E (TangentSpace I : M → Type _)]
    [inst_vec : VectorBundle 𝕜 E (TangentSpace I : M → Type _)]
    [inst_cmvb : ContMDiffVectorBundle n E (TangentSpace I : M → Type _) I] : Type (max u v w) where
  /-- The metric tensor at each point `x : M`, represented as a continuous linear map
      `TₓM →L[𝕜] (TₓM →L[𝕜] 𝕜)`. Applying it twice, `(val x v) w`, yields `gₓ(v, w)`. -/
  protected val : ∀ (x : M), TangentSpace I x →L[𝕜] (TangentSpace I x →L[𝕜] 𝕜)
  /-- The metric is symmetric: `gₓ(v, w) = gₓ(w, v)`. -/
  protected symm : ∀ (x : M) (v w : TangentSpace I x), (val x v) w = (val x w) v
  /-- The metric is non-degenerate: if `gₓ(v, w) = 0` for all `w`, then `v = 0`. -/
  protected nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w : TangentSpace I x,
    (val x v) w = 0) → v = 0
  /-- The metric varies smoothly: Expressed in local coordinates via any chart `e`, the function
      `y ↦ g_{e.symm y}(mfderiv I I e.symm y v, mfderiv I I e.symm y w)` is `C^n` smooth on the
      chart's target `e.target` for any constant vectors `v, w` in the model space `E`. -/
  protected smooth_in_charts' : ∀ (x₀ : M) (v w : E),
    let e := extChartAt I x₀
    ContDiffWithinAt 𝕜 n
      (fun y => val (e.symm y) (mfderiv I I e.symm y v) (mfderiv I I e.symm y w))
      e.target (e x₀)

namespace PseudoRiemannianMetric

section RiemannianMetric

open PseudoRiemannianMetric Bundle ContinuousLinearMap

noncomputable section

variable {E_ℝ : Type v} [NormedAddCommGroup E_ℝ] [NormedSpace ℝ E_ℝ] [FiniteDimensional ℝ E_ℝ]
variable {H_ℝ : Type w} [TopologicalSpace H_ℝ]
variable {M_ℝ : Type w} [TopologicalSpace M_ℝ] [ChartedSpace H_ℝ M_ℝ] [ChartedSpace H_ℝ E_ℝ]
variable {I_ℝ : ModelWithCorners ℝ E_ℝ H_ℝ} {n : ℕ∞}

@[ext]
structure RiemannianMetric
  (I_ℝ : ModelWithCorners ℝ E_ℝ H_ℝ)
  (n    : ℕ∞)
  [i_man : IsManifold I_ℝ (n + 1) M_ℝ]
  [inst_top : TopologicalSpace (TangentBundle I_ℝ M_ℝ)]
  [inst_fib : FiberBundle E_ℝ (TangentSpace I_ℝ : M_ℝ → Type _)]
  [inst_vec : VectorBundle ℝ E_ℝ (TangentSpace I_ℝ : M_ℝ → Type _)]
  [inst_cmvb : ContMDiffVectorBundle n E_ℝ (TangentSpace I_ℝ : M_ℝ → Type _) I_ℝ] : Type (max v w) where
  toPseudoRiemannianMetric : PseudoRiemannianMetric I_ℝ n
    (inst_top := inst_top)
    (inst_fib := inst_fib)
    (inst_vec := inst_vec)
    (inst_cmvb := inst_cmvb)
  /-- `gₓ(v, v) > 0` for all nonzero `v`. -/
  pos_def' : ∀ x v, v ≠ 0 → toPseudoRiemannianMetric.val x v v > 0

[Kevin Buzzard]

Jens Lindekamp said:

Great, I'm new at lean, still learn about dependent type theory and picked "one of the hardest areas in lean to learn". Anyway, challenge accepted....

In return, if you accept this challenge, you will find a very supportive community here who are keen to get more differential geometry formalized and will always be happy to help with questions, however basic.

If you really are completely new to Lean, I would recommend going through at least some of #mil before attempting to write your own code, and also coming up with concrete goals (which you seem to have done) and discussing strategies for achieving them with the community before embarking on them (which you also seem to be doing). There is an art to formalization and not all of it is taught to mathematicians; you need to know more than the underlying mathematics, there are new principles, and design decisions which in some sense are not even mathematical, and which you will pick up by working on projects.

My impression is that one reason that not much differential geometry is done is that there are not many differential geometers using Lean, our community seems to skew far more algebraic for some reason. All the foundations are now there and projects such as yours will be great tests for them. You might even want to consider supplying tutorials as you work through projects, e.g. with PRs to #mil or even as worksheets to Imperial's course https://github.com/b-mehta/formalising-mathematics-notes . These notes typically take the form of a few files which show undergraduates how to say basic things like "let M be a smooth manifold and let T be its tangent bundle and let f be a smooth section of T" in Lean, or give very basic exercises in the theory just to get people started. The goal of the course is to get undergraduates formalizing results from their course notes, and the goal of the repository is to show them the absolute basics of setting things up so that they can confidently state the question they're working on.

[Jens Lindekamp]

@Matteo Cipollina Thank you for the link; I just had a quick look, but looks promising to me. I will spend more time on it to learn....

@Kevin Buzzard That was my impression as well - lot's of examples on algebra, number theory and others, but not so much on differential geometry.

I'm actually working through #mil, and also the other documentation, it's quite a learning curve, but no worries.

For now, I want to create a github project and use the standard documentation tools like doc-gen4 to formalize my rough ideas. I'm not brave enough yet to explain it to others, though of course the project will be public and I will post it.

[Dominic Steinitz]

I am also working on connections - my plan is to defined the Ehresmann connection on a principal bundle and then specialise to vector bundles. That makes the geometric content of the connection a bit clearer and takes away the mystery of the non-tensor bit of the usual definition of a connection. I have got as far as defining a G-bundle but not yet made it to the heady height of a principal G-bundle. Some code here: https://github.com/leanprover-community/mathlib4/pull/23426.

One thing I want to do is reproduce my article on what I call the Mercator connection (straight lines on it are the straight lines on the Mercator projection - they are not the shortest distance - so this connection must have torsion - but now we need soldering forms and forms don't yet exist in Mathlib so there's plenty to do)

I always like to have examples and I am very slowly groping towards deriving the local trivialisations for the Mobius bundle (it turns out you can define a bundle in Mathlib just by specifying the coordinate transformations). This was meant to be an easy step before moving on to connections - lol.

@Matteo Cipollina don't you need principal bundles for gauge fields? I plan to do an example of electromagnetism (U(1)).

[Jens Lindekamp]

Cool. I shortly thought about Ehresmann & principal bundles, but then decided to get linear connections under control first and rather focus on the applications to geodesics, Jacobi fields etc.

Maybe we can meet in the middle - we agree on the notion of connection on vector bundles. I specialize towards linear connection on tensor fields on TM with applications on (Pseudo-) Riemannian metrics while you spezialize from principal / Ehresmann to connections on vector bundles.

But given the fact that I still struggle with lean & mathlib, that's a bit ambitious on my side...

[Matteo Cipollina]

Dominic Steinitz ha scritto:

Matteo Cipollina don't you need principal bundles for gauge fields? I plan to do an example of electromagnetism (U(1)).

Yes, that would be essential for gauge fields, Yang-Mills etc. will check your repo :)

[Joseph Tooby-Smith]

@Dominic Steinitz If you wanted to contribute your example (when done) of electromagnetism through the U(1) bundle to PhysLean that would be very much appreciated.
(see also #PhysLean )

We have the more rudiments of EM already, but would be nice to make a step towards gauge field theory.

[Dominic Steinitz]

I would love to contribute my example but I am some way off defining a connection form so don't hold your breath.

[Dominic Steinitz]

I am trying to define a horizontal bundle as part of my attempt at defining an Ehresmann connection and following the discussion above about vector fields I have

import Mathlib

open Bundle FiberBundle Function Set
open IsManifold Manifold
open scoped ModelWithCorners

variable {E_base : Type*} [NormedAddCommGroup E_base] [NormedSpace ℝ E_base]
variable {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E_base H}
variable {M : Type*} [TopologicalSpace M] [ChartedSpace H M] {x : M}

section EhresmannConnection

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {H' : Type*} [TopologicalSpace H']
  {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type*} [TopologicalSpace M'] [ChartedSpace H' M']
  {x₀ : M}

variable {V : Π (x : M'), TangentSpace I' x}
variable {t : Set M'}

variable [IsManifold I' ⊤ M']

structure LocalFrame (I' : ModelWithCorners 𝕜 E' H') (M' : Type*)
  [TopologicalSpace M'] [ChartedSpace H' M'] [IsManifold I' ⊤ M']
  (index : Type*) [Fintype index] where
  submodule_at : (e : M') → Submodule 𝕜 (TangentSpace I' e)
  smooth_local : ∀ (x₀ : M') (X : index → M' → TangentBundle I' M'),
    ∃ (U : Set M'),
      x₀ ∈ U ∧
      ∀ i : index, ∀ y ∈ U,
        MDifferentiableWithinAt I' I'.tangent (X i) U y ∧
        (∀ e ∈ U, submodule_at e = Submodule.span 𝕜 (Set.range (fun i => (X i e).2)))

end EhresmannConnection

Does that look the right way to be going about things?

@Jens Lindekamp Did you make any progress with your approach?

[Michael Rothgang]

Patrick and I have defined local frames as part of our Levi-Civita work: can you reuse that instead?

[Michael Rothgang]

If you need, I could make a PR against current mathlib adding them.

[Michael Rothgang]

(I would make, and did, make a few design decisions differently. For example,

• my local frame is a collection of sections directly
• the second condition is its own predicate IsLocalFrameOn
• that condition is a structure with named fields

I can write more after making a PR.)

[Dominic Steinitz]

Michael Rothgang said:

Patrick and I have defined local frames as part of our Levi-Civita work: can you reuse that instead?

Almost certainly.

[Dominic Steinitz]

Michael Rothgang said:

If you need, I could make a PR against current mathlib adding them.

Yes please.

[Dominic Steinitz]

@Michael Rothgang what do you think about making this a stand alone PR and then I can add what it means to be an Ehresmann connection?

-- Copied from https://github.com/leanprover-community/mathlib4/pull/26221/files#diff-5299ff7f9b0ed6c90a7e2caecbbe13bbe74307087ae1455d82c9a93bec81b28d
noncomputable def verticalSubspaceGeneral (v : TotalSpace F V) :
    Submodule ℝ (TangentSpace (I.prod 𝓘(ℝ, F)) v) :=
  LinearMap.ker (mfderiv (I.prod 𝓘(ℝ, F)) I TotalSpace.proj v)

[Dominic Steinitz]

One thing that worried me about my definition is that it is finite dimensional. For my purposes, I don't care but other folk might.

[Dominic Steinitz]

Dominic Steinitz said:

One thing that worried me about my definition is that it is finite dimensional. For my purposes, I don't care but other folk might.

I mean for the local frame.

[Michael Rothgang]

Dominic Steinitz said:

Michael Rothgang said:

If you need, I could make a PR against current mathlib adding them.

Yes please.

Sure, here you go: #30083 is the PR. It makes use of the custom elaborators (as I'm not willing to un-use them, and it's a good testing group).

[Michael Rothgang]

My definition is not necessarily finite-dimensional, but some of its lemmas are. Help understanding to what extend this is essential is welcome.

[Michael Rothgang]

(The code is not maximally polished yet: some doc-strings are missing or outdated. I will polish that file once the differential geometry elaborators have been merged.)

[Michael Rothgang]

@Dominic Steinitz I'll let the PR speak for itself, for now. If you wonder about particular design questions, I can try to explain why we did things this way.

[Michael Rothgang]

Dominic Steinitz said:

Michael Rothgang what do you think about making this a stand alone PR and then I can add what it means to be an Ehresmann connection?

-- Copied from https://github.com/leanprover-community/mathlib4/pull/26221/files#diff-5299ff7f9b0ed6c90a7e2caecbbe13bbe74307087ae1455d82c9a93bec81b28d
noncomputable def verticalSubspaceGeneral (v : TotalSpace F V) :
    Submodule ℝ (TangentSpace (I.prod 𝓘(ℝ, F)) v) :=
  LinearMap.ker (mfderiv (I.prod 𝓘(ℝ, F)) I TotalSpace.proj v)

That definition is not sorry-free yet, right? IIUC, making it sorry free amounts to completing the proof that an affine connection induces an Ehresman connection. (Patrick and I want to do this, but we can't work on this full-time, sadly.)

[Michael Rothgang]

In general, I'm on the fence about PRs adding just a single definition without surrounding API: how do you know the definition is workable?

[Michael Rothgang]

(If you also intend to work on Ehresman connections, we should try to not duplicate work/if you're aiming for mathlib, let's discuss the proper way to do things first. And if you just want to do this for yourself, you could also copy-paste other code, right?)

[Dominic Steinitz]

There's a lot to chew over in what you have posted. Yes I want to define Ehresmann connections and express these as Lie-algebra valued 1-forms. And yes I would like it to form part of mathlib.

I've always thought of the picture as the other way up: an affine connection is derived from an Ehresmann connection and this explains the co-ordinate transformation behaviour of the Christoffel symbols (they are not tensors). I guess you could go the way round you suggest and maybe to show that an affine connection defines a connection on the frame bundle but I haven't thought this through.

The problem with what I want to do is that forms is that they do not yet exist in mathlib and the last commit I can find for the work on them is 3 months ago: https://github.com/urkud/DeRhamCohomology/commits/main/

So the short answer is yes I would like to discuss the proper way to do things (I still count myself as a noob).

So I suppose one way forward would be for me to show that an affine connection induces an Ehresmann connection using what you and Patrick have done. Alternatively I could try picking up the forms work. I am in your and Patrick's hands.

[Michael Rothgang]

Yury has been picking up the work on differential forms again (and been making PRs with material to mathlib). So I expect the project to move again (and am very happy about this).

[Dominic Steinitz]

I created a structure capturing what it means to be a principal fibre (fiber?) bundle: https://github.com/leanprover-community/mathlib4/pull/30121