Continuous cohomology computed from a contracted complex

Let J be a complex of topological G-representations with a contraction c : TopRep.ResolutionContraction X J onto X, whose maps need not be equivariant. The comparison c.comparison : J ⟶ TopRep.resolution' X induces a map on the cohomology of invariants

c.cohomologyMap n : Hⁿ(Jᴳ) ⟶ Hⁿ(G, X),

and every G-invariant cocycle z of J has a class c.cohomologyClass z in Mathlib's continuous cohomology: the class of the homogeneous cocycle into which the comparison carries z, which is also the image of the class of z under c.cohomologyMap (TopRep.ResolutionContraction.cohomologyMap_homologyπ). This is how a cocycle on a complex built from other resolutions, such as the diagonal tensor of a cocycle on the tensor-induced resolution of an open subgroup in Evens' multiplicative transfer, is read as a continuous cohomology class.

Over a locally compact group the comparison is unique up to homotopy, which makes these maps canonical:

• they do not depend on the contraction, only on its augmentation (TopRep.ResolutionContraction.cohomologyMap_eq_of_ι_eq);
• more generally, two maps of degree n from J into the coinduced resolution of any Z, commuting with the differentials and agreeing on the augmentation, give an invariant cocycle the same class (TopRep.ResolutionContraction.cochainClass_eq_of_ι_comp_eq); such maps carry invariant cocycles to homogeneous cocycles (TopRep.d_mapInvariants_apply_of_comm);
• they are natural in chain maps of contracted complexes lying over a coefficient morphism (TopRep.ResolutionContraction.cohomologyMap_comp_coeffMap); in particular a chain map over the identity of X preserves classes (TopRep.ResolutionContraction.cohomologyClass_map);
• for the coinduced resolution contracted by evaluation at 1, they are the identity and the ordinary class map (TopRep.cohomologyMap_resolutionContraction, TopRep.cohomologyClass_resolutionContraction).

Already without local compactness, the class is linear in the cocycle and cohomologous invariant cocycles have the same class (TopRep.ResolutionContraction.cohomologyClass_eq_of_sub_eq_d). In degree zero a cocycle is the augmentation of its retraction, so its class is the degree-zero class of that invariant vector (TopRep.ResolutionContraction.cohomologyClass_eq_degreeZeroClass).

Main definitions

• TopRep.ResolutionContraction.cohomologyMap: the map Hⁿ(Jᴳ) ⟶ Hⁿ(G, X) induced by the comparison.
• TopRep.ResolutionContraction.cohomologyClass: the class in Hⁿ(G, X) of an invariant cocycle of J.

Main results

• TopRep.ResolutionContraction.cohomologyMap_homologyπ: the class of an invariant cocycle is the image of its class in Hⁿ(Jᴳ).
• TopRep.ResolutionContraction.cohomologyClass_eq_of_sub_eq_d: cohomologous invariant cocycles have the same class.
• TopRep.ResolutionContraction.cohomologyClass_eq_degreeZeroClass: classes in degree zero are degree-zero classes of invariant vectors.
• TopRep.ResolutionContraction.cohomologyMap_eq_of_ι_eq and TopRep.ResolutionContraction.cohomologyClass_eq_of_ι_eq: independence of the contraction.
• TopRep.ResolutionContraction.cochainClass_eq_of_ι_comp_eq: maps of degree n from a contracted complex into the coinduced resolution, commuting with the differentials and agreeing on the augmentation, give invariant cocycles the same class.
• TopRep.ResolutionContraction.cohomologyMap_comp_coeffMap, TopRep.ResolutionContraction.homologyMap_comp_cohomologyMap, TopRep.ResolutionContraction.coeffMap_cohomologyClass and TopRep.ResolutionContraction.cohomologyClass_map: naturality in the contracted complex and in the coefficients.

References

• C. A. Weibel, An Introduction to Homological Algebra, Comparison Theorem 2.3.7.
• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), §§2–5.

theorem TopRep.d_mapInvariants_apply_of_comm {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {Z : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} {n : ℕ} (φ : (p : ℕ) → J.X p ⟶ Z.resolution'.X (p + n)) (hφ : ∀ (p : ℕ), CategoryTheory.CategoryStruct.comp (φ p) (Z.resolution'.d (p + n) (p + 1 + n)) = CategoryTheory.CategoryStruct.comp (J.d p (p + 1)) (φ (p + 1))) {p : ℕ} (a : ↥(J.X p).ρ.invariants) (ha : (Hom.hom (J.d p (p + 1))) ↑a = 0) : (TopModuleCat.Hom.hom (Z.homogeneousCochains.d (p + n) (p + n + 1))) ((Hom.hom (φ p)).mapInvariants a) = 0

A family of maps Jᵖ ⟶ C^{p + n} into the coinduced resolution of Z, raising degrees by n and commuting with the differentials, carries an invariant cocycle of J to a homogeneous cocycle of Z.

noncomputable def TopRep.ResolutionContraction.cohomologyMap {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (n : ℕ) : (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).obj J).homology n ⟶ continuousCohomology n X

The map Hⁿ(Jᴳ) ⟶ Hⁿ(G, X) of a contracted complex: the map induced by the comparison c.comparison : J ⟶ TopRep.resolution' X on the cohomology of invariants.

theorem TopRep.ResolutionContraction.cohomologyMap_def {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (n : ℕ) : c.cohomologyMap n = HomologicalComplex.homologyMap (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).map c.comparison) n

The defining equation of cohomologyMap: it is the map on the cohomology of invariants induced by the comparison.

theorem TopRep.ResolutionContraction.d_mapInvariants_comparison_f {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) ((Hom.hom (c.comparison.f n)).mapInvariants z) = 0

The comparison carries an invariant cocycle of J to a homogeneous cocycle of X.

noncomputable def TopRep.ResolutionContraction.cohomologyClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : ↑(continuousCohomology n X).toModuleCat

The class in Hⁿ(G, X) of an invariant cocycle z of the contracted complex J: the class of the homogeneous cocycle into which the comparison carries z.

theorem TopRep.ResolutionContraction.cohomologyClass_def {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : c.cohomologyClass z hz = X.cochainClass n ((Hom.hom (c.comparison.f n)).mapInvariants z) ⋯

The defining equation of cohomologyClass.

@[simp]

theorem TopRep.ResolutionContraction.cohomologyMap_homologyπ {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : (CategoryTheory.ConcreteCategory.hom (c.cohomologyMap n)) ((CategoryTheory.ConcreteCategory.hom ((((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).obj J).homologyπ n)) ((((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).obj J).cyclesMkOfEq z (n + 1) ⋯ ⋯)) = c.cohomologyClass z hz

The class of an invariant cocycle is its image under the cohomology map: cohomologyMap sends the class of z in Hⁿ(Jᴳ) to c.cohomologyClass z.

@[simp]

theorem TopRep.ResolutionContraction.cohomologyClass_add {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z z' : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) (hz' : (Hom.hom (J.d n (n + 1))) ↑z' = 0) : c.cohomologyClass (z + z') ⋯ = c.cohomologyClass z hz + c.cohomologyClass z' hz'

The class of a sum of invariant cocycles is the sum of their classes.

@[simp]

theorem TopRep.ResolutionContraction.cohomologyClass_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} : c.cohomologyClass 0 ⋯ = 0

The class of the zero cocycle is zero.

@[simp]

theorem TopRep.ResolutionContraction.cohomologyClass_smul {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (r : k) (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : c.cohomologyClass (r • z) ⋯ = r • c.cohomologyClass z hz

The class of a scalar multiple of an invariant cocycle is the scalar multiple of its class.

theorem TopRep.ResolutionContraction.cohomologyClass_eq_of_sub_eq_d {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) {n : ℕ} (z z' : ↥(J.X (n + 1)).ρ.invariants) (hz : (Hom.hom (J.d (n + 1) (n + 2))) ↑z = 0) (hz' : (Hom.hom (J.d (n + 1) (n + 2))) ↑z' = 0) (y : ↥(J.X n).ρ.invariants) (hy : ↑z - ↑z' = (Hom.hom (J.d n (n + 1))) ↑y) : c.cohomologyClass z hz = c.cohomologyClass z' hz'

Cohomologous invariant cocycles have the same class: if z - z' is the differential of an invariant element of J, then z and z' have the same class in Hⁿ⁺¹(G, X).

theorem TopRep.ResolutionContraction.cohomologyClass_eq_degreeZeroClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) (z : ↥(J.X 0).ρ.invariants) (hz : (Hom.hom (J.d 0 (0 + 1))) ↑z = 0) : c.cohomologyClass z hz = TauCeti.ContinuousCohomology.degreeZeroClass X (c.proj ↑z) ⋯

The class of an invariant degree-zero cocycle is the degree-zero class of its retraction. In degree zero a cocycle z of the contracted complex is ι (proj z), so its class in H⁰(G, X) = X^G is the invariant vector proj z.

theorem TopRep.ResolutionContraction.cohomologyMap_eq_of_ι_eq {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] (c' : X.ResolutionContraction J) (h : c.ι = c'.ι) (n : ℕ) : c.cohomologyMap n = c'.cohomologyMap n

Independence of the contraction. Two contractions of J onto X with the same augmentation induce the same map on cohomology.

theorem TopRep.ResolutionContraction.cohomologyMap_comp_coeffMap {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] {Y : TopRep k G} {J' : CochainComplex (TopRep k G) ℕ} (c' : Y.ResolutionContraction J') (g : X ⟶ Y) (f : J ⟶ J') (hf : CategoryTheory.CategoryStruct.comp c.ι (f.f 0) = CategoryTheory.CategoryStruct.comp g c'.ι) (n : ℕ) : CategoryTheory.CategoryStruct.comp (c.cohomologyMap n) (TauCeti.ContinuousCohomology.coeffMap g n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).map f) n) (c'.cohomologyMap n)

Naturality of the cohomology map. For contractions c of J onto X and c' of J' onto Y, a coefficient morphism g : X ⟶ Y and a chain map f : J ⟶ J' lying over it give a commutative square: Hⁿ(Jᴳ) ⟶ Hⁿ(G, X) ⟶ Hⁿ(G, Y) equals Hⁿ(Jᴳ) ⟶ Hⁿ(J'ᴳ) ⟶ Hⁿ(G, Y).

theorem TopRep.ResolutionContraction.cohomologyMap_comp_coeffMap_assoc {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] {Y : TopRep k G} {J' : CochainComplex (TopRep k G) ℕ} (c' : Y.ResolutionContraction J') (g : X ⟶ Y) (f : J ⟶ J') (hf : CategoryTheory.CategoryStruct.comp c.ι (f.f 0) = CategoryTheory.CategoryStruct.comp g c'.ι) (n : ℕ) {Z : TopModuleCat k} (h : continuousCohomology n Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (c.cohomologyMap n) (CategoryTheory.CategoryStruct.comp (TauCeti.ContinuousCohomology.coeffMap g n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (((invariantsFunctor k G).mapHomologicalComplex (ComplexShape.up ℕ)).map f) n) (CategoryTheory.CategoryStruct.comp (c'.cohomologyMap n) h)

Naturality of the cohomology map. For contractions c of J onto X and c' of J' onto Y, a coefficient morphism g : X ⟶ Y and a chain map f : J ⟶ J' lying over it give a commutative square: Hⁿ(Jᴳ) ⟶ Hⁿ(G, X) ⟶ Hⁿ(G, Y) equals Hⁿ(Jᴳ) ⟶ Hⁿ(J'ᴳ) ⟶ Hⁿ(G, Y).

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

Naturality of the cohomology map in the complex. A chain map f : J ⟶ J' of complexes contracted onto the same X, lying over the identity of X, commutes with the cohomology maps.

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

Naturality of the cohomology map in the complex. A chain map f : J ⟶ J' of complexes contracted onto the same X, lying over the identity of X, commutes with the cohomology maps.

theorem TopRep.ResolutionContraction.cohomologyClass_eq_of_ι_eq {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] (c' : X.ResolutionContraction J) (h : c.ι = c'.ι) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : c.cohomologyClass z hz = c'.cohomologyClass z hz

Classes are independent of the contraction. Two contractions of J onto X with the same augmentation give every invariant cocycle the same class.

theorem TopRep.ResolutionContraction.cohomologyClass_map {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] {J' : CochainComplex (TopRep k G) ℕ} (c' : X.ResolutionContraction J') (f : J ⟶ J') (hf : CategoryTheory.CategoryStruct.comp c.ι (f.f 0) = c'.ι) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : c'.cohomologyClass ((Hom.hom (f.f n)).mapInvariants z) ⋯ = c.cohomologyClass z hz

A chain map over the identity preserves classes. If f : J ⟶ J' lies over the identity of X for contractions c of J and c' of J', then an invariant cocycle z of J and its image f z have the same class in Hⁿ(G, X).

theorem TopRep.ResolutionContraction.coeffMap_cohomologyClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] {Y : TopRep k G} {J' : CochainComplex (TopRep k G) ℕ} (c' : Y.ResolutionContraction J') (g : X ⟶ Y) (f : J ⟶ J') (hf : CategoryTheory.CategoryStruct.comp c.ι (f.f 0) = CategoryTheory.CategoryStruct.comp g c'.ι) {n : ℕ} (z : ↥(J.X n).ρ.invariants) (hz : (Hom.hom (J.d n (n + 1))) ↑z = 0) : (CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.coeffMap g n)) (c.cohomologyClass z hz) = c'.cohomologyClass ((Hom.hom (f.f n)).mapInvariants z) ⋯

Naturality of classes in the coefficients. For a chain map f : J ⟶ J' lying over a coefficient morphism g : X ⟶ Y, the coefficient map of g carries the class of an invariant cocycle z of J to the class of f z.

theorem TopRep.ResolutionContraction.cochainClass_eq_of_ι_comp_eq {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} {J : CochainComplex (TopRep k G) ℕ} (c : X.ResolutionContraction J) [LocallyCompactSpace G] {Z : TopRep k G} {n : ℕ} (φ ψ : (p : ℕ) → J.X p ⟶ Z.resolution'.X (p + n)) (hφ : ∀ (p : ℕ), CategoryTheory.CategoryStruct.comp (φ p) (Z.resolution'.d (p + n) (p + 1 + n)) = CategoryTheory.CategoryStruct.comp (J.d p (p + 1)) (φ (p + 1))) (hψ : ∀ (p : ℕ), CategoryTheory.CategoryStruct.comp (ψ p) (Z.resolution'.d (p + n) (p + 1 + n)) = CategoryTheory.CategoryStruct.comp (J.d p (p + 1)) (ψ (p + 1))) (h : CategoryTheory.CategoryStruct.comp c.ι (φ 0) = CategoryTheory.CategoryStruct.comp c.ι (ψ 0)) {p : ℕ} (a : ↥(J.X p).ρ.invariants) (ha : (Hom.hom (J.d p (p + 1))) ↑a = 0) : Z.cochainClass (p + n) ((Hom.hom (φ p)).mapInvariants a) ⋯ = Z.cochainClass (p + n) ((Hom.hom (ψ p)).mapInvariants a) ⋯

Uniqueness of comparisons of degree n. Let φ and ψ be families of equivariant maps Jᵖ ⟶ C^{p + n} into the coinduced resolution of Z, raising degrees by n and commuting with the differentials, that agree on the augmentation of a contraction c of J. Then they carry an invariant cocycle of J to cohomologous homogeneous cocycles of Z.

@[simp]

theorem TopRep.cohomologyMap_resolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) (n : ℕ) : X.resolutionContraction.cohomologyMap n = CategoryTheory.CategoryStruct.id (continuousCohomology n X)

For the coinduced resolution contracted by evaluation at 1, the cohomology map is the identity of Hⁿ(G, X).

@[simp]

theorem TopRep.cohomologyClass_resolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] (X : TopRep k G) {n : ℕ} (z : ↥(X.resolution'.X n).ρ.invariants) (hz : (Hom.hom (X.resolution'.d n (n + 1))) ↑z = 0) : X.resolutionContraction.cohomologyClass z hz = X.cochainClass n z ⋯

For the coinduced resolution contracted by evaluation at 1, the class of an invariant cocycle is its class in continuous cohomology.