19.23. Finiteness.ChartDiskLeray🔗

Jacobians.Finiteness.ChartDiskLeray — source

shrinkSetOpens

The shrinking sets as Opens X (they are open, shrinkSet_isOpen).

noncomputable def shrinkSetOpens (a : 𝔇.ι) : Opens X

shrinkSetOpens_coe

@[simp] theorem shrinkSetOpens_coe (a : 𝔇.ι) :
    ((𝔇.shrinkSetOpens a : Opens X) : Set X) = 𝔇.shrinkSet a

exists_shrinkPoU

The shrinking-level smooth PoU exists (sum-to-one on all of X). A smooth partition of unity over 𝓘(ℝ,ℂ), subordinate to the covering shrinkings (V_a), summing to 1 on ALL of X (the closed sum-to-one locus is univ, since the shrinkings cover X). This is the foundation the Forster 14.6 smooth split consumes: the PoU is subordinate to the SHRINKINGS, where the input cocycle is defined.

theorem exists_shrinkPoU :
    ∃ ρ : SmoothPartitionOfUnity 𝔇.ι 𝓘(ℝ, ℂ) X Set.univ,
      ρ.IsSubordinate (fun a => (𝔇.shrinkSet a))

shrinkPoU

A fixed shrinking-level smooth PoU subordinate to (V_a), summing to 1 on all of X.

noncomputable def shrinkPoU : SmoothPartitionOfUnity 𝔇.ι 𝓘(ℝ, ℂ) X Set.univ

shrinkPoU_subordinate

The shrinking PoU is subordinate to (V_a): tsupport ρ_a ⊆ V_a.

theorem shrinkPoU_subordinate :
    (𝔇.shrinkPoU).IsSubordinate (fun a => (𝔇.shrinkSet a))

sum_shrinkPoU_eq_one

Sum-to-one EVERYWHERE. ∑ a, ρ_a x = 1 for every x : X.

theorem sum_shrinkPoU_eq_one (x : X) :
    ∑ a, (𝔇.shrinkPoU) a x = 1

shrinkPoU_tsupport_subset

The subordination as a tsupport containment: tsupport (ρ_a) ⊆ V_a.

theorem shrinkPoU_tsupport_subset (a : 𝔇.ι) :
    tsupport (𝔇.shrinkPoU a) ⊆ 𝔇.shrinkSet a