16.11. Dbar.DiskAcyclicCore🔗

Jacobians.Dbar.DiskAcyclicCore — source

exists_smoothPartitionOfUnity_core

Closed-core subordinate PoU exists. For a finite family of opens U : ι → Opens X and a CLOSED set C ⊆ ⋃ i, Uᵢ, there is a smooth partition of unity over 𝓘(ℝ, ℂ), subordinate to (Uᵢ) (tsupport ρᵢ ⊆ Uᵢ), summing to 1 on C. This is the sound replacement for the (vacuous on a single-chart family) univ-subordinate PoU: the closed set C is the sum-to-one locus, avoiding the clopen obstruction. Direct application of SmoothPartitionOfUnity.exists_isSubordinate with s := C.

theorem exists_smoothPartitionOfUnity_core [T2Space X] [SigmaCompactSpace X] [IsManifold 𝓘(ℂ) ω X]
    {ι : Type} [Fintype ι] (U : ι → Opens X)
    {C : Set X} (hCclosed : IsClosed C) (hCsub : C ⊆ ⋃ i, (U i : Set X)) :
    ∃ ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, ℂ) X C,
      ρ.IsSubordinate (fun i => (U i : Set X))

smoothPartitionOfUnity_sum_eq_one_of_mem

Sum-to-one on the core, value form: a PoU over the closed set C sums to 1 at every point of C. (Repackages Mathlib's SmoothPartitionOfUnity.sum_eq_one with the finsum = Finset.sum collapse for the Fintype index.)

theorem smoothPartitionOfUnity_sum_eq_one_of_mem {ι : Type} [Fintype ι] {C : Set X}
    (ρ : SmoothPartitionOfUnity ι 𝓘(ℝ, ℂ) X C) {x : X} (hx : x ∈ C) :
    ∑ i, ρ i x = 1