Comparing a contractible complex with the coinduced resolution

Mathlib computes continuous cohomology from the shifted coinduced resolution TopRep.resolution' X, the complex C(G, X) → C(G, C(G, X)) → ⋯ augmented by the constant functions X → C(G, X). Each of its terms is coinduced, so equivariant maps into it are determined by linear maps evaluated at 1 (ContRepresentation.coind₁Lift). This file records the consequence that makes it the target of comparison maps: every complex J of topological representations augmented by X and contractible by maps that need not be equivariant maps equivariantly into it, over the identity of X, and uniquely up to homotopy.

The contraction data is TopRep.ResolutionContraction X J: an equivariant augmentation ι : X ⟶ J⁰, linear maps proj : J⁰ → X and hom n : Jⁿ⁺¹ → Jⁿ with proj ∘ ι = id, ι ∘ proj + hom 0 ∘ d = id and d ∘ hom n + hom (n + 1) ∘ d = id, together with joint continuity of their conjugates x • hom n (x⁻¹ • v) in v and x. For smooth discrete representations the continuity is automatic (TauCeti.IsSmoothDiscrete.continuous_conj, in the smooth discrete module).

The comparison TopRep.ResolutionContraction.comparison is built degree by degree from the lift into a coinduced representation: F⁰ v x = x • proj (x⁻¹ • v) and Fⁿ⁺¹ v x = Fⁿ (x • hom n (x⁻¹ • v)). The conjugate x • hom n (x⁻¹ • -) of the contraction is again a contraction, and this is what makes F commute with the differentials. For a locally compact group, any two chain maps from J into a coinduced resolution TopRep.resolution' Z agreeing on the augmentation are homotopic (TopRep.ResolutionContraction.homotopy), for any Z: an equivariant map into a coinduced term that vanishes on the image of the previous differential extends along the next one (TopRep.ResolutionContraction.desc), which builds the homotopy degree by degree. Consequently the map Hⁿ(Jᴳ) → Hⁿ(G, X) on the cohomology of invariants does not depend on the choice of comparison.

The coinduced resolution is itself contracted by evaluation at 1 (TopRep.resolutionContraction), and the comparison it produces is the identity (TopRep.comparison_resolutionContraction).

A cocycle on a complex built from other resolutions, such as the tensor-induced resolution of an open subgroup in Evens' multiplicative transfer, defines a class in continuous cohomology through this comparison; the resulting maps and classes are in TauCeti.RepresentationTheory.Homological.ContCohomology.Resolution.Cohomology.

Main definitions

• TopRep.ResolutionContraction X J: a non-equivariant contraction of a complex J of topological representations onto the augmentation X → J⁰.
• TopRep.ResolutionContraction.comparison: the equivariant comparison map from J to the shifted coinduced resolution of X.
• TopRep.ResolutionContraction.homotopy: two chain maps into a coinduced resolution agreeing on the augmentation are homotopic.
• TopRep.resolutionContraction: the contraction of the coinduced resolution by evaluation at 1.

Main results

• TopRep.ResolutionContraction.ι_proj_of_d_eq_zero and TopRep.ResolutionContraction.ρ_proj_of_d_eq_zero: a degree-zero cocycle is the augmentation of its retraction, and the retraction of an invariant one is invariant.
• TopRep.ResolutionContraction.ι_comp_comparison_f_zero: the comparison lies over the identity of X, carrying the augmentation ι to the constant functions.
• TopRep.ResolutionContraction.comparison_f_zero_apply_apply and TopRep.ResolutionContraction.comparison_f_succ_apply_apply: the pointwise formulas, and TopRep.ResolutionContraction.d_comparison_f_apply: commutation with the differentials.
• TopRep.ResolutionContraction.homologyMap_eq_homologyMap_comparison: every chain map over the identity of X induces the same map on the cohomology of invariants as the comparison.
• TopRep.comparison_resolutionContraction: evaluation at 1 compares the coinduced resolution with itself by the identity.

References

• C. A. Weibel, An Introduction to Homological Algebra, Comparison Theorem 2.2.6 and its dual 2.3.7, for the comparison of a resolution with one by relatively injective objects.
• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), §§2–5, for the comparison of tensor-induced resolutions.

structure TopRep.ResolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] (X : TopRep k G) (J : CochainComplex (TopRep k G) ℕ) : Type (max v w)

A contraction of a complex J of topological representations onto X: an equivariant augmentation ι : X ⟶ J⁰ together with linear maps proj : J⁰ → X and hom n : Jⁿ⁺¹ → Jⁿ, not assumed equivariant, satisfying proj ∘ ι = id, ι ∘ proj + hom 0 ∘ d = id on J⁰ and d ∘ hom n + hom (n + 1) ∘ d = id on Jⁿ⁺¹. The conjugates x • proj (x⁻¹ • v) and x • hom n (x⁻¹ • v) are required to be jointly continuous in v and x. Such a contraction makes X → J exact, and gives the equivariant comparison TopRep.ResolutionContraction.comparison from J to the coinduced resolution of X.

• ι : X ⟶ J.X 0

  The equivariant augmentation X ⟶ J⁰.

• proj : ↑(J.X 0) →ₗ[k] ↑X

  The retraction J⁰ → X of the augmentation, which need not be equivariant.

• hom (n : ℕ) : ↑(J.X (n + 1)) →ₗ[k] ↑(J.X n)

  The contracting homotopy Jⁿ⁺¹ → Jⁿ, which need not be equivariant.

• proj_ι (x : ↑X) : self.proj ((Hom.hom self.ι) x) = x

  The retraction is a left inverse of the augmentation.

• ι_proj_add_hom_d (v : ↑(J.X 0)) : (Hom.hom self.ι) (self.proj v) + (self.hom 0) ((Hom.hom (J.d 0 1)) v) = v

  The contraction identity on J⁰: ι ∘ proj + hom 0 ∘ d = id.

• d_hom_add_hom_d (n : ℕ) (v : ↑(J.X (n + 1))) : (Hom.hom (J.d n (n + 1))) ((self.hom n) v) + (self.hom (n + 1)) ((Hom.hom (J.d (n + 1) (n + 2))) v) = v

  The contraction identity on Jⁿ⁺¹: d ∘ hom n + hom (n + 1) ∘ d = id.

• continuous_proj : Continuous fun (p : ↑(J.X 0) × G) => (X.ρ p.2) (self.proj (((J.X 0).ρ p.2⁻¹) p.1))

  The conjugates x • proj (x⁻¹ • v) of the retraction are jointly continuous.

• continuous_hom (n : ℕ) : Continuous fun (p : ↑(J.X (n + 1)) × G) => ((J.X n).ρ p.2) ((self.hom n) (((J.X (n + 1)).ρ p.2⁻¹) p.1))

  The conjugates x • hom n (x⁻¹ • v) of the contracting homotopy are jointly continuous.

theorem TopRep.ResolutionContraction.ι_proj_of_d_eq_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {v : ↑(J.X 0)} (hv : (Hom.hom (J.d 0 1)) v = 0) : (Hom.hom c.ι) (c.proj v) = v

A degree-zero cocycle is the augmentation of its retraction: if d v = 0 in degree zero, then v = ι (proj v).

theorem TopRep.ResolutionContraction.ρ_proj_of_d_eq_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {v : ↑(J.X 0)} (hv : (Hom.hom (J.d 0 1)) v = 0) (hinv : ∀ (g : G), ((J.X 0).ρ g) v = v) (g : G) : (X.ρ g) (c.proj v) = c.proj v

The retraction of an invariant degree-zero cocycle is invariant.

noncomputable def TopRep.ResolutionContraction.comparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] : J ⟶ X.resolution'

The comparison map from a complex contracted onto X to the shifted coinduced resolution of X. It is equivariant, commutes with the differentials, and lies over the identity of X (TopRep.ResolutionContraction.ι_comp_comparison_f_zero). In degree 0 it is v ↦ (x ↦ x • proj (x⁻¹ • v)), and in degree n + 1 it is v ↦ (x ↦ Fⁿ (x • hom n (x⁻¹ • v))) for the degree-n component Fⁿ.

@[simp]

theorem TopRep.ResolutionContraction.comparison_f_zero_apply_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] (v : ↑(J.X 0)) (x : G) : ((Hom.hom (c.comparison.f 0)) v) x = (X.ρ x) (c.proj (((J.X 0).ρ x⁻¹) v))

The comparison in degree 0, at a point: F⁰ v x = x • proj (x⁻¹ • v).

@[simp]

theorem TopRep.ResolutionContraction.comparison_f_succ_apply_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] (n : ℕ) (v : ↑(J.X (n + 1))) (x : G) : ((Hom.hom (c.comparison.f (n + 1))) v) x = (Hom.hom (c.comparison.f n)) (((J.X n).ρ x) ((c.hom n) (((J.X (n + 1)).ρ x⁻¹) v)))

The comparison in degree n + 1, at a point: Fⁿ⁺¹ v x = Fⁿ (x • hom n (x⁻¹ • v)).

@[simp]

theorem TopRep.ResolutionContraction.ι_comp_comparison_f_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] : CategoryTheory.CategoryStruct.comp c.ι (c.comparison.f 0) = X.d 0

The comparison lies over the identity of X: it carries the augmentation ι to the augmentation d X 0 of the coinduced resolution by constant functions.

@[simp]

theorem TopRep.ResolutionContraction.ι_comp_comparison_f_zero_assoc {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] {Z : TopRep k G} (h : X.resolution'X 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp c.ι (CategoryTheory.CategoryStruct.comp (c.comparison.f 0) h) = CategoryTheory.CategoryStruct.comp (X.d 0) h

The comparison lies over the identity of X: it carries the augmentation ι to the augmentation d X 0 of the coinduced resolution by constant functions.

theorem TopRep.ResolutionContraction.d_comparison_f_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] (n : ℕ) (v : ↑(J.X n)) : (Hom.hom (X.d (n + 1))) ((Hom.hom (c.comparison.f n)) v) = (Hom.hom (c.comparison.f (n + 1))) ((Hom.hom (J.d n (n + 1))) v)

The comparison commutes with the differentials, on elements.

noncomputable def TopRep.ResolutionContraction.desc {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Y : TopRep k G} (n : ℕ) (r : J.X n ⟶ Y.coind₁) : J.X (n + 1) ⟶ Y.coind₁

The extension of an equivariant map r : Jⁿ ⟶ C(G, Y) along the differential Jⁿ → Jⁿ⁺¹: the lift to the coinduced representation of v ↦ r (hom n v) 1. When r vanishes on the image of the previous differential, or on the augmentation if n = 0, it is an extension (TopRep.ResolutionContraction.d_comp_desc_zero, TopRep.ResolutionContraction.d_comp_desc_succ).

theorem TopRep.ResolutionContraction.desc_apply_one {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Y : TopRep k G} (n : ℕ) (r : J.X n ⟶ Y.coind₁) (v : ↑(J.X (n + 1))) : ((Hom.hom (c.desc n r)) v) 1 = ((Hom.hom r) ((c.hom n) v)) 1

The extension desc at the point 1: desc n r v 1 = r (hom n v) 1.

theorem TopRep.ResolutionContraction.d_comp_desc_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Y : TopRep k G} (r : J.X 0 ⟶ Y.coind₁) (hr : CategoryTheory.CategoryStruct.comp c.ι r = 0) : CategoryTheory.CategoryStruct.comp (J.d 0 1) (c.desc 0 r) = r

In degree 0, desc extends a map killing the augmentation along the first differential.

theorem TopRep.ResolutionContraction.d_comp_desc_succ {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Y : TopRep k G} (n : ℕ) (r : J.X (n + 1) ⟶ Y.coind₁) (hr : CategoryTheory.CategoryStruct.comp (J.d n (n + 1)) r = 0) : CategoryTheory.CategoryStruct.comp (J.d (n + 1) (n + 2)) (c.desc (n + 1) r) = r

In positive degree, desc extends a map killing the image of the previous differential along the next one.

noncomputable def TopRep.ResolutionContraction.nullHomotopy {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Y : ℕ → TopRep k G} {δ : (p : ℕ) → (Y p).coind₁ ⟶ (Y (p + 1)).coind₁} {hδ : ∀ (p : ℕ), CategoryTheory.CategoryStruct.comp (δ p) (δ (p + 1)) = 0} (e : J ⟶ CochainComplex.of (fun (p : ℕ) => (Y p).coind₁) δ hδ) (he : CategoryTheory.CategoryStruct.comp c.ι (e.f 0) = 0) : Homotopy e 0

A chain map into a complex of coinduced representations killing the augmentation is null-homotopic, by an equivariant homotopy whose components are built degree by degree with desc. The target is any complex whose terms are coinduced, Kᵖ = C(G, Yₚ): the coinduced resolution of any Z, not only of X, and its shifts.

noncomputable def TopRep.ResolutionContraction.homotopy {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] {Z : TopRep k G} (φ ψ : J ⟶ Z.resolution') (h : CategoryTheory.CategoryStruct.comp c.ι (φ.f 0) = CategoryTheory.CategoryStruct.comp c.ι (ψ.f 0)) : Homotopy φ ψ

Uniqueness of comparisons up to homotopy. Two chain maps from J to the coinduced resolution of Z that agree on the augmentation ι are homotopic. Taking Z = X gives uniqueness of the comparison; other Z compare chain maps lying over a coefficient morphism X ⟶ Z.

noncomputable def TopRep.ResolutionContraction.homotopyComparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] (φ : J ⟶ X.resolution') (hφ : CategoryTheory.CategoryStruct.comp c.ι (φ.f 0) = X.d 0) : Homotopy φ c.comparison

Every chain map from J to the coinduced resolution of X over the identity of X is homotopic to the comparison.

theorem TopRep.ResolutionContraction.homologyMap_eq_homologyMap_comparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [IsTopologicalGroup G] [LocallyCompactSpace G] (φ : J ⟶ X.resolution') (hφ : CategoryTheory.CategoryStruct.comp c.ι (φ.f 0) = X.d 0) (n : ℕ) : HomologicalComplex.homologyMap (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).map φ) n = HomologicalComplex.homologyMap (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).map c.comparison) n

The comparison is canonical on cohomology. On the cohomology of the invariants, every chain map from J to the coinduced resolution of X over the identity of X induces the same map Hⁿ(Jᴳ) → Hⁿ(G, X) as the comparison.

noncomputable def TopRep.resolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) : X.ResolutionContraction X.resolution'

The contraction of the coinduced resolution by evaluation at 1: the augmentation is the inclusion of constant functions, and both the retraction and the contracting homotopy evaluate the outermost variable at 1. Its conjugates are evaluations at other points, which are jointly continuous because G is locally compact.

@[simp]

theorem TopRep.resolutionContraction_ι {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) : X.resolutionContraction.ι = X.d 0

The augmentation of the coinduced resolution is the inclusion of constant functions.

@[simp]

theorem TopRep.resolutionContraction_proj_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) (v : ↑(X.resolution'.X 0)) : X.resolutionContraction.proj v = v 1

The retraction of the coinduced resolution evaluates at 1.

@[simp]

theorem TopRep.resolutionContraction_hom_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) (n : ℕ) (v : ↑(X.resolution'.X (n + 1))) : (X.resolutionContraction.hom n) v = v 1

The contracting homotopy of the coinduced resolution evaluates at 1.

theorem TopRep.comparison_resolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) : X.resolutionContraction.comparison = CategoryTheory.CategoryStruct.id X.resolution'

The coinduced resolution compares with itself by the identity: the comparison map given by its contraction by evaluation at 1 is the identity.