The cochain complex of a graded topological representation

Let M be a topological representation of G whose underlying module carries a ℤ-indexed family ℳ of submodules, each stable under the action, and let d : M ⟶ M be an equivariant endomorphism of degree one with d ≫ d = 0. Then the subrepresentations on the pieces ℳ n for n : ℕ, with the restrictions of d, form a cochain complex of topological representations. This file performs that assembly.

Constructions such as tensor products and tensor induction are easier to write on a single carrier than on a family of summands: the total module of a resolution carries one action and one differential, and a tensor product of such modules again does. Continuous cohomology, on the other hand, is computed from complexes in TopRep k G indexed by ℕ (TopRep.resolution'), and the comparison of TopRep.ResolutionContraction takes such a complex as input. This construction passes from the first description to the second. No decomposition hypothesis on ℳ is needed, and the pieces in negative degrees are ignored.

This is the counterpart for topological representations of TauCeti.gradedCochainComplex, which assembles a ℤ-indexed complex of modules from the same kind of data.

Main definitions

• TopRep.gradedCochainComplex: the cochain complex whose degree-n term is the subrepresentation on ℳ n and whose differential is the restriction of d.
• TopRep.gradedCochainComplexι: the inclusion of each term into M.
• TopRep.gradedCochainComplexRestrict: the linear maps between terms induced by a homogeneous linear endomorphism of M.
• TopRep.gradedCochainComplexInvariant: a fixed homogeneous vector of M as an invariant element of a term.
• TopRep.gradedCochainComplexLift: the factorization through a term of a morphism into M with values in one piece of the grading.
• TopRep.gradedCochainComplexMap: the chain map induced by a morphism of degree zero commuting with the differentials.
• TopRep.gradedCochainComplexIso: an isomorphism preserving and detecting degrees induces an isomorphism of complexes when it commutes with the differentials.
• TopRep.gradedCochainComplexResMap: the chain map from the restricted complex of a graded representation induced by a morphism of degree zero.

Main results

• TopRep.gradedCochainComplex_d_comp_ι: the inclusions intertwine the differential of the complex with d.
• TopRep.gradedCochainComplex_d_apply: the same statement on an element.
• TopRep.gradedCochainComplexLift_comp_ι, TopRep.gradedCochainComplexLift_unique: the factorization through a term is characterized by its composite with the inclusion.
• TopRep.gradedCochainComplex_d_invariant: a fixed homogeneous vector killed by d is an invariant cocycle of the complex.

noncomputable def TopRep.gradedCochainComplex {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) : CochainComplex (TopRep k G) ℕ

The cochain complex of a graded topological representation: its degree-n term is the subrepresentation on the piece ℳ n, with the induced topology, and its differential is the restriction of the degree-one endomorphism d, which squares to zero.

theorem TopRep.gradedCochainComplex_X {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) : (M.gradedCochainComplex ℳ hρ d hd hdd).X n = M.subrepresentation (ℳ ↑n) ⋯

The degree-n term of gradedCochainComplex is the subrepresentation on ℳ n.

@[simp]

theorem TopRep.gradedCochainComplex_ρ_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) (g : G) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : ↑((((M.gradedCochainComplex ℳ hρ d hd hdd).X n).ρ g) v) = (M.ρ g) ↑v

The action on a term of gradedCochainComplex is the action of M.

theorem TopRep.continuous_gradedCochainComplex_X_iff {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Z : Type u_1} [TopologicalSpace Z] (n : ℕ) (f : Z → ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : Continuous f ↔ Continuous fun (z : Z) => ↑(f z)

A map into a term of gradedCochainComplex is continuous exactly when it is continuous as a map into M, since the term carries the topology induced from M.

noncomputable def TopRep.gradedCochainComplexLift {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Y : TopRep k G} (n : ℕ) (f : Y ⟶ M) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ ℳ ↑n) : Y ⟶ (M.gradedCochainComplex ℳ hρ d hd hdd).X n

A morphism into M with values in ℳ n factors through the degree-n term of gradedCochainComplex.

@[simp]

theorem TopRep.gradedCochainComplexLift_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Y : TopRep k G} (n : ℕ) (f : Y ⟶ M) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ ℳ ↑n) (y : ↑Y) : ↑((Hom.hom (M.gradedCochainComplexLift ℳ hρ d hd hdd n f hf)) y) = (Hom.hom f) y

The factorization through a term of gradedCochainComplex evaluates by the original morphism.

noncomputable def TopRep.gradedCochainComplexRestrict {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (f : ↑M →ₗ[k] ↑M) {q : ℤ} (hf : TauCeti.LinearMap.IsHomogeneous f ℳ ℳ q) {m n : ℕ} (hmn : ↑m + q = ↑n) : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X m) →ₗ[k] ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)

A linear endomorphism f of M of degree q restricts to a linear map from the degree-m term of gradedCochainComplex to the degree-n term whenever m + q = n. Such maps need not be equivariant: the contracting homotopies of TopRep.ResolutionContraction are of this form.

@[simp]

theorem TopRep.gradedCochainComplexRestrict_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (f : ↑M →ₗ[k] ↑M) {q : ℤ} (hf : TauCeti.LinearMap.IsHomogeneous f ℳ ℳ q) {m n : ℕ} (hmn : ↑m + q = ↑n) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X m)) : ↑((M.gradedCochainComplexRestrict ℳ hρ d hd hdd f hf hmn) v) = f ↑v

The restriction of a homogeneous linear endomorphism to the terms of gradedCochainComplex evaluates by the endomorphism.

noncomputable def TopRep.gradedCochainComplexι {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) : (M.gradedCochainComplex ℳ hρ d hd hdd).X n ⟶ M

The inclusion of the degree-n term of gradedCochainComplex into the graded representation.

@[simp]

theorem TopRep.gradedCochainComplexι_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : (Hom.hom (M.gradedCochainComplexι ℳ hρ d hd hdd n)) v = ↑v

The inclusion of a term of gradedCochainComplex is the inclusion of the submodule.

theorem TopRep.gradedCochainComplexι_injective {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) : Function.Injective ⇑(Hom.hom (M.gradedCochainComplexι ℳ hρ d hd hdd n))

The inclusions of the terms of gradedCochainComplex are injective.

@[simp]

theorem TopRep.gradedCochainComplexLift_comp_ι {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Y : TopRep k G} (n : ℕ) (f : Y ⟶ M) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ ℳ ↑n) : CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexLift ℳ hρ d hd hdd n f hf) (M.gradedCochainComplexι ℳ hρ d hd hdd n) = f

The factorization through a term of gradedCochainComplex, followed by the inclusion, is the original morphism.

@[simp]

theorem TopRep.gradedCochainComplexLift_comp_ι_assoc {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Y : TopRep k G} (n : ℕ) (f : Y ⟶ M) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ ℳ ↑n) {Z : TopRep k G} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexLift ℳ hρ d hd hdd n f hf) (CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexι ℳ hρ d hd hdd n) h) = CategoryTheory.CategoryStruct.comp f h

The factorization through a term of gradedCochainComplex, followed by the inclusion, is the original morphism.

theorem TopRep.gradedCochainComplexLift_unique {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {Y : TopRep k G} (n : ℕ) (f : Y ⟶ M) (hf : ∀ (y : ↑Y), (Hom.hom f) y ∈ ℳ ↑n) (g : Y ⟶ (M.gradedCochainComplex ℳ hρ d hd hdd).X n) (hg : CategoryTheory.CategoryStruct.comp g (M.gradedCochainComplexι ℳ hρ d hd hdd n) = f) : g = M.gradedCochainComplexLift ℳ hρ d hd hdd n f hf

A morphism into a term of gradedCochainComplex is the factorization of its composite with the inclusion.

theorem TopRep.gradedCochainComplex_d_comp_ι {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((M.gradedCochainComplex ℳ hρ d hd hdd).d n (n + 1)) (M.gradedCochainComplexι ℳ hρ d hd hdd (n + 1)) = CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexι ℳ hρ d hd hdd n) d

The inclusions intertwine the differentials: the differential of gradedCochainComplex followed by the inclusion is the inclusion followed by d.

theorem TopRep.gradedCochainComplex_d_comp_ι_assoc {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) {Z : TopRep k G} (h : M ⟶ Z) : CategoryTheory.CategoryStruct.comp ((M.gradedCochainComplex ℳ hρ d hd hdd).d n (n + 1)) (CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexι ℳ hρ d hd hdd (n + 1)) h) = CategoryTheory.CategoryStruct.comp (M.gradedCochainComplexι ℳ hρ d hd hdd n) (CategoryTheory.CategoryStruct.comp d h)

The inclusions intertwine the differentials: the differential of gradedCochainComplex followed by the inclusion is the inclusion followed by d.

@[simp]

theorem TopRep.gradedCochainComplex_d_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : ↑((Hom.hom ((M.gradedCochainComplex ℳ hρ d hd hdd).d n (n + 1))) v) = (Hom.hom d) ↑v

The differential of gradedCochainComplex on an element is d applied to it in M.

def TopRep.gradedCochainComplexInvariant {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) (z : ↑M) (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) : ↥((M.gradedCochainComplex ℳ hρ d hd hdd).X n).ρ.invariants

A vector of ℳ n fixed by G is an invariant element of the degree-n term of gradedCochainComplex.

@[simp]

theorem TopRep.gradedCochainComplexInvariant_val {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) (n : ℕ) (z : ↑M) (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) : ↑↑(M.gradedCochainComplexInvariant ℳ hρ d hd hdd n z hz hinv) = z

The invariant element of a term of gradedCochainComplex given by a fixed vector of ℳ n is that vector.

theorem TopRep.gradedCochainComplex_d_invariant {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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) {n : ℕ} {z : ↑M} (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : (Hom.hom ((M.gradedCochainComplex ℳ hρ d hd hdd).d n (n + 1))) ↑(M.gradedCochainComplexInvariant ℳ hρ d hd hdd n z hz hinv) = 0

A fixed vector of ℳ n killed by d is a cocycle of gradedCochainComplex.

noncomputable def TopRep.gradedCochainComplexMap {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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} {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} (F : M ⟶ M') (hF : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom F).toContinuousLinearMap) ℳ ℳ' 0) (hFd : CategoryTheory.CategoryStruct.comp d F = CategoryTheory.CategoryStruct.comp F d') : M.gradedCochainComplex ℳ hρ d hd hdd ⟶ M'.gradedCochainComplex ℳ' hρ' d' hd' hdd'

A morphism F : M ⟶ M' of graded topological representations, of degree zero and commuting with the differentials, restricts degree by degree to a chain map between their cochain complexes. This is the counterpart of TauCeti.gradedCochainComplexMap for topological representations.

@[simp]

theorem TopRep.gradedCochainComplexMap_f_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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} {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} (F : M ⟶ M') (hF : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom F).toContinuousLinearMap) ℳ ℳ' 0) (hFd : CategoryTheory.CategoryStruct.comp d F = CategoryTheory.CategoryStruct.comp F d') (n : ℕ) (v : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : ↑((Hom.hom ((gradedCochainComplexMap F hF hFd).f n)) v) = (Hom.hom F) ↑v

The chain map gradedCochainComplexMap F evaluates by F.

noncomputable def TopRep.gradedCochainComplexIso {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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} {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} (F : M ≅ M') (hF : ∀ (n : ℤ) (x : ↑M), (Hom.hom F.hom) x ∈ ℳ' n ↔ x ∈ ℳ n) (hFd : CategoryTheory.CategoryStruct.comp d F.hom = CategoryTheory.CategoryStruct.comp F.hom d') : M.gradedCochainComplex ℳ hρ d hd hdd ≅ M'.gradedCochainComplex ℳ' hρ' d' hd' hdd'

An isomorphism preserving and detecting degrees and commuting with the differentials induces an isomorphism of the associated cochain complexes.

@[simp]

theorem TopRep.gradedCochainComplexIso_hom_f_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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} {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} (F : M ≅ M') (hF : ∀ (n : ℤ) (x : ↑M), (Hom.hom F.hom) x ∈ ℳ' n ↔ x ∈ ℳ n) (hFd : CategoryTheory.CategoryStruct.comp d F.hom = CategoryTheory.CategoryStruct.comp F.hom d') (n : ℕ) (x : ↑((M.gradedCochainComplex ℳ hρ d hd hdd).X n)) : ↑((Hom.hom ((gradedCochainComplexIso F hF hFd).hom.f n)) x) = (Hom.hom F.hom) ↑x

The induced complex isomorphism applies the original isomorphism in each degree.

@[simp]

theorem TopRep.gradedCochainComplexIso_inv_f_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Monoid 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} {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} (F : M ≅ M') (hF : ∀ (n : ℤ) (x : ↑M), (Hom.hom F.hom) x ∈ ℳ' n ↔ x ∈ ℳ n) (hFd : CategoryTheory.CategoryStruct.comp d F.hom = CategoryTheory.CategoryStruct.comp F.hom d') (n : ℕ) (x : ↑((M'.gradedCochainComplex ℳ' hρ' d' hd' hdd').X n)) : ↑((Hom.hom ((gradedCochainComplexIso F hF hFd).inv.f n)) x) = (Hom.hom F.inv) ↑x

The inverse complex isomorphism applies the inverse original isomorphism in each degree.

noncomputable def TopRep.gradedCochainComplexResMap {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} {H : Type u_3} [Group G] [Monoid H] {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} {M' : TopRep k H} {ℳ' : ℤ → Submodule k ↑M'} {hρ' : ∀ (n : ℤ) (g : H), ∀ 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} (φ : H →* G) (F : res φ M ⟶ M') (hF : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom F).toContinuousLinearMap) ℳ ℳ' 0) (hFd : CategoryTheory.CategoryStruct.comp ((resFunctor φ).map d) F = CategoryTheory.CategoryStruct.comp F d') : ((resFunctor φ).mapHomologicalComplex (ComplexShape.up ℕ)).obj (M.gradedCochainComplex ℳ hρ d hd hdd) ⟶ M'.gradedCochainComplex ℳ' hρ' d' hd' hdd'

A morphism F : res φ M ⟶ M' of degree zero commuting with the differentials, from the restriction of a graded G-representation along φ : H →* G to a graded H-representation, restricts degree by degree to a chain map from the restriction of the complex of M to the complex of M'. It is TopRep.gradedCochainComplexMap F on the complex of res φ M, whose terms are those of the restricted complex.

theorem TopRep.gradedCochainComplexResMap_f_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} {H : Type u_3} [Group G] [Monoid H] {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} {M' : TopRep k H} {ℳ' : ℤ → Submodule k ↑M'} {hρ' : ∀ (n : ℤ) (g : H), ∀ 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} (φ : H →* G) (F : res φ M ⟶ M') (hF : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom F).toContinuousLinearMap) ℳ ℳ' 0) (hFd : CategoryTheory.CategoryStruct.comp ((resFunctor φ).map d) F = CategoryTheory.CategoryStruct.comp F d') (n : ℕ) (v : ↑((resFunctor φ).obj ((M.gradedCochainComplex ℳ hρ d hd hdd).X n))) : ↑((Hom.hom ((gradedCochainComplexResMap φ F hF hFd).f n)) v) = (Hom.hom F) ↑v

The chain map gradedCochainComplexResMap φ F evaluates by F.