Cutoff functions for étale groupoids

Let C be a quiver, such as a groupoid, whose objects and total arrows Quiver.Total C carry topologies. A cutoff function (TauCeti.Quiver.IsCutoff) is a nonnegative function c on the objects such that

• for every object x, the values of c at the targets of the arrows with source x sum to one, ∑ᶠ a ∈ Quiver.Total.left ⁻¹' {x}, c a.right = 1;
• for every compact set K of objects, the arrows with source in K and target in the support of c form a compact set.

The second condition makes the source map proper on the support of c composed with the target (TauCeti.Quiver.IsCutoff.isProperMap_left). When the source is a local homeomorphism it also makes each of the sums above finite (TauCeti.Quiver.IsCutoff.finite_preimage_left_singleton_inter). Every arrow is counted, so isotropy arrows acting trivially near their object, and with them the ineffective isotropy of an orbifold presentation, are retained.

For a groupoid, dividing a nonnegative function β by its sums x ↦ ∑ᶠ a, β a.right over the arrows with source x gives a cutoff function, as soon as every orbit meets the locus where β is nonzero and β satisfies the compactness condition (TauCeti.Quiver.isCutoff_div_finsum). The sums are constant along orbits, by Quiver.Total.finsum_mem_preimage_left_singleton_eq_of_iso.

Cutoff functions turn sums over the arrows of a proper groupoid into locally finite sums, as needed to average data along its orbits. Smooth cutoff functions of proper étale manifold groupoids are constructed in TauCeti.Geometry.Manifold.Groupoid.Cutoff. For the action groupoid of a discrete group, TauCeti.MulAction.IsCutoff is the corresponding notion.

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.

structure TauCeti.Quiver.IsCutoff {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] (c : C → ℝ) : Prop

A cutoff function for a topological quiver, such as a topological groupoid: a nonnegative function on objects whose values at the targets of the arrows with each given source sum to one, and such that the arrows with source in a compact set and target in its support form a compact set.

• nonneg (x : C) : 0 ≤ c x

  A cutoff function is nonnegative.

• finsum_eq_one (x : C) : ∑ᶠ (a : Quiver.Total C) (_ : a ∈ Quiver.Total.left ⁻¹' {x}), c a.right = 1

  The values of a cutoff function at the targets of the arrows with source x sum to one.

• isCompact_preimage_inter ⦃K : Set C⦄ (hK : IsCompact K) : IsCompact (Quiver.Total.left ⁻¹' K ∩ Quiver.Total.right ⁻¹' tsupport c)

  The arrows with source in a compact set and target in the support of a cutoff function form a compact set.

theorem TauCeti.Quiver.finite_preimage_left_singleton_inter {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {R : Type u_2} [Zero R] {f : C → R} (hs : IsLocalHomeomorph Quiver.Total.left) (hf : ∀ ⦃K : Set C⦄, IsCompact K → IsCompact (Quiver.Total.left ⁻¹' K ∩ Quiver.Total.right ⁻¹' tsupport f)) (x : C) : (Quiver.Total.left ⁻¹' {x} ∩ Quiver.Total.right ⁻¹' tsupport f).Finite

If the source map is a local homeomorphism and the arrows with source in a compact set and target in the support of f form a compact set, then only finitely many arrows with a given source have their target in the support of f.

theorem TauCeti.Quiver.isCompact_preimage_left_inter_tsupport_comp {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {R : Type u_2} [Zero R] {f : C → R} (ht : Continuous Quiver.Total.right) {K : Set C} (hf : IsCompact (Quiver.Total.left ⁻¹' K ∩ Quiver.Total.right ⁻¹' tsupport f)) : IsCompact (Quiver.Total.left ⁻¹' K ∩ tsupport (f ∘ Quiver.Total.right))

If the arrows with source in a compact set K and target in the support of f form a compact set, then so do the arrows with source in K lying in the support of f composed with the target.

theorem TauCeti.Quiver.finsum_mem_preimage_left_singleton_pos {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] (hs : IsLocalHomeomorph Quiver.Total.left) {f : C → ℝ} (hf0 : ∀ (x : C), 0 ≤ f x) (hf : ∀ ⦃K : Set C⦄, IsCompact K → IsCompact (Quiver.Total.left ⁻¹' K ∩ Quiver.Total.right ⁻¹' tsupport f)) {x : C} (hx : ∃ a ∈ Quiver.Total.left ⁻¹' {x}, f a.right ≠ 0) : 0 < ∑ᶠ (a : Quiver.Total C) (_ : a ∈ Quiver.Total.left ⁻¹' {x}), f a.right

If the source map is a local homeomorphism, f is nonnegative and nonzero at the target of some arrow with source x, and the arrows with source in a compact set and target in the support of f form a compact set, then the sum of f over the targets of the arrows with source x is positive.

theorem TauCeti.Quiver.IsCutoff.finite_preimage_left_singleton_inter {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {c : C → ℝ} (hc : IsCutoff c) (hs : IsLocalHomeomorph Quiver.Total.left) (x : C) : (Quiver.Total.left ⁻¹' {x} ∩ Quiver.Total.right ⁻¹' tsupport c).Finite

If the source map is a local homeomorphism, only finitely many arrows with a given source have their target in the support of a cutoff function.

theorem TauCeti.Quiver.IsCutoff.isCompact_preimage_left_inter_tsupport_comp {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {c : C → ℝ} (hc : IsCutoff c) (ht : Continuous Quiver.Total.right) {K : Set C} (hK : IsCompact K) : IsCompact (Quiver.Total.left ⁻¹' K ∩ tsupport (c ∘ Quiver.Total.right))

The arrows with source in a compact set and lying in the support of a cutoff function composed with the target form a compact set.

theorem TauCeti.Quiver.IsCutoff.isProperMap_left {C : Type u_1} [Quiver C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] {c : C → ℝ} [T2Space C] [CompactlyCoherentSpace C] (hc : IsCutoff c) (hs : Continuous Quiver.Total.left) (ht : Continuous Quiver.Total.right) : IsProperMap fun (a : ↑(tsupport (c ∘ Quiver.Total.right))) => (↑a).left

The source map is proper on the support of a cutoff function composed with the target map.

theorem TauCeti.Quiver.isCutoff_div_finsum {C : Type u_1} [CategoryTheory.Groupoid C] [TopologicalSpace C] [TopologicalSpace (Quiver.Total C)] (hs : IsLocalHomeomorph Quiver.Total.left) {β : C → ℝ} (hβ : ∀ (x : C), 0 ≤ β x) (hfin : ∀ ⦃K : Set C⦄, IsCompact K → IsCompact (Quiver.Total.left ⁻¹' K ∩ Quiver.Total.right ⁻¹' tsupport β)) (hpos : ∀ (x : C), ∃ a ∈ Quiver.Total.left ⁻¹' {x}, β a.right ≠ 0) : IsCutoff fun (x : C) => β x / ∑ᶠ (a : Quiver.Total C) (_ : a ∈ Quiver.Total.left ⁻¹' {x}), β a.right

In a groupoid whose source map is a local homeomorphism, dividing a nonnegative function β by its sums over the targets of the arrows with each given source gives a cutoff function. This needs every orbit to meet the locus where β is nonzero, and the arrows with source in a compact set and target in the support of β to form a compact set.