Homogeneous cochains in the total coinduced resolution

The homogeneous cochains are invariant elements of individual resolution terms. Their linear inclusions into the total resolution retain their degree and invariance and commute with the differential. This lets constructions on the total resolution, such as diagonal tensor powers, accept canonical cochains and coboundaries directly.

noncomputable def TopRep.cochainToGradedResolution {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) : ↑(X.homogeneousCochains.X n).toModuleCat →ₗ[R] X.gradedResolutionModule

Include a canonical homogeneous cochain into its degree of the total coinduced resolution.

theorem TopRep.cochainToGradedResolution_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) (z : ↑(X.homogeneousCochains.X n).toModuleCat) : (X.cochainToGradedResolution n) z = (DirectSum.lof R ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) ↑z

The inclusion of a cochain is its underlying resolution element in the indicated summand.

@[simp]

theorem TopRep.cochainToGradedResolution_mem {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) (z : ↑(X.homogeneousCochains.X n).toModuleCat) : (X.cochainToGradedResolution n) z ∈ X.gradedResolutionPiece ↑n

The included cochain is homogeneous of its original degree.

@[simp]

theorem TopRep.cochainToGradedResolution_invariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology R] (n : ℕ) (z : ↑(X.homogeneousCochains.X n).toModuleCat) (g : G) : (X.gradedResolutionTopRep.ρ g) ((X.cochainToGradedResolution n) z) = (X.cochainToGradedResolution n) z

The included cochain is invariant under the group action on the total resolution.

@[simp]

theorem TopRep.gradedResolutionDifferential_cochainToGradedResolution {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) (n : ℕ) (z : ↑(X.homogeneousCochains.X n).toModuleCat) : X.gradedResolutionDifferential ((X.cochainToGradedResolution n) z) = (X.cochainToGradedResolution (n + 1)) ((TopModuleCat.Hom.hom (X.homogeneousCochains.d n (n + 1))) z)

Inclusion of homogeneous cochains commutes with the differential.