5.7. Surface.ULiftManifold🔗

Jacobians.Surface.ULiftManifold — source

trans_relabel

The transition map between two relabelled charts equals the transition map of M between the underlying charts: the ULift relabel and its inverse cancel. This is the key step that lands the transition maps of ULift M in contDiffGroupoid.

theorem trans_relabel (c c' : OpenPartialHomeomorph M E) :
    (Homeomorph.ulift.transOpenPartialHomeomorph c).symm ≫ₕ
        (Homeomorph.ulift.transOpenPartialHomeomorph c')
      = c.symm ≫ₕ c'

chart

The chart of ULift M at z: relabel M's chart through ULift M ≃ₜ M. As a function it is (chartAt E z.down) ∘ ULift.down.

noncomputable def chart [ChartedSpace E M] (z : ULift.{u} M) :
    OpenPartialHomeomorph (ULift.{u} M) E

instChartedSpace

ULift M is a charted space over E, with charts the relabelled charts of M.

noncomputable instance instChartedSpace [ChartedSpace E M] : ChartedSpace E (ULift.{u} M) where

chartAt_eq

theorem chartAt_eq [ChartedSpace E M] (z : ULift.{u} M) :
    (chartAt E z : OpenPartialHomeomorph (ULift.{u} M) E) = chart z

chart_apply

theorem chart_apply [ChartedSpace E M] (z w : ULift.{u} M) :
    chart (E := E) z w = chartAt E z.down w.down

chart_source

theorem chart_source [ChartedSpace E M] (z : ULift.{u} M) :
    (chart (E := E) z).source = ULift.down ⁻¹' (chartAt E z.down).source

instIsManifold

ULift M is a C^ω manifold modelled on E: its transition maps are those of M, hence lie in contDiffGroupoid ω 𝓘(ℂ, E).

instance instIsManifold [ChartedSpace E M] [NormedSpace ℂ E] [IsManifold 𝓘(ℂ, E) ω M] :
    IsManifold 𝓘(ℂ, E) ω (ULift.{u} M)

contMDiff_uliftDown

ULift.down : ULift M → M is C^ω.

Near x, on the chart source, it factors as (M-chart at x.down).symm ∘ (ULift-chart at x), both of which are C^ω: the relabelled charts make down the identity in coordinates.

theorem contMDiff_uliftDown [ChartedSpace E M] [NormedSpace ℂ E] [IsManifold 𝓘(ℂ, E) ω M] :
    ContMDiff 𝓘(ℂ, E) 𝓘(ℂ, E) ω (ULift.down : ULift.{u} M → M)

contMDiff_uliftUp

ULift.up : M → ULift M is C^ω.

Near m, on the chart source, it factors as (ULift-chart at up m).symm ∘ (M-chart at m).

theorem contMDiff_uliftUp [ChartedSpace E M] [NormedSpace ℂ E] [IsManifold 𝓘(ℂ, E) ω M] :
    ContMDiff 𝓘(ℂ, E) 𝓘(ℂ, E) ω (ULift.up : M → ULift.{u} M)

instLieAddGroup

If M is an additive Lie group, so is ULift M: addition and negation are conjugates, via ULift.up/ULift.down, of the smooth operations on M, hence smooth.

ULift M already carries AddCommGroup and IsTopologicalAddGroup instances from Mathlib.

instance instLieAddGroup [ChartedSpace E M] [NormedSpace ℂ E] [AddCommGroup M]
    [LieAddGroup 𝓘(ℂ, E) ω M] : LieAddGroup 𝓘(ℂ, E) ω (ULift.{u} M) where