A contraction of the coinduced resolution

After forgetting the action and topology, Mathlib's shifted coinduced resolution C(G, X) → C(G, C(G, X)) → ⋯ is homotopy equivalent to X concentrated in degree zero. The inclusion sends a coefficient to the constant function, the projection evaluates at 1, and evaluation at 1 in each positive degree gives the contracting homotopy.

This is the splitting needed when tensoring resolutions: homotopy equivalences can be tensored without any flatness assumption. The contraction is on the underlying modules; evaluation at 1 is not equivariant and does not contract the complex of invariant cochains.

The construction follows the recursion of TopRep.d and the evaluation identity recorded in TopRep.d_sum_apply_add_sum_d_apply.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Transactions of the American Mathematical Society 108 (1963), §§2–5, for tensor resolutions.

@[reducible, inline]

noncomputable abbrev TopRep.resolutionModuleComplex {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : CochainComplex (ModuleCat R) ℕ

The shifted coinduced resolution with its action and topology forgotten.

noncomputable def TopRep.resolutionModuleIncl {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : (CochainComplex.single₀ (ModuleCat R)).obj ↧↑X ⟶ X.resolutionModuleComplex

The augmentation of the underlying shifted resolution, by constant functions.

noncomputable def TopRep.resolutionModuleProj {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.resolutionModuleComplex ⟶ (CochainComplex.single₀ (ModuleCat R)).obj ↧↑X

The projection of the underlying shifted resolution onto its coefficients.

@[simp]

theorem TopRep.resolutionModuleIncl_f_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.resolutionModuleIncl.f 0 = ModuleCat.ofHom ↑(Hom.hom (X.d 0)).toContinuousLinearMap

The augmentation in degree zero is the original constant-function map.

@[simp]

theorem TopRep.resolutionModuleProj_f_zero {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.resolutionModuleProj.f 0 = ModuleCat.ofHom ↑(ContinuousMap.evalCLM R 1)

The projection in degree zero evaluates at the identity.

@[simp]

theorem TopRep.resolutionModuleProj_f_succ {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) : X.resolutionModuleProj.f (n + 1) = 0

The projection vanishes in every positive degree.

@[simp]

theorem TopRep.resolutionModuleIncl_comp_proj {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : CategoryTheory.CategoryStruct.comp X.resolutionModuleIncl X.resolutionModuleProj = CategoryTheory.CategoryStruct.id ((CochainComplex.single₀ (ModuleCat R)).obj ↧↑X)

Evaluation retracts the constant-function augmentation.

noncomputable def TopRep.resolutionModuleHomotopy {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : Homotopy (CategoryTheory.CategoryStruct.id X.resolutionModuleComplex) (CategoryTheory.CategoryStruct.comp X.resolutionModuleProj X.resolutionModuleIncl)

Evaluation contracts the identity onto the coefficient summand of the underlying shifted resolution.

@[simp]

theorem TopRep.resolutionModuleHomotopy_hom_succ {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) : X.resolutionModuleHomotopy.hom (n + 1) n = ModuleCat.ofHom ↑(ContinuousMap.evalCLM R 1)

The contracting homotopy in every positive degree evaluates the outermost variable at 1.

noncomputable def TopRep.resolutionModuleHomotopyEquiv {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : HomotopyEquiv ((CochainComplex.single₀ (ModuleCat R)).obj ↧↑X) X.resolutionModuleComplex

The underlying shifted coinduced resolution is homotopy equivalent to the coefficient module concentrated in degree zero. No discreteness, compactness or flatness is needed.

@[simp]

theorem TopRep.resolutionModuleHomotopyEquiv_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.resolutionModuleHomotopyEquiv.hom = X.resolutionModuleIncl

The forward map of the homotopy equivalence is the constant-function augmentation.

@[simp]

theorem TopRep.resolutionModuleHomotopyEquiv_inv {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : X.resolutionModuleHomotopyEquiv.inv = X.resolutionModuleProj

The inverse map of the homotopy equivalence is evaluation in degree zero.