Contractions of graded representations and classes of homogeneous cocycles

Let M be a topological representation of G with a ℤ-grading ℳ by invariant submodules and an equivariant differential d of degree one, and let TopRep.gradedCochainComplex be the cochain complex of TopRep k G they assemble. A contraction of M onto X given on the total module, that is, an equivariant augmentation ι : X ⟶ M into degree zero, a retraction π : M → X vanishing in positive degrees and a homotopy h of degree -1 vanishing in degree zero with

π ∘ ι = 1,        d ∘ h + h ∘ d = 1 - ι ∘ π,

where neither π nor h need be equivariant, restricts degree by degree to a TopRep.ResolutionContraction of that complex onto X (TopRep.ResolutionContraction.ofGraded). Through the comparison with the coinduced resolution, a cocycle z ∈ ℳ n of M fixed by G then has a class in Hⁿ(G, X) (TopRep.ResolutionContraction.gradedCohomologyClass).

This is how cocycles written on a total module reach continuous cohomology. Tensor constructions produce their differentials and contractions on a single carrier, and in Evens' multiplicative transfer the norm of a class is the class of the tensor power of a representing cocycle, an invariant cocycle of the tensor-induced total resolution.

The total shifted coinduced resolution X.gradedResolutionTopRep, with its evaluation-at-1 contraction, is the first instance (TopRep.gradedResolutionContraction), and there the class of a homogeneous cocycle is its class in continuous cohomology (TopRep.gradedCohomologyClass_gradedResolutionContraction).

Main definitions

• TopRep.ResolutionContraction.ofGraded: the contraction of TopRep.gradedCochainComplex obtained from a contraction of the total module.
• TopRep.ResolutionContraction.gradedCohomologyClass: the class in Hⁿ(G, X) of an invariant cocycle of M homogeneous of degree n.
• TopRep.gradedResolutionContraction: the contraction of the complex of the total coinduced resolution by evaluation at 1.

Main results

• TopRep.ResolutionContraction.ofGraded_ι, TopRep.ResolutionContraction.ofGraded_proj_apply, TopRep.ResolutionContraction.ofGraded_hom_apply: the data of ofGraded are ι, π and h.
• TopRep.ResolutionContraction.gradedCohomologyClass_add, gradedCohomologyClass_zero and gradedCohomologyClass_smul: the class is linear in the cocycle.
• TopRep.ResolutionContraction.gradedCohomologyClass_eq_of_sub_eq_d: homogeneous cocycles differing by the differential of a homogeneous invariant element have the same class.
• TopRep.ResolutionContraction.gradedCohomologyClass_map: a morphism of degree zero commuting with the differentials and carrying one augmentation to the other preserves classes.
• TopRep.ResolutionContraction.gradedCohomologyClass_eq_degreeZeroClass: in degree zero, the class of a cocycle is the invariant vector given by its retraction.
• TopRep.ResolutionContraction.gradedCohomologyClass_eq_of_ι_eq: over a locally compact group, the class depends on the contraction only through its augmentation.
• TopRep.ResolutionContraction.gradedCohomologyClass_degreeCast and TopRep.ResolutionContraction.coeffMap_gradedCohomologyClass_degreeCast: equal cocycles read in equal degrees have classes related by degreeCast.
• TopRep.gradedCohomologyClass_gradedResolutionContraction: on the total coinduced resolution, the class of a homogeneous cocycle is its class in continuous cohomology.
• TopRep.gradedCohomologyClass_eq_degreeCast_cochainClass: the same, for a cocycle included by cochainToGradedResolution and read in a degree equal to its own, through degreeCast.

References

• L. Evens, A generalization of the transfer map in the cohomology of groups, Trans. Amer. Math. Soc. 108 (1963), §§2–5.

noncomputable def TopRep.ResolutionContraction.ofGraded {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} (X : TopRep k G) (ι : X ⟶ M) (hι : ∀ (x : ↑X), (Hom.hom ι) x ∈ ℳ 0) (π : ↑M →ₗ[k] ↑X) (h : ↑M →ₗ[k] ↑M) (hh : TauCeti.LinearMap.IsHomogeneous h ℳ ℳ (-1)) (hπι : ∀ (x : ↑X), π ((Hom.hom ι) x) = x) (hπ : ∀ (n : ℕ), ∀ v ∈ ℳ ↑(n + 1), π v = 0) (hh₀ : ∀ v ∈ ℳ 0, h v = 0) (hdh : ∀ (v : ↑M), (Hom.hom d) (h v) + h ((Hom.hom d) v) = v - (Hom.hom ι) (π v)) (hπc : Continuous fun (p : ↑M × G) => (X.ρ p.2) (π ((M.ρ p.2⁻¹) p.1))) (hhc : Continuous fun (p : ↑M × G) => (M.ρ p.2) (h ((M.ρ p.2⁻¹) p.1))) : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)

The contraction of a graded representation: a contraction of the total module M onto X restricts to a contraction of the complex TopRep.gradedCochainComplex onto X. The data are an equivariant augmentation ι into degree zero, a retraction π vanishing in positive degrees and a homotopy h of degree -1 vanishing in degree zero, with π ∘ ι = 1 and d ∘ h + h ∘ d = 1 - ι ∘ π; the conjugates of π and h must be jointly continuous, which holds automatically between smooth discrete representations (TauCeti.IsSmoothDiscrete.continuous_conj).

@[simp]

theorem TopRep.ResolutionContraction.ofGraded_ι {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} (X : TopRep k G) (ι : X ⟶ M) (hι : ∀ (x : ↑X), (Hom.hom ι) x ∈ ℳ 0) (π : ↑M →ₗ[k] ↑X) (h : ↑M →ₗ[k] ↑M) (hh : TauCeti.LinearMap.IsHomogeneous h ℳ ℳ (-1)) (hπι : ∀ (x : ↑X), π ((Hom.hom ι) x) = x) (hπ : ∀ (n : ℕ), ∀ v ∈ ℳ ↑(n + 1), π v = 0) (hh₀ : ∀ v ∈ ℳ 0, h v = 0) (hdh : ∀ (v : ↑M), (Hom.hom d) (h v) + h ((Hom.hom d) v) = v - (Hom.hom ι) (π v)) (hπc : Continuous fun (p : ↑M × G) => (X.ρ p.2) (π ((M.ρ p.2⁻¹) p.1))) (hhc : Continuous fun (p : ↑M × G) => (M.ρ p.2) (h ((M.ρ p.2⁻¹) p.1))) : (ofGraded X ι hι π h hh hπι hπ hh₀ hdh hπc hhc).ι = M.gradedCochainComplexLift ℳ hρ d hd hdd 0 ι hι

The augmentation of ofGraded is the factorization of ι through the degree-zero term.

@[simp]

theorem TopRep.ResolutionContraction.ofGraded_proj_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} (X : TopRep k G) (ι : X ⟶ M) (hι : ∀ (x : ↑X), (Hom.hom ι) x ∈ ℳ 0) (π : ↑M →ₗ[k] ↑X) (h : ↑M →ₗ[k] ↑M) (hh : TauCeti.LinearMap.IsHomogeneous h ℳ ℳ (-1)) (hπι : ∀ (x : ↑X), π ((Hom.hom ι) x) = x) (hπ : ∀ (n : ℕ), ∀ v ∈ ℳ ↑(n + 1), π v = 0) (hh₀ : ∀ v ∈ ℳ 0, h v = 0) (hdh : ∀ (v : ↑M), (Hom.hom d) (h v) + h ((Hom.hom d) v) = v - (Hom.hom ι) (π v)) (hπc : Continuous fun (p : ↑M × G) => (X.ρ p.2) (π ((M.ρ p.2⁻¹) p.1))) (hhc : Continuous fun (p : ↑M × G) => (M.ρ p.2) (h ((M.ρ p.2⁻¹) p.1))) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X 0)) : (ofGraded X ι hι π h hh hπι hπ hh₀ hdh hπc hhc).proj v = π ↑v

The retraction of ofGraded is π on the degree-zero term.

@[simp]

theorem TopRep.ResolutionContraction.ofGraded_hom_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} (X : TopRep k G) (ι : X ⟶ M) (hι : ∀ (x : ↑X), (Hom.hom ι) x ∈ ℳ 0) (π : ↑M →ₗ[k] ↑X) (h : ↑M →ₗ[k] ↑M) (hh : TauCeti.LinearMap.IsHomogeneous h ℳ ℳ (-1)) (hπι : ∀ (x : ↑X), π ((Hom.hom ι) x) = x) (hπ : ∀ (n : ℕ), ∀ v ∈ ℳ ↑(n + 1), π v = 0) (hh₀ : ∀ v ∈ ℳ 0, h v = 0) (hdh : ∀ (v : ↑M), (Hom.hom d) (h v) + h ((Hom.hom d) v) = v - (Hom.hom ι) (π v)) (hπc : Continuous fun (p : ↑M × G) => (X.ρ p.2) (π ((M.ρ p.2⁻¹) p.1))) (hhc : Continuous fun (p : ↑M × G) => (M.ρ p.2) (h ((M.ρ p.2⁻¹) p.1))) (n : ℕ) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X (n + 1))) : ↑(((ofGraded X ι hι π h hh hπι hπ hh₀ hdh hπc hhc).hom n) v) = h ↑v

The contracting homotopy of ofGraded is h on each term.

noncomputable def TopRep.ResolutionContraction.gradedCohomologyClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} (z : ↑M) (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : ↑(continuousCohomology n X).toModuleCat

The class of a homogeneous cocycle: a vector z ∈ ℳ n of M fixed by G and killed by d is an invariant cocycle of TopRep.gradedCochainComplex, and this is its class in Hⁿ(G, X) through the contraction c.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_def {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} (z : ↑M) (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : c.gradedCohomologyClass z hz hinv hdz = c.cohomologyClass (M.gradedCochainComplexInvariant ℳ hρ d hd hdd n z hz hinv) ⋯

The defining equation of gradedCohomologyClass: it is the class cohomologyClass of the invariant cocycle given by z.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_eq_of_sub_eq_d {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} {z z' : ↑M} (hz : z ∈ ℳ ↑(n + 1)) (hz' : z' ∈ ℳ ↑(n + 1)) (hinv : ∀ (g : G), (M.ρ g) z = z) (hinv' : ∀ (g : G), (M.ρ g) z' = z') (hdz : (Hom.hom d) z = 0) (hdz' : (Hom.hom d) z' = 0) {y : ↑M} (hy : y ∈ ℳ ↑n) (hyinv : ∀ (g : G), (M.ρ g) y = y) (hzy : z - z' = (Hom.hom d) y) : c.gradedCohomologyClass z hz hinv hdz = c.gradedCohomologyClass z' hz' hinv' hdz'

Cohomologous homogeneous cocycles have the same class: if z - z' is the differential of a vector y ∈ ℳ n fixed by G, then z and z' have the same class in Hⁿ⁺¹(G, X).

theorem TopRep.ResolutionContraction.gradedCohomologyClass_map {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [LocallyCompactSpace G] {M' : TopRep k G} {ℳ' : ℤ → Submodule k ↑M'} {hρ' : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ' n, (M'.ρ g) x ∈ ℳ' n} {d' : M' ⟶ M'} {hd' : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d').toContinuousLinearMap) ℳ' ℳ' 1} {hdd' : CategoryTheory.CategoryStruct.comp d' d' = 0} (c' : X.ResolutionContraction (M'.gradedCochainComplex ℳ' hρ' d' hd' hdd')) (F : M ⟶ M') (hF : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom F).toContinuousLinearMap) ℳ ℳ' 0) (hFd : CategoryTheory.CategoryStruct.comp d F = CategoryTheory.CategoryStruct.comp F d') (hι : ∀ (x : ↑X), (Hom.hom F) ↑((Hom.hom c.ι) x) = ↑((Hom.hom c'.ι) x)) {n : ℕ} {z : ↑M} (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : c'.gradedCohomologyClass ((Hom.hom F) z) ⋯ ⋯ ⋯ = c.gradedCohomologyClass z hz hinv hdz

A chain map over the identity preserves classes. Let F : M ⟶ M' be a morphism of degree zero commuting with the differentials, between graded representations whose complexes are contracted onto the same X by c and c', and suppose F carries the augmentation of c to that of c'. Then a homogeneous cocycle z of M fixed by G and its image F z have the same class in Hⁿ(G, X).

@[simp]

theorem TopRep.ResolutionContraction.gradedCohomologyClass_add {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} {z z' : ↑M} (hz : z ∈ ℳ ↑n) (hz' : z' ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hinv' : ∀ (g : G), (M.ρ g) z' = z') (hdz : (Hom.hom d) z = 0) (hdz' : (Hom.hom d) z' = 0) : c.gradedCohomologyClass (z + z') ⋯ ⋯ ⋯ = c.gradedCohomologyClass z hz hinv hdz + c.gradedCohomologyClass z' hz' hinv' hdz'

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

@[simp]

theorem TopRep.ResolutionContraction.gradedCohomologyClass_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} : c.gradedCohomologyClass 0 ⋯ ⋯ ⋯ = 0

The class of the zero cocycle is zero.

@[simp]

theorem TopRep.ResolutionContraction.gradedCohomologyClass_smul {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n : ℕ} (r : k) {z : ↑M} (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : c.gradedCohomologyClass (r • z) ⋯ ⋯ ⋯ = r • c.gradedCohomologyClass z hz hinv hdz

The class of a scalar multiple of a homogeneous cocycle is the scalar multiple of its class.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_eq_degreeZeroClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) (z : ↑M) (hz : z ∈ ℳ ↑0) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : c.gradedCohomologyClass z hz hinv hdz = TauCeti.ContinuousCohomology.degreeZeroClass X (c.proj ↑(M.gradedCochainComplexInvariant ℳ hρ d hd hdd 0 z hz hinv)) ⋯

The class of a degree-zero cocycle is the degree-zero class of its retraction: a vector z ∈ ℳ 0 fixed by G and killed by d has class proj z in H⁰(G, X) = X^G.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_eq_of_ι_eq {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [LocallyCompactSpace G] (c' : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) (h : c.ι = c'.ι) {n : ℕ} (z : ↑M) (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : c.gradedCohomologyClass z hz hinv hdz = c'.gradedCohomologyClass z hz hinv hdz

Independence of the contraction. Over a locally compact group, two contractions of the complex of a graded representation with the same augmentation give a homogeneous cocycle the same class.

theorem TopRep.ResolutionContraction.coeffMap_gradedCohomologyClass_degreeCast {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {Y : TopRep k G} (b : X ⟶ Y) {n n' : ℕ} (h : n = n') {z z' : ↑M} (hzz : z' = z) (hz : z ∈ ℳ ↑n) (hz' : z' ∈ ℳ ↑n') (hinv : ∀ (g : G), (M.ρ g) z = z) (hinv' : ∀ (g : G), (M.ρ g) z' = z') (hdz : (Hom.hom d) z = 0) (hdz' : (Hom.hom d) z' = 0) : (CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.coeffMap b n')) (c.gradedCohomologyClass z' hz' hinv' hdz') = (CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.degreeCast Y h).hom) ((CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.coeffMap b n)) (c.gradedCohomologyClass z hz hinv hdz))

Transport along an equality of degrees. Equal homogeneous cocycles z' = z, read in equal degrees n = n', have classes that agree after transporting the degree with degreeCast, also after a coefficient map b.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_degreeCast {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] {M : TopRep k G} {ℳ : ℤ → Submodule k ↑M} {hρ : ∀ (n : ℤ) (g : G), ∀ x ∈ ℳ n, (M.ρ g) x ∈ ℳ n} {d : M ⟶ M} {hd : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom d).toContinuousLinearMap) ℳ ℳ 1} {hdd : CategoryTheory.CategoryStruct.comp d d = 0} [IsTopologicalGroup G] {X : TopRep k G} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) {n n' : ℕ} (h : n = n') {z z' : ↑M} (hzz : z' = z) (hz : z ∈ ℳ ↑n) (hz' : z' ∈ ℳ ↑n') (hinv : ∀ (g : G), (M.ρ g) z = z) (hinv' : ∀ (g : G), (M.ρ g) z' = z') (hdz : (Hom.hom d) z = 0) (hdz' : (Hom.hom d) z' = 0) : c.gradedCohomologyClass z' hz' hinv' hdz' = (CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.degreeCast X h).hom) (c.gradedCohomologyClass z hz hinv hdz)

Transport along an equality of degrees. Equal homogeneous cocycles z' = z, read in equal degrees n = n', have classes that agree after transporting the degree with degreeCast.

@[reducible, inline]

noncomputable abbrev TopRep.gradedResolutionCochainComplex {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] (X : TopRep k G) : CochainComplex (TopRep k G) ℕ

The cochain complex TopRep.gradedCochainComplex of the total shifted coinduced resolution, whose degree-n term is the copy of C(G, …, C(G, X)) with n + 1 layers.

noncomputable def TopRep.gradedResolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) : X.ResolutionContraction X.gradedResolutionCochainComplex

The contraction of the total coinduced resolution onto smooth discrete coefficients, by the evaluation-at-1 maps gradedResolutionProjection and gradedResolutionHomotopy.

@[simp]

theorem TopRep.gradedResolutionContraction_ι_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) (x : ↑X) : ↑((Hom.hom (gradedResolutionContraction hX).ι) x) = X.gradedResolutionAugmentation x

The augmentation of gradedResolutionContraction is the augmentation of the total resolution.

@[simp]

theorem TopRep.gradedResolutionContraction_proj_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) (v : ↑(X.gradedResolutionCochainComplex.X 0)) : (gradedResolutionContraction hX).proj v = X.gradedResolutionProjection ↑v

The retraction of gradedResolutionContraction is gradedResolutionProjection.

@[simp]

theorem TopRep.gradedResolutionContraction_hom_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) (n : ℕ) (v : ↑(X.gradedResolutionCochainComplex.X (n + 1))) : ↑(((gradedResolutionContraction hX).hom n) v) = X.gradedResolutionHomotopy ↑v

The contracting homotopy of gradedResolutionContraction is gradedResolutionHomotopy.

theorem TopRep.gradedCohomologyClass_gradedResolutionContraction {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) {n : ℕ} (z : ↥(X.resolution'.X n).ρ.invariants) (hz : (Hom.hom (X.resolution'.d n (n + 1))) ↑z = 0) : (gradedResolutionContraction hX).gradedCohomologyClass ((DirectSum.lof k ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) ↑z) ⋯ ⋯ ⋯ = X.cochainClass n z ⋯

On the total coinduced resolution, the class of a homogeneous cocycle is its class in continuous cohomology: a homogeneous cocycle z of degree n, included into the total resolution, has as class through gradedResolutionContraction the class X.cochainClass n z.

theorem TopRep.gradedCohomologyClass_eq_degreeCast_cochainClass {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [DiscreteTopology k] [IsTopologicalGroup G] {X : TopRep k G} [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) {n k✝ : ℕ} (hk : n = k✝) (z : ↑(X.homogeneousCochains.X n).toModuleCat) (hz : (TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) z = 0) (y : ↑X.gradedResolutionTopRep) (hy : y = (X.cochainToGradedResolution n) z) (hy' : y ∈ X.gradedResolutionPiece ↑k✝) (hinv : ∀ (g : G), (X.gradedResolutionTopRep.ρ g) y = y) (hdy : (Hom.hom X.gradedResolutionTopRepDifferential) y = 0) : (gradedResolutionContraction hX).gradedCohomologyClass y hy' hinv hdy = (CategoryTheory.ConcreteCategory.hom (TauCeti.ContinuousCohomology.degreeCast X hk).hom) (X.cochainClass n z hz)

The class of an included homogeneous cocycle, in an equal degree: a vector y of the total coinduced resolution that is the inclusion of a homogeneous cocycle z of degree n, regarded as homogeneous of an equal degree k, has as class through gradedResolutionContraction the transport along n = k of X.cochainClass n z. This reads off classes of cocycles produced in a degree, such as 1 · n, that equals n but not definitionally.