The differential of transition maps

Stream: new members

[Dominic Steinitz]

I am trying to prove that the differential of transition maps is a non-singular linear map. So here is what I hope is a MWE (except it doesn't work). In the example, I can get a map from the target of a chart back to itself via the manifold but I don't seem to be able to differentiate it.

import Mathlib

open SmoothManifoldWithCorners
open IsManifold
open scoped Manifold
open TopologicalSpace

variable
{n : ℕ}
{a : (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))}
{h : a.1 ∈ (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))}
{x : (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)}

example : true := by
  let s := { carrier := a.1.source, is_open' := a.1.open_source : Opens (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)}
  let t := { carrier := a.1.target, is_open' := a.1.open_target : Opens (EuclideanSpace ℝ (Fin n))}
  let (j1h : Structomorph ((contDiffGroupoid ⊤) (𝓡 n)) s t) := PartialHomeomorph.toStructomorph h
  let baz := j1h.symm.trans j1h
  let foo := (baz.toFun : a.1.target -> a.1.target)
  let (ptl : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) := fderiv ℝ /- I can't put foo here -/ sorry (a.1 x)
  let B := Pi.basisFun ℝ (Fin n)
  let tm := LinearMap.toMatrix B B ptl.toLinearMap
  have h1 : Matrix.det tm ≠ 0 := sorry
  trivial /- exact h1 -/

[Vlad Tsyrklevich]

I have no idea the underlying mathematics you are working with, but adding foo where indicated fails because foo is not a map EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n) but rather ↥t → ↥t where hovering over ↥t gives that it's a Subtype, specifically @Subtype (EuclideanSpace ℝ (Fin n)) fun x => x ∈ t, so foo is defined over $\R^n \cap t$ instead of all of R^n. Not being familiar with the underlying math/APIs, it's not clear to me if R^n=t so this just requires a little massaging to make Lean realize the types are equivalent or if there is something else going on.

[Michael Rothgang]

Can you make an actual MWE - in the sense of showing the statement you want to prove? I only have a vague idea about that...

[Michael Rothgang]

However, a general comment: the differential geometry library uses the "junk value pattern" a lot. A manifold chart only maps an open subset of the manifold to an open subset of (say, for simplification) Euclidean space.
You could model this as a map between subtypes of the manifold/Euclidean space - but this would make working with them painful: for instance, you'd have to constantly prove that your terms lie in this subtype, and compatibility of transition maps were a statement about differentiability of maps between subtypes.
Instead, mathlib defines charts as PartialHomeomorphs: they are defined on the whole manifold and map into the whole normed space, but they value is only meaningful on open sets of the domain (and codomain). Outside of them, they take a "junk value". These open subsets are the source and target of the chart; compatibility speaks about the transition maps being differentiable on the source.

This is still a bit cumbersome to work with, but much nicer than dealing with subtypes.

[Michael Rothgang]

For vector bundles, the design is similar: trivialisations extend PartialHomeomorph --- are defined globally, but only make sense between their source and target (which have a particular shape, related to their baseSet).

Hence, my strong suggestion is to revise your design, and consider maps defined on the whole space.

[Michael Rothgang]

One last comment: I'm slightly confused how you get into the MWE above. "Transition maps are smooth" is implied by the construction of a smooth manifold structure; mathlib already has the sphere being a smooth manifold.

Or is this just an illustrative example, and you need to prove smoothness of a new manifold you constructed?

[Dominic Steinitz]

I am constructing the frame bundle as a fibre bundle and and the coordinate transforms are linear maps within the fibres so I need to construct the linear map from the transition map. I am busy at the moment but can give a more detailed explanation tomorrow.

[Dominic Steinitz]

I'll answer your points one by one but first I wanted to give the big picture.

I want to construct the frame bundle. The fibres are elements of GL(n). The question is then what are the co-ordinate change maps. For any change of basis we have the Jacobian. So we can transform an element of GL(n) by composing it with the Jacobian. This should satisfy all the requirements to be a FiberBundleCore.

Here's where I got to.

import Mathlib

open SmoothManifoldWithCorners
open IsManifold
open scoped Manifold
open TopologicalSpace

noncomputable
def GLBundle {n : ℕ} : FiberBundleCore
  (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))
  (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)
  (GL (Fin n) ℝ)
  where

  baseSet i := i.1.source
  isOpen_baseSet i := i.1.open_source
  indexAt := achart (EuclideanSpace ℝ (Fin n))
  mem_baseSet_at := mem_chart_source (EuclideanSpace ℝ (Fin n))

  coordChange i j x v := by
    have h1 : i.1 ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1) := i.2
    have h2 : j.1 ∈ atlas (EuclideanSpace ℝ (Fin n)) ↑(Metric.sphere 0 1) := j.2
    have h3 : (i.1).symm ≫ₕ j.1 ∈ ((contDiffGroupoid ⊤) (𝓡 n)) := HasGroupoid.compatible h1 h2

    -- I think the above h3 should be enough to determine that the differential of
    -- `(i.1).symm ≫ₕ j.1` is a non-degenerate linear map (at a point) but I don't
    -- know how get hold of this fact.

    -- Let's try a different way:

    let d := (fderiv ℝ (j.1 ∘ (i.1).symm) (i.1 x)).toLinearMap
    let B := Pi.basisFun ℝ (Fin n)
    let m := LinearMap.toMatrix B B d
    let (p : Matrix (Fin n) (Fin n) ℝ) := m * v
    -- But we can't return `p` - we need to convert to an element of GL(n) and that requires
    -- knowing that it has non-zero determinant.
    exact (sorry : GL (Fin n) ℝ)

  coordChange_self := sorry
  continuousOn_coordChange := sorry
  coordChange_comp := sorry

-- So how can we show that the differential of a chart map is a non-degenerate
-- linear map (at a point). Here's an attempt but I get stuck trying to show that
-- maps are `MDifferentiable`

variable
{n : ℕ}
{a : (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))}
{h : a.1 ∈ (atlas (EuclideanSpace ℝ (Fin n)) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1))}
{x : (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1)}

open PartialHomeomorph
open Set Filter Function
open PartialHomeomorph.MDifferentiable

example : LinearMap.ker (mfderiv (𝓡 n) (𝓡 n) ((a.1).symm ≫ₕ a.1) (a.1 x)) = ⊥ := by
  let I := (𝓡 n)
  let sI := range I
  let iext := a.1.extend I
  let jext := a.1.extend I
  let ji := jext ∘ iext.symm
  have hx : (a.1 x) ∈ ((a.1).symm ≫ₕ a.1).source := sorry
  have hz : PartialHomeomorph.MDifferentiable I I ((a.1).symm ≫ₕ a.1) := sorry
  have h0 : LinearMap.ker (mfderiv (𝓡 n) (𝓡 n) ((a.1).symm ≫ₕ a.1) (a.1 x)) = ⊥ :=
    ker_mfderiv_eq_bot hz hx
  exact h0

[Dominic Steinitz]

Michael Rothgang said:

However, a general comment: the differential geometry library uses the "junk value pattern" a lot. A manifold chart only maps an open subset of the manifold to an open subset of (say, for simplification) Euclidean space.
You could model this as a map between subtypes of the manifold/Euclidean space - but this would make working with them painful: for instance, you'd have to constantly prove that your terms lie in this subtype, and compatibility of transition maps were a statement about differentiability of maps between subtypes.
Instead, mathlib defines charts as PartialHomeomorphs: they are defined on the whole manifold and map into the whole normed space, but they value is only meaningful on open sets of the domain (and codomain). Outside of them, they take a "junk value". These open subsets are the source and target of the chart; compatibility speaks about the transition maps being differentiable on the source.

This is still a bit cumbersome to work with, but much nicer than dealing with subtypes.

I didn't mean to work with subtypes - Lean or Mathlib somehow led me to using them. I don't think I am using them now.

[Dominic Steinitz]

Michael Rothgang said:

One last comment: I'm slightly confused how you get into the MWE above. "Transition maps are smooth" is implied by the construction of a smooth manifold structure; mathlib already has the sphere being a smooth manifold.

Or is this just an illustrative example, and you need to prove smoothness of a new manifold you constructed?

I know that transition maps are smooth but they are also diffeomorphisms and thus their derivative should be a non-degenerate linear map (at a point) - the Jacobian $\frac{\partial y^b}{\partial x^a}\big|_p$ in co-ordinates. It is this linear map and a proof its non-degeneracy that I wish to get hold of.

[Michael Rothgang]

Dominic Steinitz said:

Michael Rothgang said:

One last comment: I'm slightly confused how you get into the MWE above. "Transition maps are smooth" is implied by the construction of a smooth manifold structure; mathlib already has the sphere being a smooth manifold.

Or is this just an illustrative example, and you need to prove smoothness of a new manifold you constructed?

I know that transition maps are smooth but they are also diffeomorphisms and thus their derivative should be a non-degenerate linear map (at a point) - the Jacobian $\frac{\partial y^b}{\partial x^a}\big|_p$ in co-ordinates. It is this linear map and a proof its non-degeneracy that I wish to get hold of.

I'll need to think more (and am going home now) - but one comment I can already make: this comment sounds like you want to prove "the differential of a diffeomorphism is a linear equivalence" - is that correct?

[Dominic Steinitz]

I'll need to think more (and am going home now) - but one comment I can already make: this comment sounds like you want to prove "the differential of a diffeomorphism is a linear equivalence" - is that correct?

Correct

Apologies for not giving enough detail. I am very new at this.

[Michael Rothgang]

No worries, I understand what you meant :-)

[Michael Rothgang]

I have a PR for that (#8738), which stalled about a year ago: it was stuck with a question "how can we make this argument work nicely, without assuming completeness". I've been meaning to get back to that PR, so this could be a nice occasion. (I don't mind help - but I'm not sure if that's an easy task.)

So: one sensible course of action is to sorry that statement and move to your other questions (and have your PR depend on 8738).

[Dominic Steinitz]

I am about to have to work on something else but two points:

1. I hope f ∈((contDiffGroupoid ⊤) (𝓡 n)) means that f is a diffeomorphism (but I don't know how to get that yet)
2. If I have a diffeo don't I just compose it with its inverse and differentiate and use the chain rule to get a linear map and its inverse?

[Michael Rothgang]

About 2. Yes, you do. But that's not how you'd want to prove it in mathlib - there, you'd realised that the same holds for a local diffeomorphism, so you prove "charts are local diffeos" and "local diffeos have invertible differential" (which is what my branch does). But then "charts are local diffeos" is more subtle than me-a-year-ago anticipated (having to do with completeness).
In short: for mathlib, you want the more elaborate proof. For your learning, using the chain rule is fine.

[Michael Rothgang]

About 1. first off: charts are not diffeomorphisms, as they are only nicely behaved on an open sets. This sounds pedantic (and it is), but Lean will complain if you overlook that detail...
"Every chart is a local diffeomorphism" is true (an inverse is given by .symm). This is not quite what your statement says, though.