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.