6.11. MappingDegree.ChartPullbackDataConstruction🔗

Jacobians.MappingDegree.ChartPullbackDataConstruction — source

chartPullbackData_of_contMDiff

Constructor: ChartPullbackData from ContMDiffAt … ω.

Given f : X → Y between ChartedSpace ℂ manifolds, with ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω f x and the local non-degeneracy hypothesis that the chart pullback of f is not eventually equal to its value at (chartAt ℂ x) x, we build a ChartPullbackData f x (f x) witness.

noncomputable def chartPullbackData_of_contMDiff
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y} {x : X}
    (hf : ContMDiffAt 𝓘(ℂ) 𝓘(ℂ) ω f x)
    (hne : ¬ ∀ᶠ z in 𝓝 ((chartAt ℂ x) x),
        ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm) z
          = (chartAt ℂ (f x)) (f x)) :
    ChartPullbackData f x (f x)

chartPullbackData_of_contMDiff_global

Globalised constructor. From global ContMDiff … ω f and a chart-pullback non-degeneracy hypothesis at every fibre point of y₀, build a ChartPullbackData witness at every fibre point.

noncomputable def chartPullbackData_of_contMDiff_global
    {X : Type u} [TopologicalSpace X] [ChartedSpace ℂ X]
    {Y : Type v} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {f : X → Y} (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    {y₀ : Y}
    (hne : ∀ x : X, f x = y₀ →
      ¬ ∀ᶠ z in 𝓝 ((chartAt ℂ x) x),
          ((chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm) z
            = (chartAt ℂ (f x)) (f x)) :
    ∀ x ∈ f ⁻¹' {y₀}, ChartPullbackData f x y₀