Smooth functions meeting every fiber of an open quotient map

Let π : M → Q be an open quotient map from a Hausdorff σ-compact finite-dimensional real manifold onto a Hausdorff space. Then M has a nonnegative smooth function β which is nonzero somewhere on every fiber of π, and whose support meets the preimage of each compact subset of Q in a compact set (TauCeti.exists_contMDiff_nonneg_isCompact_tsupport_inter_preimage).

Such functions are the starting point for cutoff functions: dividing β by its sums along orbits gives the cutoff functions of proper actions of discrete groups (TauCeti.MulAction.exists_isCutoff_contMDiff), where Q is the orbit space, and of proper étale groupoids (TauCeti.Quiver.exists_isCutoff_contMDiff), where Q is the coarse space of isomorphism classes.

Implementation notes

Note that Q is paracompact. Cover it by a locally finite family of open sets O y contained in the images of compact sets K₀ y, shrink it to a cover by sets V y with closure (V y) ⊆ O y, and sum smooth bump functions equal to one on K₀ y ∩ π ⁻¹' closure (V y) and supported in a compact neighbourhood of K₀ y over O y.

References

• N. Bourbaki, Integration II, Chapter VII, §2, for Bruhat functions of proper actions.

theorem TauCeti.exists_contMDiff_nonneg_isCompact_tsupport_inter_preimage {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M] {Q : Type u_4} [TopologicalSpace Q] [T2Space Q] {π : M → Q} (hπ : IsOpenQuotientMap π) : ∃ (β : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑⊤) β ∧ (∀ (x : M), 0 ≤ β x) ∧ (∀ ⦃L : Set Q⦄, IsCompact L → IsCompact (tsupport β ∩ π ⁻¹' L)) ∧ ∀ (x : M), ∃ (z : M), π z = π x ∧ β z ≠ 0

Let π : M → Q be an open quotient map from a Hausdorff σ-compact finite-dimensional real manifold onto a Hausdorff space, such as the projection to the orbit space of a proper action or to the coarse space of a proper étale groupoid. Then M has a nonnegative smooth function which is nonzero somewhere on every fiber of π, and whose topological support meets the preimage of each compact set in a compact set.