The comparison of a graded representation with the total coinduced resolution

Let M be a discrete topological representation of G with a ℤ-grading ℳ by invariant submodules and an equivariant differential d of degree one, and let c : TopRep.ResolutionContraction X (M.gradedCochainComplex ℳ hρ d hd hdd) contract the complex it assembles onto X. The comparison c.comparison maps that complex, degree by degree, into the coinduced resolution of X. When M is the direct sum of its pieces (DirectSum.Decomposition ℳ), these components add up to a single morphism of representations on the total modules,

κ : M ⟶ X.gradedResolutionTopRep,      κ v = ∑ₙ Fⁿ (vₙ),

applying the degree-n component Fⁿ of the comparison to the degree-n part vₙ of v and discarding the parts of negative degree (TopRep.ResolutionContraction.gradedComparison). It has degree zero and lies over the identity of X. It commutes with the differentials on the pieces of non-negative degree, and on all of M as soon as d does not leave the negative degrees, that is, kills ℳ (-1). For smooth discrete X over a compact group, a homogeneous cocycle z of M fixed by G and the homogeneous cocycle κ z of the total coinduced resolution have the same class in Hⁿ(G, X) (TopRep.ResolutionContraction.gradedCohomologyClass_gradedComparison).

Constructions on total modules, such as tensor induction, act on morphisms of representations rather than on families of components, so this is the form in which a contracted graded representation, such as a tensor-induced resolution, is compared with the total coinduced resolution. In Evens' multiplicative transfer along a tower V ≤ U ≤ G of compact open subgroups, the norm from V to U of a cocycle is the class of a cocycle of the tensor-induced resolution from V to U; its image under κ is a cocycle of the total coinduced resolution with the same class, which is the kind of cocycle the norm from U to G is computed on.

Main definitions

• TopRep.ResolutionContraction.gradedComparison: the comparison on total modules.

Main results

• TopRep.ResolutionContraction.gradedComparison_apply_of_mem: on ℳ n it is the degree-n component of c.comparison, included in degree n.
• TopRep.ResolutionContraction.gradedComparison_apply_of_mem_of_neg: it vanishes in negative degrees.
• TopRep.ResolutionContraction.isHomogeneous_gradedComparison: it has degree zero.
• TopRep.ResolutionContraction.gradedComparison_ι_apply: it carries the augmentation of c to the augmentation of the total resolution.
• TopRep.ResolutionContraction.gradedComparison_differential_apply_of_mem: it commutes with the differentials on the pieces of non-negative degree.
• TopRep.ResolutionContraction.gradedComparison_differential: it commutes with the differentials when d kills ℳ (-1).
• TopRep.ResolutionContraction.gradedCohomologyClass_gradedComparison: it preserves classes of homogeneous cocycles.

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.

noncomputable def TopRep.ResolutionContraction.gradedComparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] : M ⟶ X.gradedResolutionTopRep

The comparison on total modules. Through the decomposition of M into its pieces, the degree-n components Fⁿ of the comparison c.comparison assemble to the morphism v ↦ ∑ₙ Fⁿ (vₙ) from M to the total coinduced resolution of X, where vₙ is the part of v in ℳ n; the parts of negative degree are sent to zero.

theorem TopRep.ResolutionContraction.gradedComparison_apply_of_mem {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {n : ℕ} {v : ↑M} (hv : v ∈ ℳ ↑n) : (Hom.hom c.gradedComparison) v = (DirectSum.lof k ℕ (fun (n : ℕ) => ↑(X.resolutionX (n + 1))) n) ((Hom.hom (c.comparison.f n)) ⟨v, hv⟩)

On the piece ℳ n, the comparison on total modules is the degree-n component of c.comparison, included in degree n of the total resolution.

theorem TopRep.ResolutionContraction.gradedComparison_apply_of_mem_of_neg {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {p : ℤ} (hp : p < 0) {v : ↑M} (hv : v ∈ ℳ p) : (Hom.hom c.gradedComparison) v = 0

The comparison on total modules vanishes on the pieces of negative degree.

theorem TopRep.ResolutionContraction.isHomogeneous_gradedComparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] : TauCeti.LinearMap.IsHomogeneous (↑(Hom.hom c.gradedComparison).toContinuousLinearMap) ℳ X.gradedResolutionPiece 0

The comparison on total modules has degree zero.

theorem TopRep.ResolutionContraction.gradedComparison_mem_gradedResolutionPiece {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {p : ℤ} {v : ↑M} (hv : v ∈ ℳ p) : (Hom.hom c.gradedComparison) v ∈ X.gradedResolutionPiece p

The comparison on total modules carries ℳ p into the piece of degree p of the total resolution.

theorem TopRep.ResolutionContraction.gradedResolutionTopRep_ρ_gradedComparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {v : ↑M} (hv : ∀ (g : G), (M.ρ g) v = v) (g : G) : (X.gradedResolutionTopRep.ρ g) ((Hom.hom c.gradedComparison) v) = (Hom.hom c.gradedComparison) v

The comparison on total modules carries a vector fixed by G to a vector fixed by G.

@[simp]

theorem TopRep.ResolutionContraction.gradedComparison_ι_apply {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] (x : ↑X) : (Hom.hom c.gradedComparison) ↑((Hom.hom c.ι) x) = X.gradedResolutionAugmentation x

The comparison lies over the identity of X: it carries the augmentation of c to the augmentation of the total coinduced resolution, by constant functions in degree zero.

theorem TopRep.ResolutionContraction.gradedComparison_differential_apply_of_mem {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {n : ℕ} {v : ↑M} (hv : v ∈ ℳ ↑n) : (Hom.hom X.gradedResolutionTopRepDifferential) ((Hom.hom c.gradedComparison) v) = (Hom.hom c.gradedComparison) ((Hom.hom d) v)

The comparison commutes with the differentials on the pieces of non-negative degree.

theorem TopRep.ResolutionContraction.gradedResolutionTopRepDifferential_gradedComparison_eq_zero {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] {n : ℕ} {z : ↑M} (hz : z ∈ ℳ ↑n) (hdz : (Hom.hom d) z = 0) : (Hom.hom X.gradedResolutionTopRepDifferential) ((Hom.hom c.gradedComparison) z) = 0

The comparison carries a homogeneous cocycle of non-negative degree to a cocycle of the total coinduced resolution.

theorem TopRep.ResolutionContraction.gradedComparison_differential {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] (hneg : ∀ v ∈ ℳ (-1), (Hom.hom d) v = 0) : CategoryTheory.CategoryStruct.comp d c.gradedComparison = CategoryTheory.CategoryStruct.comp c.gradedComparison X.gradedResolutionTopRepDifferential

The comparison commutes with the differentials, provided d kills the piece ℳ (-1), so that it does not carry the discarded negative degrees into degree zero. This holds in particular when the pieces of negative degree vanish.

theorem TopRep.ResolutionContraction.gradedCohomologyClass_gradedComparison {k : Type u} [Ring k] [TopologicalSpace k] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup 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} (c : X.ResolutionContraction (M.gradedCochainComplex ℳ hρ d hd hdd)) [DirectSum.Decomposition ℳ] [DiscreteTopology k] [DiscreteTopology ↑M] [CompactSpace G] (hX : TauCeti.IsSmoothDiscrete k X) {n : ℕ} {z : ↑M} (hz : z ∈ ℳ ↑n) (hinv : ∀ (g : G), (M.ρ g) z = z) (hdz : (Hom.hom d) z = 0) : (gradedResolutionContraction hX).gradedCohomologyClass ((Hom.hom c.gradedComparison) z) ⋯ ⋯ ⋯ = c.gradedCohomologyClass z hz hinv hdz

The comparison preserves classes. For smooth discrete X over a compact group, a homogeneous cocycle z ∈ ℳ n fixed by G has the same class in Hⁿ(G, X) through c as the homogeneous cocycle κ z of the total coinduced resolution through its evaluation-at-1 contraction TopRep.gradedResolutionContraction.