Contractions of inhomogeneous cochains from operators lowering the degree

Let A be a k-linear representation of a group G, and let h n : Cⁿ⁺¹(G, A) → Cⁿ(G, A) be linear maps between the inhomogeneous cochains satisfying $$h \circ d = d \circ h + (-1)^n \text{ on } (n + 1)\text{-cochains}, \qquad h \circ d = P - 1 \text{ on } 0\text{-cochains}$$ for an endomorphism P of the 0-cochains. The maps (-1)^(n+1) • h n then satisfy the sign-free identities of CochainComplex.homotopyOfDCompEq. So P is a cochain map when placed in degree 0 (TauCeti.groupCohomology.comp_d_zero_eq_zero), and the maps (-1)^(n+1) • h n form a homotopy from the identity of inhomogeneousCochains A to it. Every positive-degree cocycle f is the coboundary of (-1)^(n+1) h f.

This is the formal part shared by the contractions that insert a last argument: averaging over a finite group (TauCeti.inhomogeneousCochains.averageLast) and weighting by a cutoff function (TauCeti.inhomogeneousCochains.cutoffLast).

Main declarations

• TauCeti.inhomogeneousCochains.d_smul_of_d_comp_eq: the explicit primitive of a positive-degree cocycle.
• TauCeti.groupCohomology.homotopyOfDCompEq: the homotopy from the identity to P placed in degree 0 by CochainComplex.ofDegreeZero.

theorem TauCeti.inhomogeneousCochains.d_smul_of_d_comp_eq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {n : ℕ} {h : (m : ℕ) → ↧((Fin (m + 1) → G) → ↑A) ⟶ ↧((Fin m → G) → ↑A)} (hd : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A (n + 1)) (h (n + 1)) = CategoryTheory.CategoryStruct.comp (h n) (inhomogeneousCochains.d A n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑A)) {f : ↑↧((Fin (n + 1) → G) → ↑A)} (hf : (ModuleCat.Hom.hom (inhomogeneousCochains.d A (n + 1))) f = 0) : (ModuleCat.Hom.hom (inhomogeneousCochains.d A n)) ((-1) ^ (n + 1) • (ModuleCat.Hom.hom (h n)) f) = f

The explicit primitive of a positive-degree cocycle. If h ∘ d = d ∘ h + (-1)^n on (n + 1)-cochains, then an (n + 1)-cocycle f is the coboundary of (-1)^(n+1) • h f.

theorem TauCeti.groupCohomology.comp_d_zero_eq_zero {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {P : ↧((Fin 0 → G) → ↑A) ⟶ ↧((Fin 0 → G) → ↑A)} {h : (n : ℕ) → ↧((Fin (n + 1) → G) → ↑A) ⟶ ↧((Fin n → G) → ↑A)} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A (n + 1)) (h (n + 1)) = CategoryTheory.CategoryStruct.comp (h n) (inhomogeneousCochains.d A n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑A)) (hd₀ : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A 0) (h 0) = P - CategoryTheory.CategoryStruct.id ↧((Fin 0 → G) → ↑A)) : CategoryTheory.CategoryStruct.comp P ((groupCohomology.inhomogeneousCochains A).d 0 1) = 0

If h ∘ d = d ∘ h + (-1)^n on positive-degree cochains and h ∘ d = P - 1 on 0-cochains, then the composite of P with the differential vanishes.

noncomputable def TauCeti.groupCohomology.homotopyOfDCompEq {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {P : ↧((Fin 0 → G) → ↑A) ⟶ ↧((Fin 0 → G) → ↑A)} {h : (n : ℕ) → ↧((Fin (n + 1) → G) → ↑A) ⟶ ↧((Fin n → G) → ↑A)} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A (n + 1)) (h (n + 1)) = CategoryTheory.CategoryStruct.comp (h n) (inhomogeneousCochains.d A n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑A)) (hd₀ : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A 0) (h 0) = P - CategoryTheory.CategoryStruct.id ↧((Fin 0 → G) → ↑A)) : Homotopy (CategoryTheory.CategoryStruct.id (groupCohomology.inhomogeneousCochains A)) ((groupCohomology.inhomogeneousCochains A).ofDegreeZero P ⋯)

The contraction defined by an operator lowering the degree. If h ∘ d = d ∘ h + (-1)^n on (n + 1)-cochains and h ∘ d = P - 1 on 0-cochains, then the identity of the complex of inhomogeneous cochains is homotopic to P placed in degree 0, through the homotopy whose component from degree n + 1 to degree n is (-1)^(n+1) • h n (TauCeti.groupCohomology.homotopyOfDCompEq_hom_succ).

@[simp]

theorem TauCeti.groupCohomology.homotopyOfDCompEq_hom_succ {k G : Type u} [CommRing k] [Group G] {A : Rep k G} {P : ↧((Fin 0 → G) → ↑A) ⟶ ↧((Fin 0 → G) → ↑A)} {h : (n : ℕ) → ↧((Fin (n + 1) → G) → ↑A) ⟶ ↧((Fin n → G) → ↑A)} (hd : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A (n + 1)) (h (n + 1)) = CategoryTheory.CategoryStruct.comp (h n) (inhomogeneousCochains.d A n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑A)) (hd₀ : CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A 0) (h 0) = P - CategoryTheory.CategoryStruct.id ↧((Fin 0 → G) → ↑A)) (n : ℕ) : (homotopyOfDCompEq hd hd₀).hom (n + 1) n = (-1) ^ (n + 1) • h n

The component of TauCeti.groupCohomology.homotopyOfDCompEq from degree n + 1 to degree n is (-1)^(n+1) • h n.