Smooth cutoff functions for proper étale groupoids

Let C be a groupoid whose objects form a Hausdorff σ-compact finite-dimensional real manifold and whose total arrows form a Hausdorff manifold, with source and target C^n local diffeomorphisms and proper source-target map a ↦ (a.left, a.right). Then C has a C^n cutoff function (TauCeti.Quiver.exists_isCutoff_contMDiff): a nonnegative C^n function c on objects with ∑ᶠ a ∈ Quiver.Total.left ⁻¹' {x}, c a.right = 1 for every object x, such that the source map is proper on the support of c composed with the target. No effectiveness is assumed: every arrow is counted, so isotropy arrows acting trivially near their object are retained.

This generalizes the cutoff functions of proper actions of discrete groups, TauCeti.MulAction.exists_isCutoff_contMDiff, to proper étale groupoids. Cutoff functions are used to average data over the arrows of a proper groupoid, and so to contract complexes of cochains on its nerve.

Implementation notes

The construction starts from a nonnegative smooth function β on objects which is nonzero somewhere on every isomorphism class, and whose support meets the preimage of each compact set of the coarse space of isomorphism classes in a compact set (TauCeti.exists_contMDiff_nonneg_isCompact_tsupport_inter_preimage). The properness of the source-target map then gives the compactness condition of a cutoff function, and c = β / ∑ᶠ a, β a.right by TauCeti.Quiver.isCutoff_div_finsum. Near each object the denominator is a finite sum of β composed with the target and local inverses of the source (IsLocalHomeomorph.eventually_finsum_mem_preimage_singleton_eq_sum), hence C^n.

References

• M. Crainic, Differentiable and algebroid cohomology, van Est isomorphisms, and characteristic classes, Comment. Math. Helv. 78 (2003), Section 2, for cutoff functions on proper groupoids.

theorem TauCeti.Quiver.exists_isCutoff_contMDiff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {E' : Type u_3} [NormedAddCommGroup E'] [NormedSpace ℝ E'] {H' : Type u_4} [TopologicalSpace H'] {J : ModelWithCorners ℝ E' H'} {C : Type u_5} [CategoryTheory.Groupoid C] [TopologicalSpace C] [ChartedSpace H C] [IsManifold I (↑⊤) C] [T2Space C] [SigmaCompactSpace C] [TopologicalSpace (Quiver.Total C)] [ChartedSpace H' (Quiver.Total C)] [T2Space (Quiver.Total C)] {n : ℕ∞} (hp : IsProperMap fun (a : Quiver.Total C) => (a.left, a.right)) (hs : IsLocalDiffeomorph J I (↑n) Quiver.Total.left) (ht : IsLocalDiffeomorph J I (↑n) Quiver.Total.right) : ∃ (c : C → ℝ), IsCutoff c ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) c

Smooth cutoff functions of proper étale groupoids. A groupoid whose objects form a Hausdorff σ-compact finite-dimensional real manifold, whose total arrows form a Hausdorff manifold, whose source and target are C^n local diffeomorphisms, and whose source-target map is proper, has a C^n cutoff function.