The cutoff contraction of the cochains of an action presentation

Let a group G act on a type X and linearly on a k-module A through ρ, and let c : X → k be a function whose translates sum to one, ∑ᶠ g, c (g • x) = 1 for every x. For a proper action of a discrete group on a space, a cutoff function TauCeti.MulAction.IsCutoff is such a function over k = ℝ (its field finsum_smul_eq_one). The group need not be finite, and its action need not be faithful.

The inhomogeneous cochains of G with coefficients in the functions X → A (Representation.funLeft ρ X) are the functions Gⁿ × X → A. A string of n composable arrows of the action groupoid G ⋉ X is determined by its n labels and one of its points, so under this identification of the n-simplices of the nerve of G ⋉ X with Gⁿ × X, these are the cochains on the nerve of G ⋉ X with coefficients in the G-equivariant family X × A. This file constructs an explicit contracting homotopy of this complex in positive degrees, by inserting a last arrow weighted by c: $$(hf)(g_1, \dots, g_n)(x) = \sum_{g \in G} c(g \cdot x)\, f\bigl(g_1, \dots, g_n, (g\, g_1 \cdots g_n)^{-1}\bigr)(x).$$ For each x only finitely many terms are nonzero. With the sign (-1)^(n+1) on the component of degree n + 1 → n, the identity of the cochain complex is homotopic to the chain map that is the cutoff average Representation.cutoffAverage in degree 0 and zero in positive degrees, the projection onto the invariant functions placed in degree 0. In particular every positive-degree cocycle has an explicit primitive, and the positive-degree group cohomology with coefficients in X → A vanishes. As for averaging, the homotopy and the primitives are assembled from the two identities of h with the differential by TauCeti.groupCohomology.homotopyOfDCompEq and TauCeti.inhomogeneousCochains.d_smul_of_d_comp_eq.

For a finite group and the constant function |G|⁻¹, h averages over the inserted label, as in TauCeti.inhomogeneousCochains.averageLast. The operator is natural for pullback along equivariant maps Y → X, with the cutoff function pulled back to Y; restriction to an invariant subset is the case of an inclusion.

Main declarations

• TauCeti.inhomogeneousCochains.cutoffLast: the insertion of a last arrow weighted by c.
• TauCeti.inhomogeneousCochains.d_comp_cutoffLast: h ∘ d = d ∘ h + (-1)^n on (n + 1)-cochains.
• TauCeti.inhomogeneousCochains.d_zero_comp_cutoffLast: h ∘ d = Q - 1 on 0-cochains, where Q is the cutoff average.
• TauCeti.inhomogeneousCochains.cutoffLast_hom_comp: naturality for pullback along equivariant maps.
• TauCeti.groupCohomology.cutoffHomotopy: the homotopy from the identity of the cochain complex to TauCeti.groupCohomology.cutoffCochainMap, the cutoff average in degree 0.
• TauCeti.groupCohomology.subsingleton_funLeft_of_finsum_smul_eq_one: positive-degree group cohomology with coefficients in X → A vanishes.

References

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

noncomputable def TauCeti.inhomogeneousCochains.cutoffLast {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) : ↧((Fin (n + 1) → G) → ↑(Rep.of (ρ.funLeft X))) ⟶ ↧((Fin n → G) → ↑(Rep.of (ρ.funLeft X)))

The insertion x ↦ ∑ᶠ g, c (g • x) • f (y, (g * y₀ ⋯ yₙ₋₁)⁻¹) x of a last arrow into an (n + 1)-cochain f with coefficients in X → A, weighted by c, an n-cochain.

@[simp]

theorem TauCeti.inhomogeneousCochains.cutoffLast_hom_apply {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) (f : (Fin (n + 1) → G) → X → A) (y : Fin n → G) (x : X) : (ModuleCat.Hom.hom (cutoffLast ρ hc n)) f y x = ∑ᶠ (g : G), c (g • x) • f (Fin.snoc y (g * Fin.partialProd y (Fin.last n))⁻¹) x

The value of the weighted insertion of a last arrow.

theorem TauCeti.inhomogeneousCochains.d_comp_cutoffLast {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d (Rep.of (ρ.funLeft X)) (n + 1)) (cutoffLast ρ hc (n + 1)) = CategoryTheory.CategoryStruct.comp (cutoffLast ρ hc n) (inhomogeneousCochains.d (Rep.of (ρ.funLeft X)) n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑(Rep.of (ρ.funLeft X)))

The weighted insertion of a last arrow is a homotopy relation with the differential. On (n + 1)-cochains, h ∘ d = d ∘ h + (-1)^n.

theorem TauCeti.inhomogeneousCochains.d_zero_comp_cutoffLast {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d (Rep.of (ρ.funLeft X)) 0) (cutoffLast ρ hc 0) = ModuleCat.ofHom ((ρ.cutoffAverage hc).compLeft (Fin 0 → G)) - CategoryTheory.CategoryStruct.id ↧((Fin 0 → G) → X → A)

The weighted insertion of a last arrow on a coboundary of degree one. On 0-cochains, h ∘ d is the cutoff average minus the identity.

theorem TauCeti.inhomogeneousCochains.cutoffLast_hom_comp {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) {Y : Type u} [MulAction G Y] (π : Y →ₑ[id] X) (hc' : ∀ (y : Y), ∑ᶠ (g : G), (c ∘ ⇑π) (g • y) = 1) (n : ℕ) (f : ↑↧((Fin (n + 1) → G) → ↑(Rep.of (ρ.funLeft X)))) : ((ModuleCat.Hom.hom (cutoffLast ρ hc' n)) fun (z : Fin (n + 1) → G) => f z ∘ ⇑π) = fun (z : Fin n → G) => (ModuleCat.Hom.hom (cutoffLast ρ hc n)) f z ∘ ⇑π

Naturality of the weighted insertion for pullback. Pulling a cochain back along an equivariant map π : Y → X commutes with the weighted insertion of a last arrow, for the pulled-back weight c ∘ π. For the inclusion of an invariant subset this is restriction.

theorem TauCeti.inhomogeneousCochains.d_smul_cutoffLast_of_d_eq_zero {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) {n : ℕ} {f : ↑↧((Fin (n + 1) → G) → ↑(Rep.of (ρ.funLeft X)))} (hf : (ModuleCat.Hom.hom (inhomogeneousCochains.d (Rep.of (ρ.funLeft X)) (n + 1))) f = 0) : (ModuleCat.Hom.hom (inhomogeneousCochains.d (Rep.of (ρ.funLeft X)) n)) ((-1) ^ (n + 1) • (ModuleCat.Hom.hom (cutoffLast ρ hc n)) f) = f

The explicit primitive of a positive-degree cocycle. An (n + 1)-cocycle f is the coboundary of (-1)^(n+1) times its weighted insertion of a last arrow.

noncomputable def TauCeti.groupCohomology.cutoffCochainMap {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : groupCohomology.inhomogeneousCochains (Rep.of (ρ.funLeft X)) ⟶ groupCohomology.inhomogeneousCochains (Rep.of (ρ.funLeft X))

The cutoff average onto the invariant functions placed in degree 0, as an endomorphism of the complex of inhomogeneous cochains with coefficients in X → A: it is Representation.cutoffAverage on 0-cochains and zero in positive degrees.

@[simp]

theorem TauCeti.groupCohomology.cutoffCochainMap_f_zero {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : (cutoffCochainMap ρ hc).f 0 = ModuleCat.ofHom ((ρ.cutoffAverage hc).compLeft (Fin 0 → G))

In degree 0, TauCeti.groupCohomology.cutoffCochainMap is the cutoff average.

@[simp]

theorem TauCeti.groupCohomology.cutoffCochainMap_f_succ {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) : (cutoffCochainMap ρ hc).f (n + 1) = 0

In positive degrees, TauCeti.groupCohomology.cutoffCochainMap is zero.

noncomputable def TauCeti.groupCohomology.cutoffHomotopy {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) : Homotopy (CategoryTheory.CategoryStruct.id (groupCohomology.inhomogeneousCochains (Rep.of (ρ.funLeft X)))) (cutoffCochainMap ρ hc)

The cutoff contraction. The identity of the complex of inhomogeneous cochains with coefficients in X → A is homotopic to the cutoff average onto the invariant functions placed in degree 0, through the homotopy whose component from degree n + 1 to degree n is (-1)^(n+1) times the weighted insertion of a last arrow (TauCeti.groupCohomology.cutoffHomotopy_hom_succ).

@[simp]

theorem TauCeti.groupCohomology.cutoffHomotopy_hom_succ {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) : (cutoffHomotopy ρ hc).hom (n + 1) n = (-1) ^ (n + 1) • inhomogeneousCochains.cutoffLast ρ hc n

The component of TauCeti.groupCohomology.cutoffHomotopy from degree n + 1 to degree n is (-1)^(n+1) times the weighted insertion of a last arrow.

theorem TauCeti.groupCohomology.subsingleton_funLeft_of_finsum_smul_eq_one {k G A X : Type u} [CommRing k] [Group G] [AddCommGroup A] [Module k A] [MulAction G X] (ρ : Representation k G A) {c : X → k} (hc : ∀ (x : X), ∑ᶠ (g : G), c (g • x) = 1) (n : ℕ) : Subsingleton ↑(groupCohomology (Rep.of (ρ.funLeft X)) (n + 1))

Vanishing of positive-degree cohomology. If c : X → k has translates summing to one, then the group cohomology of G with coefficients in the functions X → A vanishes in positive degrees.