Transition Maps on Smooth Manifold

Stream: new members

[Dominic Steinitz]

I started trying to prove that transition maps are smooth but they should be by definition so where would I find that?

example (m : ℕ) {M : Type*}
  [TopologicalSpace M]
  [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
  [SmoothManifoldWithCorners (𝓡 m) M]
  (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
  (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
  (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
  (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) :
    ContMDiffWithinAt (𝓡 m) (𝓡 m) ⊤ (φ_α.symm.trans φ_β).toFun (φ_α.toFun '' (φ_α.source ∩ φ_β.source))
    (φ_α x) := by
    have h1 : ContMDiffOn (𝓡 m) (𝓡 m) ⊤ φ_α φ_α.source := contMDiffOn_of_mem_maximalAtlas hΦ_Α
    sorry

[Michael Rothgang]

Indeed, in a smooth manifold, all transition maps are smooth by definition - so mathematically, you have nothing to prove. In Lean, this is formalised through a docs#contDiffGroupoid: a smooth manifold has an atlas whose transition maps from a contDiffGroupoid (meaning that they are C^n on their domain of definition).

[Michael Rothgang]

By the way, a short heads-up: the file SmoothManifoldsWithCorners.lean is being refactored now. If you're working on the latest mathlib version, you'll need to update your code when that lands (which should be within a week).

[Michael Rothgang]

A maximal atlas is defined in docs#StructureGroupoid.maximalAtlas

[Sébastien Gouëzel]

import Mathlib

open scoped Manifold
open SmoothManifoldWithCorners

example (m : ℕ) {M : Type*}
    [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
    [SmoothManifoldWithCorners (𝓡 m) M]
    (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
    (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
    (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
    (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
    (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) :
    ContMDiffAt (𝓡 m) (𝓡 m) ⊤ (φ_α.symm.trans φ_β) (φ_α x) := by
  simp only [PartialHomeomorph.coe_trans]
  apply ContMDiffAt.comp (I' := 𝓡 m)
  · apply contMDiffAt_of_mem_maximalAtlas hΦ_Β
    simpa [hx.1] using hx.2
  · apply contMDiffAt_symm_of_mem_maximalAtlas hΦ_Α
    exact PartialHomeomorph.map_source φ_α hx.1

[Michael Rothgang]

StructureGroupoid is an abstraction describing the requirement on the maximal atlas. For merely topological manifolds, continuousGroupoid captures this. For C^n manifolds, docs#contDiffGroupoid describes this fact. For analytic manifolds, there's docs#analyticGroupoid. One could also imagine e.g. PLGroupoid for PL manifolds (which are not in mathlib so far).

[Michael Rothgang]

So, hopefully between this explanation of mathlib's design and the worked example, you have an answer to your question now :-)

[Dominic Steinitz]

That's great - thanks very much both. I assumed that the chart maps were members of the groupoid. What was not clear to me was how one knew that such a member was $C^n$. Given the code sample does not explicitly reference groupoids, I am guessing that e.g. contMDiffAt_of_mem_maximalAtlas uses them under the covers (I will go look shortly).

Of course this is still a derivation rather than a definition but there are many ways to define manifolds.

For my own edification, I re-wrote the proof

import Mathlib

open scoped Manifold
open SmoothManifoldWithCorners

example (m : ℕ) {M : Type*}
    [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin m)) M]
    [SmoothManifoldWithCorners (𝓡 m) M]
    (φ_α : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
    (hΦ_Α : φ_α ∈ maximalAtlas (𝓡 m) M)
    (φ_β : PartialHomeomorph M (EuclideanSpace ℝ (Fin m)))
    (hΦ_Β : φ_β ∈ maximalAtlas (𝓡 m) M)
    (x : M) (hx : x ∈  φ_α.source ∩ φ_β.source) :
    ContMDiffAt (𝓡 m) (𝓡 m) ⊤ (φ_α.symm.trans φ_β) (φ_α x) := by
  have h1 : (φ_α.symm.trans φ_β) = φ_β ∘ φ_α.symm :=
   PartialHomeomorph.coe_trans φ_α.symm φ_β
  have h2 : ContMDiffAt (𝓡 m) (𝓡 m) ⊤ φ_β x :=
   contMDiffAt_of_mem_maximalAtlas hΦ_Β hx.2
  have h3 : ContMDiffAt (𝓡 m) (𝓡 m) ⊤ φ_α.symm (φ_α x) :=
   contMDiffAt_symm_of_mem_maximalAtlas hΦ_Α (PartialHomeomorph.map_source φ_α hx.1)
  have h4 : φ_α.symm (φ_α x) = x := PartialHomeomorph.left_inv φ_α hx.1
  have h5 : ContMDiffAt (𝓡 m) (𝓡 m) ⊤ φ_β (φ_α.symm (φ_α x)) := by
    rw [h4]
    exact h2
  have h7 : ContMDiffAt (𝓡 m) (𝓡 m) ⊤ (φ_β ∘ φ_α.symm) (φ_α x) :=
   ContMDiffAt.comp (I' := 𝓡 m) (φ_α x) h5 h3
  have h8 : ContMDiffAt (𝓡 m) (𝓡 m) ⊤ (φ_α.symm.trans φ_β) (φ_α x) := by
    rw [h1]
    exact h7
  exact h8

[Dominic Steinitz]

One further thought: shouldn't this or something similar be a theorem in mathlib?

[Sébastien Gouëzel]

We have in mathlib the facts that members of the maximal atlas are smooth, and that composition of smooth maps is smooth. I don't think more is needed: the composition of two elements of the maximal atlas has nothing special in this respect (and the fact that it hasn't been needed until now is an indication that this lemma wouldn't bring much). On the other hand, if you have examples of theorems you are proving where this fact is used several times, then maybe we should reconsider indeed!