6.44. MappingDegree.PathSubdivisionByBallCharts🔗

Jacobians.MappingDegree.PathSubdivisionByBallCharts — source

Path.exists_ball_chart_subdivision

Path subdivision by ball-targeted charts: any continuous path γ : Path p q in a charted space Y over ℂ admits a finite monotone partition t : ℕ → I with t 0 = 0, eventually t m = 1, together with, for each piece i, an OpenPartialHomeomorph Y ℂ whose target is an open ball in ℂ (with positive radius and a chosen centre) and whose source contains the image of γ on Icc (t i) (t (i+1)).

Strategy:

1. For each y : I, chart_restrict_to_ball (γ y) produces a ball-restricted chart φ y with γ y ∈ (φ y).source.

2. The family c y := γ ⁻¹' (φ y).source is an open cover of I (each is open as a preimage of an open set under a continuous map; y ∈ c y because γ y ∈ (φ y).source).

3. Apply exists_monotone_Icc_subset_open_cover_unitInterval to refine to a monotone partition with one Lebesgue index y i : I per piece.

4. Take the ball-restricted chart at γ (y i) for piece i.

theorem Path.exists_ball_chart_subdivision
    {Y : Type*} [TopologicalSpace Y] [ChartedSpace ℂ Y]
    {p q : Y} (γ : Path p q) :
    ∃ (t : ℕ → I) (φ : ℕ → OpenPartialHomeomorph Y ℂ)
      (r : ℕ → ℝ) (centers : ℕ → ℂ),
      t 0 = 0 ∧ Monotone t ∧ (∃ N, ∀ m ≥ N, t m = 1) ∧
      (∀ i, 0 < r i) ∧
      (∀ i, (φ i).target = Metric.ball (centers i) (r i)) ∧
      (∀ i, ∀ s ∈ Icc (t i) (t (i + 1)), γ s ∈ (φ i).source)