14.9. Cech.ChartDiskCover🔗

Jacobians.Cech.ChartDiskCover — source

ChartDiskCover

A finite chart-disk cover: a FiniteCover together with, for each index i, a chart center i and radius i so that U i is exactly the chart-preimage of the coordinate ball ball (e i) (radius i) ⊆ ℂ (with e i = extChartAt 𝓘(ℝ,ℂ) (center i) (center i) the chart coordinate of the center). The chart extChartAt 𝓘(ℝ,ℂ) (center i) therefore restricts to a biholomorphism U i ≃ ball (e i) (radius i), which is what lets the forward operator solve ∂̄ on the whole of U i via the planar disk solve.

structure ChartDiskCover (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] extends FiniteCover X where

subset_chart_source

U i is contained in the chart source of its center.

theorem subset_chart_source (i : 𝔇.ι) :
    ((𝔇.U i : Opens X) : Set X) ⊆ (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).source

exists_bumpOuterRadius

A radius R strictly larger than the disk whose *closed* ball still lies in the chart target. Exists because the closed disk closedBall (e i) (radius i) is compact inside the open target (IsCompact.exists_cthickening_subset_open + cthickening_closedBall). The forward-solve cutoff bump uses rIn = radius i, rOut = R: it is 1 on the whole disk and supported inside the target.

theorem exists_bumpOuterRadius (i : 𝔇.ι) :
    ∃ R, 𝔇.radius i < R ∧
      Metric.closedBall (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i) (𝔇.center i)) R
        ⊆ (extChartAt 𝓘(ℝ, ℂ) (𝔇.center i)).target