The derivative of a chart on a smooth manifold is smooth

Stream: Is there code for X?

[Dominic Steinitz]

import Mathlib

open ContDiff Manifold

variable
  {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB]
  {HB : Type*} [TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞}
  {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]

example (i : B) :
  ContMDiffOn (M' := EB →L[ℝ] EB) IB 𝓘(ℝ, EB →L[ℝ] EB) ⊤
    (fun p => mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p)
    (extChartAt IB i).source := sorry

[Michael Rothgang]

You'll want a new lemma ContMDiffOn.mfderiv (saying "if f is C^{n+1}, then mfderiv f is C^n") and then use docs#contMDiffOn_extChartAt (and docs#contMDiffOn_extChartAt_symm). The former would be a nice PR to mathlib; feel free to ping me for review.

[Michael Rothgang]

We have docs#ContDiffOn.fderiv_of_isOpen, for example --- so that's hopefully just a consequence of the fderiv lemma.

[Michael Rothgang]

Actually, I might have proven this with Patrick already. Let me take a look...

[Sébastien Gouëzel]

What would it mean to say that mfderiv is smooth? You would need to put some coordinates there, otherwise it doesn't really make sense if I understand correctly what you wrote. We have docs#ContMDiffAt.mfderiv for a correct version.

[Dominic Steinitz]

Sébastien Gouëzel said:

What would it mean to say that mfderiv is smooth? You would need to put some coordinates there, otherwise it doesn't really make sense if I understand correctly what you wrote. We have docs#ContMDiffAt.mfderiv for a correct version.

Maybe I put my question clumsily. I didn't think I was saying that mfderiv is smooth but

if $f : M \longrightarrow N$ is $C^{n+1}$, then $p \mapsto mfderiv f p : M \longrightarrow T_p M \longrightarrow T_{f(p)} ​N$  is $C^n$ in $p$.

I think @Michael Rothgang is suggesting I write this as ContMDiffOn.mfderiv

EDIT: And $f$ in my question is a chart map.

[Sébastien Gouëzel]

I still think that what you wrote is not really well defined, because you are not considering a map from a manifold to another manifold. Your map starts from M, which is a manifold, fine, but what space does it go into?
Maybe you're looking for docs#ContMDiffOn.contMDiffOn_tangentMapWithin?

[Dominic Steinitz]

Ah in my head the space it goes into is $\R^n$ (it's a chart map) but maybe that is too limiting. Anyway I should be explicit. I hope I have understood correctly.

[Sébastien Gouëzel]

You are looking at the map sending p : M to (a linear map from T_p M to $\R^n$). On the right, we have something which is not a manifold -- it's not even really a target space as it depends on the initial point p.

[Dominic Steinitz]

I have done what I wanted via coordinates (or rather nearly done it as I have 2 sorry). I will have no time to work on this further until the new year but I would be interested in any feedback. BTW I seem to have invented the cotangent bundle on my journey :monocle:

import Mathlib
open Bundle Manifold ContDiff

noncomputable section

variable {EB : Type*} [NormedAddCommGroup EB] [InnerProductSpace ℝ EB] [FiniteDimensional ℝ EB]
variable {HB : Type*} [TopologicalSpace HB]
variable {B : Type*} [TopologicalSpace B] [ChartedSpace HB B]
variable (IB : ModelWithCorners ℝ EB HB)
variable {n : WithTop ℕ∞}
variable [IsManifold IB ⊤ B]
variable [SigmaCompactSpace B] [T2Space B]

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
variable {E : B → Type*} [TopologicalSpace (TotalSpace F E)]
variable [∀ x, TopologicalSpace (E x)] [∀ x, AddCommGroup (E x)] [∀ x, Module ℝ (E x)]
variable [FiberBundle F E] [VectorBundle ℝ F E]
variable [ContMDiffVectorBundle ⊤ F E IB]

noncomputable instance : TopologicalSpace (TotalSpace EB (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _)) :=
  inferInstanceAs (TopologicalSpace (TangentBundle IB B))

noncomputable instance (p : B) : NormedAddCommGroup (TangentSpace IB p) := by
  change NormedAddCommGroup EB
  infer_instance

noncomputable instance (p : B) : NormedSpace ℝ (TangentSpace IB p) := by
  change NormedSpace ℝ EB
  infer_instance

noncomputable instance (p : B) : InnerProductSpace ℝ (TangentSpace IB p) := by
  change InnerProductSpace ℝ EB
  infer_instance

section CotangentBundle

variable (E) in
/-- This is the bundle `Hom_ℝ(E, T)`, where `T` is the rank one trivial bundle over `B`. -/
private def V : (b : B) → Type _ := (fun b ↦ E b →L[ℝ] Trivial B ℝ b)

noncomputable instance : (x : B) → TopologicalSpace (V E x) := by
  unfold V
  infer_instance

noncomputable instance : (x : B) → AddCommGroup (V E x) := by
  unfold V
  infer_instance

noncomputable instance (x : B) : Module ℝ (V E x) := by
  unfold V
  infer_instance

noncomputable instance : TopologicalSpace (TotalSpace (F →L[ℝ] ℝ) (V E)) := by
  unfold V
  infer_instance

noncomputable instance : FiberBundle (F →L[ℝ] ℝ) (V E) := by
  unfold V
  infer_instance

noncomputable instance : VectorBundle ℝ (F →L[ℝ] ℝ) (V E) := by
  unfold V
  infer_instance

noncomputable instance :
VectorBundle ℝ (EB →L[ℝ] ℝ) (V (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _)) := by
  unfold V
  infer_instance

noncomputable instance : ContMDiffVectorBundle n (F →L[ℝ] ℝ) (V E) IB := by
  unfold V
  infer_instance

noncomputable instance (x : B) : NormedAddCommGroup
 (V (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) x) := by
  unfold V
  change NormedAddCommGroup (TangentSpace IB x →L[ℝ] ℝ)
  infer_instance

noncomputable instance (x : B) : NormedSpace ℝ (V (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) x) := by
  unfold V
  change NormedSpace ℝ (TangentSpace IB x →L[ℝ] ℝ)
  infer_instance

noncomputable instance : ContMDiffVectorBundle ∞ (EB →L[ℝ] ℝ)
 (V (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _)) IB := by
  unfold V
  infer_instance

end CotangentBundle

noncomputable
def simple_section (e₀ : EB) (i : B) (x : B) : TangentSpace IB x →L[ℝ] ℝ :=
  let φ := extChartAt IB i
  let dφ := mfderiv IB 𝓘(ℝ, EB) φ x
  (innerSL ℝ e₀).comp dφ

theorem simple_section_in_trivialization (e₀ : EB) (i p : B) (hp : p ∈ (extChartAt IB i).source) :
  let e := trivializationAt (EB →L[ℝ] ℝ) (fun b => TangentSpace IB b →L[ℝ] ℝ) i
  (e ⟨p, simple_section IB e₀ i p⟩).2 = innerSL ℝ e₀ := by

  unfold simple_section

  let e_tangent := trivializationAt EB (TangentSpace IB) i
  have : trivializationAt (EB →L[ℝ] ℝ) (fun b => TangentSpace IB b →L[ℝ] ℝ) i =
         Trivialization.continuousLinearMap (RingHom.id ℝ) e_tangent
         (trivializationAt ℝ (fun _ : B => ℝ) i) := rfl
  rw [this]

  change
    (Trivialization.continuousLinearMap (RingHom.id ℝ) e_tangent
    (trivializationAt ℝ (fun _ : B => ℝ) i)
    ⟨p, ((innerSL ℝ e₀).comp (mfderiv IB 𝓘(ℝ, EB) (extChartAt IB i) p))⟩).2 = innerSL ℝ e₀

  rw [Trivialization.continuousLinearMap_apply]
  simp
  have e_tangent_symmL_eq : e_tangent.symmL ℝ p =
    (tangentBundleCore IB B).coordChange (achart HB i) (achart HB p) p := by
    have hp : p ∈ (chartAt HB i).source := Set.mem_of_mem_inter_left hp
    exact TangentBundle.symmL_trivializationAt_eq_core hp
  rw [e_tangent_symmL_eq, tangentBundleCore_coordChange_achart]

  simp
  rw [ContinuousLinearMap.comp_assoc]

  -- I hope this is obvious and straightforward
  have key : (mfderiv IB 𝓘(ℝ, EB) (↑IB ∘ ↑(chartAt HB i)) p).comp
    (fderivWithin ℝ ((↑IB ∘ ↑(chartAt HB p)) ∘ ↑(chartAt HB i).symm ∘ ↑IB.symm)
      (Set.range ↑IB) (IB ((chartAt HB i) p))) =
    ContinuousLinearMap.id ℝ EB := by
    sorry

  rw [key]
  rw [ContinuousLinearMap.comp_id]

theorem simple_section_smooth (e₀ : EB) (i : B) :
  ContMDiffOn IB (IB.prod 𝓘(ℝ, EB →L[ℝ] ℝ)) ω
    (fun p => TotalSpace.mk' (EB →L[ℝ] ℝ) p (simple_section IB e₀ i p))
    (extChartAt IB i).source := by
  intro p hp
  let e := trivializationAt (EB →L[ℝ] ℝ) (fun b ↦ TangentSpace IB b →L[ℝ] ℝ) i

  letI : ChartedSpace (EB →L[ℝ] ℝ) (TangentSpace IB p →L[ℝ] ℝ) := by
    change ChartedSpace (EB →L[ℝ] ℝ) (EB →L[ℝ] ℝ)
    infer_instance

  have h2 :  TotalSpace.mk' (EB →L[ℝ] ℝ) p (simple_section IB e₀ i p) ∈ e.source := by
    rw [e.mem_source]
    simp
    exact sorry

  have h_iff :=
  Trivialization.contMDiffWithinAt_iff
    (n := ω)
    (e := e)
    (x₀ := p)
    (f := (fun p => TotalSpace.mk' (EB →L[ℝ] ℝ) p (simple_section IB e₀ i p)))
    (s := (extChartAt IB i).source)
    (IB := IB)
    (IM := IB)
    (M := B)
    (F := EB →L[ℝ] ℝ)
    (E := fun b => TangentSpace IB b →L[ℝ] ℝ)
    h2

  rw [h_iff]
  constructor
  · simp
    have : ContMDiffWithinAt IB IB ω (fun x ↦ x) (chartAt HB i).source p := contMDiffWithinAt_id
    exact this
  · have h_const : ∀ x ∈ (extChartAt IB i).source,
      (e ⟨x, simple_section IB e₀ i x⟩).2 = innerSL ℝ e₀ :=
      fun x hx => simple_section_in_trivialization IB e₀ i x hx

    apply ContMDiffWithinAt.congr contMDiffWithinAt_const
    · intro x hx
      change (e ⟨x, simple_section IB e₀ i x⟩).2 = innerSL ℝ e₀
      exact h_const x hx
    · exact h_const p hp

[Dominic Steinitz]

I don't know why the playground is kicking off about

#synth TopologicalSpace (TotalSpace (EB →L[ℝ] ℝ)
  fun b => (@TangentSpace ℝ _ _ _ _ _ _ IB B _ _) b →L[ℝ] ℝ)

That is fine on my computer.

[Dominic Steinitz]

Huh - Zulip has capitalised "i" to "I" causing mayhem - I am trying to fix.

[Dominic Steinitz]

I get no errors in playground now :relieved:

[Dominic Steinitz]

Does this sound reasonable?

We have

theorem TangentBundle.trivializationAt_baseSet (x : M) : (trivializationAt E (TangentSpace I) x).baseSet = (chartAt H x).source := rfl

so if we can proved the baseSet for the tangent trivialisations are the same as the baseSet for the cotangent trivialisations then we are home and dry. And they should be because the cotangent bundle is derived from the tangent bundle.

[Dominic Steinitz]

This solved the sorry

  have h_base' : (trivializationAt (EB →L[ℝ] ℝ) (fun b ↦ TangentSpace IB b →L[ℝ] ℝ) i).baseSet =
                 (chartAt HB i).source := by
     dsimp [trivializationAt]
     exact Set.inter_univ (chartAt HB i).source

  have h2 :  TotalSpace.mk' (EB →L[ℝ] ℝ) p (simple_section IB e₀ i p) ∈ e.source := by
    rw [e.mem_source]
    simp
    have : p ∈ (extChartAt IB i).source := hp
    rw [extChartAt_source] at this
    have : p ∈ (trivializationAt (EB →L[ℝ] ℝ) (fun b ↦ TangentSpace IB b →L[ℝ] ℝ) i).baseSet := by
      rw [<-h_base'] at this
      exact this
    exact this

[Dominic Steinitz]

This looks very fishy to me

  -- I hope this is obvious and straightforward
  have key : (mfderiv IB 𝓘(ℝ, EB) (↑IB ∘ ↑(chartAt HB i)) p).comp
    (fderivWithin ℝ ((↑IB ∘ ↑(chartAt HB p)) ∘ ↑(chartAt HB i).symm ∘ ↑IB.symm)
      (Set.range ↑IB) (IB ((chartAt HB i) p))) =
    ContinuousLinearMap.id ℝ EB := by
    sorry

but I will repair the actual lemma about trivialisation of the section being the definition in the chart.