coordchange as function of base is smooth

Stream: maths

[Sam Lindauer]

Hey there, in the project I am working on, I need to prove that the unitsection in the tangentbundle of the circle is smooth. I have defined the unitsection as follows:

import Mathlib

open scoped Manifold

notation "ℝ¹" => EuclideanSpace ℝ (Fin 1)
notation "𝕊¹" => Metric.sphere (0 : EuclideanSpace ℝ (Fin 2)) 1

/- The unit section of the tangent bundle of the circle -/
def unitSection : 𝕊¹ → TangentBundle (𝓡 1) (𝕊¹) := (⟨·, fun _ ↦ 1⟩)

In the intuitive sense, this 'is' the product of the identity function and the constant function, which is clearly smooth. I have been able to reduce the proof to a statement on the smoothness of coordchanges between the tangent spaces, but I am not sure how to prove this...

/- Smooth coordchange function -/
lemma coordchange_smooth (x : 𝕊¹) :
  SmoothAt 𝓘(ℝ, ℝ¹) 𝓘(ℝ, ℝ¹ →L[ℝ] ℝ¹)
    (fun (s : 𝕊¹) ↦
      (tangentBundleCore (𝓡 1) (𝕊¹)).coordChange
        ((tangentBundleCore (𝓡 1) (𝕊¹)).indexAt s)
        ((tangentBundleCore (𝓡 1) (𝕊¹)).indexAt x) s)
    x := by
      sorry

All help is much appreciated!
Sam

PS. For insight in how I have deduced the proof to this statement, the reduction is below.

/- unitSection is Smooth section -/
lemma smooth_unit : Smooth (𝓡 1) ((𝓡 1).prod (𝓡 1)) unitSection := by
  -- Take arbitrary point `x` and trivialization at `x`
  intro x
  let e' := (trivializationAt (ℝ¹) (TangentSpace (𝓡 1)) x)
  -- Show `unitSection x` is in the source of the trivialization
  have h1 : unitSection x ∈ e'.source := by
    refine (Trivialization.mem_source (trivializationAt (ℝ¹) (TangentSpace (𝓡 1)) x)).mpr ?_
    exact FiberBundle.mem_baseSet_trivializationAt' (unitSection x).proj
  haveI : MemTrivializationAtlas e' := by
    exact instMemTrivializationAtlasTrivializationAt x
  -- join of two smooth maps `id` and `const`
  have h : SmoothAt (𝓡 1) (𝓡 1) (fun s ↦ (e' (unitSection s)).1) x ∧
    SmoothAt (𝓡 1) (𝓡 1) ((fun s ↦ (e' (unitSection s)).2)) x := by
      constructor
      · -- `id` is smooth
        exact smooth_id x
      · refine ContMDiffAt.clm_apply ?right.hg ?right.hf
        · -- `coordchange function` is smooth
          apply coordchange_smooth
        · -- `const` is smooth
          exact smoothAt_const
  -- Finish proof using `h1` and `h`
  refine (Trivialization.smoothAt_iff (𝓡 1) h1).mpr ?_
  constructor
  · exact h.left
  · exact h.right

[Patrick Massot]

@Floris van Doorn is our expert in manifold smoothness proofs.

[Floris van Doorn]

For proving that something is smooth into the total space, I recommend using docs#Trivialization.contMDiffAt_iff. The fact that the coordinate change of the tangent bundle is smooth is stated in docs#TangentBundle.smoothVectorBundle. Probably those coordinate changes are not exactly the same, but they should be the same within charts.
Hope this helps.

[Sam Lindauer]

Thanks for the replies! Will be working on it today.

[Sam Lindauer]

@Floris van Doorn I am still having some trouble with finishing this proof. I have used docs#Trivialization.contMDiffAt_iff and can't quite get the two coordinate transformations, the one above and the one received from docs#TangentBundle.smoothVectorBundle, to line up. This is the coordtransformation we get from docs#TangentBundle.smoothVectorBundle:

class SmoothVectorBundle : Prop where
  protected smoothOn_coordChangeL :
    ∀ (e e' : Trivialization F (π F E)) [MemTrivializationAtlas e] [MemTrivializationAtlas e'],
      SmoothOn IB 𝓘(𝕜, F →L[𝕜] F) (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F))
        (e.baseSet ∩ e'.baseSet)

which needs me to give two fixed trivializations. Now, the problem I am having is that the coordchange function that I need to prove has one of the charts as a variable in the function itself, see the variable s in the function coordchange_smooth above. My plan was to essentially shrink down the neighbourhood around x enough (say the baseSet of x using for example docs#ContMDiffAt.congr_of_eventuallyEq) and say that any chosen ((tangentBundleCore (𝓡 1) (𝕊¹)).indexAt s) within this neighbourhood is the same as ((tangentBundleCore (𝓡 1) (𝕊¹)).indexAt x), but I don't know how to make the claim that these charts are the same in such a neighbourhood....