14.10. Cech.ChartDiskRefinement🔗

Jacobians.Cech.ChartDiskRefinement — source

exists_radius_disk_subset

For each x and open neighborhood V of x, there is a radius ρ > 0 whose *closed* coordinate ball lies in the chart target and whose coordinate disk lands inside V.

(extChartAt … x).symm is continuous at c := extChartAt … x x and sends c ↦ x ∈ V, so (extChartAt … x).symm ⁻¹' V is a neighborhood of c; intersecting with the (open) target and extracting a metric ball ball c ρ₁ gives the radius (halved for the closed-ball clause). Membership in V follows since (extChartAt … x).symm left-inverts extChartAt … x on the source.

theorem exists_radius_disk_subset {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] (x : X)
    (V : Set X) (hVopen : IsOpen V) (hxV : x ∈ V) :
    ∃ ρ > 0,
      Metric.closedBall (extChartAt 𝓘(ℝ, ℂ) x x) ρ ⊆ (extChartAt 𝓘(ℝ, ℂ) x).target ∧
      (extChartAt 𝓘(ℝ, ℂ) x) ⁻¹' Metric.ball (extChartAt 𝓘(ℝ, ℂ) x x) ρ
          ∩ (extChartAt 𝓘(ℝ, ℂ) x).source ⊆ V

exists_coverIdx

For each x, an index i of the cover with x ∈ 𝔘.U i (exists by 𝔘.covers).

theorem exists_coverIdx {X : Type*} [TopologicalSpace X] (𝔘 : FiniteCover X) (x : X) :
    ∃ i, x ∈ ((𝔘.U i : Opens X) : Set X)

coverIdx

The chosen cover index containing x.

noncomputable def coverIdx {X : Type*} [TopologicalSpace X] (𝔘 : FiniteCover X) (x : X) : 𝔘.ι

coverIdx_mem

theorem coverIdx_mem {X : Type*} [TopologicalSpace X] (𝔘 : FiniteCover X) (x : X) :
    x ∈ ((𝔘.U (coverIdx 𝔘 x) : Opens X) : Set X)

exists_refRadius

The shrinking-lemma data applied to V = 𝔘.U (coverIdx x).

theorem exists_refRadius {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) :
    ∃ ρ > 0,
      Metric.closedBall (extChartAt 𝓘(ℝ, ℂ) x x) ρ ⊆ (extChartAt 𝓘(ℝ, ℂ) x).target ∧
      (extChartAt 𝓘(ℝ, ℂ) x) ⁻¹' Metric.ball (extChartAt 𝓘(ℝ, ℂ) x x) ρ
          ∩ (extChartAt 𝓘(ℝ, ℂ) x).source ⊆ ((𝔘.U (coverIdx 𝔘 x) : Opens X) : Set X)

refRadius

The chosen disk radius around x.

noncomputable def refRadius {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) : ℝ

refRadius_pos

theorem refRadius_pos {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) : 0 < refRadius 𝔘 x

closedBall_refRadius_subset_target

theorem closedBall_refRadius_subset_target {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) :
    Metric.closedBall (extChartAt 𝓘(ℝ, ℂ) x x) (refRadius 𝔘 x) ⊆ (extChartAt 𝓘(ℝ, ℂ) x).target

refDiskNbhd

The chart-disk neighborhood of x whose chart-preimage ball sits inside 𝔘.U (coverIdx x). Written with the chart-preimage first to match the ChartDiskCover.isDisk field directly.

def refDiskNbhd {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) : Set X

refDiskNbhd_subset_cover

theorem refDiskNbhd_subset_cover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) :
    refDiskNbhd 𝔘 x ⊆ ((𝔘.U (coverIdx 𝔘 x) : Opens X) : Set X)

refDiskNbhd_isOpen

theorem refDiskNbhd_isOpen {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) : IsOpen (refDiskNbhd 𝔘 x)

mem_refDiskNbhd

theorem mem_refDiskNbhd {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    (𝔘 : FiniteCover X) (x : X) : x ∈ refDiskNbhd 𝔘 x

exists_finite_refDiskNbhd_cover

theorem exists_finite_refDiskNbhd_cover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X]
    [CompactSpace X]
    (𝔘 : FiniteCover X) :
    ∃ s : Finset X, (⋃ x ∈ s, refDiskNbhd 𝔘 x) = Set.univ

centers

The finite set of centres of the refining chart-disk cover.

noncomputable def centers {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X]
    (𝔘 : FiniteCover X) : Finset X

centers_cover

theorem centers_cover {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X]
    (𝔘 : FiniteCover X) :
    (⋃ x ∈ centers 𝔘, refDiskNbhd 𝔘 x) = Set.univ

center

The centre of X indexed by Fin (centers.card).

noncomputable def center {X : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [CompactSpace X]
    (𝔘 : FiniteCover X) (i : Fin (centers 𝔘).card) : X

cover

The refining chart-disk cover of X whose every set sits inside some 𝔘.U.

noncomputable def cover {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (𝔘 : FiniteCover X) : ChartDiskCover X where

cover_U

@[simp] theorem cover_U {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (𝔘 : FiniteCover X) (i : (cover 𝔘).ι) :
    ((cover 𝔘).U i : Set X) = refDiskNbhd 𝔘 (center 𝔘 i)

refMap

The refinement index map: each disk's centre lies in the cover set 𝔘.U (coverIdx center).

noncomputable def refMap {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (𝔘 : FiniteCover X) (i : (cover 𝔘).ι) : 𝔘.ι

isRefinement

theorem isRefinement {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (𝔘 : FiniteCover X) :
    (cover 𝔘).toFiniteCover.IsRefinement 𝔘 (refMap 𝔘)

exists_chartDiskCover_refinement

Every finite cover of compact X is refined by a chart-disk cover. For each point pick a cover set containing it (coverIdx), shrink a coordinate disk around the point to fit inside that cover set and the chart target (exists_radius_disk_subset), extract a finite subcover by compactness, and assemble the ChartDiskCover; the refinement map sends each disk's centre to its chosen cover index.

theorem exists_chartDiskCover_refinement {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (𝔘 : FiniteCover X) :
    ∃ (𝔇 : ChartDiskCover X) (r : 𝔇.ι → 𝔘.ι),
      FiniteCover.IsRefinement 𝔇.toFiniteCover 𝔘 r