Continuous cohomology does not see the scalars

Mathlib's continuousCohomology n X, for X : TopRep k G, is the homology of the complex of homogeneous cochains, a complex of topological k-modules built from the iterated coinduction C(G, C(G, …, X.V)) and its invariants. Forgetting the scalars, that is reading X as a continuous representation on the underlying topological abelian group X.V, gives an object TopRep.restrictScalarsInt.obj X of TopRep ℤ G, and this file proves that its continuous cohomology is the underlying topological abelian group of the continuous cohomology of X:

continuousCohomology n (TopRep.restrictScalarsInt.obj X)
  ≅ TopModuleCat.restrictScalarsInt.obj (continuousCohomology n X).

The identification is available at every level of the construction, not only on cohomology: the coinduced resolution of the underlying additive representation is the underlying additive resolution (TopRep.resolutionXRestrictScalarsIntIso, compatible with the differentials), the complex of homogeneous cochains of the underlying additive representation is the image of the complex of homogeneous cochains under the functor forgetting the scalars (TopRep.homogeneousCochainsRestrictScalarsIntIso), and the cocycles are identified by TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso. A consumer holding a cocycle of X can read it as a cocycle of the underlying additive representation and compare the two classes through TauCeti.ContCohomology.π_comp_restrictScalarsIntIso_hom.

The point of the statement is that the calculus of continuous cohomology, with its explicit low degree cocycles, its long exact sequences and its comparison with discrete group cohomology, is developed for coefficients in TopRep ℤ G, in particular for the discrete modules TauCeti.ofDiscreteModule ℤ G M, while the coefficient objects of the pro-p theory, such as the trivial representation on 𝔽_p, are objects of TopRep (ZMod p) G so that their cohomology is a vector space over 𝔽_p. The isomorphism here, together with TauCeti.ContCohomology.ofDiscreteModule_eq_restrictScalarsInt_obj, which identifies the underlying additive representation of a discrete X with TauCeti.ofDiscreteModule ℤ G X.V, is what lets every result of the first kind be applied to coefficients of the second kind.

Main definitions

• TopRep.resolutionXRestrictScalarsIntIso: the coinduced resolution of the underlying additive representation is the underlying additive resolution.
• TopRep.homogeneousCochainsRestrictScalarsIntIso: the homogeneous cochains of the underlying additive representation are the image of the homogeneous cochains under forgetting the scalars.
• TauCeti.ContCohomology.restrictScalarsIntIso: continuous cohomology commutes with forgetting the scalars, as an isomorphism in TopModuleCat ℤ; TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso is the corresponding identification of the cocycles.
• TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso: for a discrete X, the continuous cohomology of ofDiscreteModule ℤ G X.V is the underlying topological abelian group of the continuous cohomology of X; subsingleton_continuousCohomology_ofDiscreteModule_iff and nontrivial_continuousCohomology_ofDiscreteModule_iff read it on vanishing, and TauCeti.ContCohomology.ofDiscreteModuleCocyclesRestrictScalarsIntIso is the corresponding identification of the cocycles.

Main results

• TopRep.d_comp_resolutionXRestrictScalarsIntIso_hom: the identification of the resolutions commutes with the differentials.
• TauCeti.ContCohomology.π_comp_restrictScalarsIntIso_hom: the isomorphism carries the class of a cocycle to the class of the corresponding cocycle, and TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso_hom_comp_map_iCycles identifies the corresponding cocycle as the same homogeneous cochain; TauCeti.ContCohomology.π_comp_ofDiscreteModuleRestrictScalarsIntIso_hom and TauCeti.ContCohomology.iCycles_ofDiscreteModuleCocyclesRestrictScalarsIntIso_hom_apply are the corresponding statements for a discrete X. The additive equivalences TauCeti.ContCohomology.restrictScalarsIntEquiv, TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv and TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv between the carriers are the isomorphisms on elements; they act through the values of the iterated function spaces (TopRep.resolutionXRestrictScalarsIntIso_succ_hom_apply, TauCeti.ContCohomology.iCycles_cocyclesRestrictScalarsIntEquiv_zero_apply and its analogues in degrees one and two, TauCeti.ContCohomology.restrictScalarsIntEquiv_π).
• TauCeti.ContCohomology.coeffMap_comp_restrictScalarsIntIso_hom: the isomorphism is natural in the representation, with respect to the coefficient maps TauCeti.ContinuousCohomology.coeffMap; TopRep.cochainsMap_comp_homogeneousCochainsRestrictScalarsIntIso_hom and TauCeti.ContCohomology.cocyclesMap_comp_cocyclesRestrictScalarsIntIso_hom are the corresponding statements for the cochains and the cocycles.
• TauCeti.ContCohomology.map_comp_restrictScalarsIntIso_hom_of_hom: the isomorphism is also natural with respect to the simultaneous change of group and coefficients ContinuousCohomology.map phi f along a continuous homomorphism phi : H →ₜ* G, with the scalar-restricted coefficient map TopRep.resRestrictScalarsIntMap phi f. This is what transfers statements about change-of-group maps, such as Shapiro's lemma, from discrete ℤ-modules to coefficients over an arbitrary ring.
• TauCeti.ContCohomology.ofDiscreteModule_eq_restrictScalarsInt_obj: for a discrete X, the underlying additive representation is TauCeti.ofDiscreteModule ℤ G X.V.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. I, §2: the cohomology of a profinite group with coefficients in a discrete module is computed by continuous cochains valued in the underlying abelian group; no scalars enter the construction.

The resolution

noncomputable def TopRep.resolutionXRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : (restrictScalarsInt.obj X).resolutionX n ≅ restrictScalarsInt.obj (X.resolutionX n)

The coinduced resolution of the underlying additive representation of X is the underlying additive resolution of X, degree by degree: in degree n both sides are the representation on the iterated function space C(G, C(G, …, X.V)).

Equations

• X.resolutionXRestrictScalarsIntIso 0 = CategoryTheory.Iso.refl ((TopRep.restrictScalarsInt.obj X).resolutionX 0)
• X.resolutionXRestrictScalarsIntIso n.succ = (TopRep.coind₁Functor ℤ G).mapIso (X.resolutionXRestrictScalarsIntIso n) ≪≫ (X.resolutionX n).coind₁RestrictScalarsIntIso

@[simp]

theorem TopRep.resolutionXRestrictScalarsIntIso_zero {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : X.resolutionXRestrictScalarsIntIso 0 = CategoryTheory.Iso.refl ((restrictScalarsInt.obj X).resolutionX 0)

In degree zero the identification of the resolutions is the identity.

theorem TopRep.resolutionXRestrictScalarsIntIso_zero_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (x : ↑((restrictScalarsInt.obj X).resolutionX 0)) : (Hom.hom (X.resolutionXRestrictScalarsIntIso 0).hom) x = x

In degree zero the identification of the resolutions does not change elements.

theorem TopRep.resolutionXRestrictScalarsIntIso_succ {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.resolutionXRestrictScalarsIntIso (n + 1) = (coind₁Functor ℤ G).mapIso (X.resolutionXRestrictScalarsIntIso n) ≪≫ (X.resolutionX n).coind₁RestrictScalarsIntIso

In degree n + 1 the identification of the resolutions is the coinduction of the identification in degree n, followed by the identification of the coinduced representations.

@[simp]

theorem TopRep.resolutionXRestrictScalarsIntIso_succ_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (f : ↑((restrictScalarsInt.obj X).resolutionX (n + 1))) (g : G) : ((Hom.hom (X.resolutionXRestrictScalarsIntIso (n + 1)).hom) f) g = (Hom.hom (X.resolutionXRestrictScalarsIntIso n).hom) (f g)

In degree n + 1 the identification of the resolutions acts on an element of the iterated function space C(G, C(G, …, X.V)) by applying the identification in degree n to its values.

theorem TopRep.d_comp_resolutionXRestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((restrictScalarsInt.obj X).d n) (X.resolutionXRestrictScalarsIntIso (n + 1)).hom = CategoryTheory.CategoryStruct.comp (X.resolutionXRestrictScalarsIntIso n).hom (restrictScalarsInt.map (X.d n))

The identification of the resolutions commutes with the differentials of the resolution.

theorem TopRep.d_comp_resolutionXRestrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) {Z : TopRep ℤ G} (h : restrictScalarsInt.obj (X.resolutionX (n + 1)) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((restrictScalarsInt.obj X).d n) (CategoryTheory.CategoryStruct.comp (X.resolutionXRestrictScalarsIntIso (n + 1)).hom h) = CategoryTheory.CategoryStruct.comp (X.resolutionXRestrictScalarsIntIso n).hom (CategoryTheory.CategoryStruct.comp (restrictScalarsInt.map (X.d n)) h)

The identification of the resolutions commutes with the differentials of the resolution.

The homogeneous cochains

noncomputable def TopRep.homogeneousCochainsRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) : (restrictScalarsInt.obj X).homogeneousCochains ≅ (TopModuleCat.restrictScalarsInt.mapHomologicalComplex (ComplexShape.up ℕ)).obj X.homogeneousCochains

The complex of homogeneous cochains of the underlying additive representation of X is the image of the complex of homogeneous cochains of X under the functor forgetting the scalars.

Equations

• One or more equations did not get rendered due to their size.

theorem TopRep.homogeneousCochainsRestrictScalarsIntIso_hom_f {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : X.homogeneousCochainsRestrictScalarsIntIso.hom.f n = ((invariantsFunctor ℤ G).mapIso (X.resolutionXRestrictScalarsIntIso (n + 1)) ≪≫ (X.resolutionX (n + 1)).invariantsRestrictScalarsIntIso).hom

The component in degree n of homogeneousCochainsRestrictScalarsIntIso is the identification of the invariants of the identified resolutions.

theorem TopRep.coe_homogeneousCochainsRestrictScalarsIntIso_hom_f {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (u : ↑((restrictScalarsInt.obj X).homogeneousCochains.X n).toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom (X.homogeneousCochainsRestrictScalarsIntIso.hom.f n)) u) = (Hom.hom (X.resolutionXRestrictScalarsIntIso (n + 1)).hom) ↑u

On elements, the identification of the homogeneous cochains in degree n is the identification of the resolutions in degree n + 1 on the underlying invariant elements.

Naturality

theorem TopRep.resolutionXRestrictScalarsIntIso_hom_resolutionMap_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep k G} (f : X ⟶ Y) (i : ℕ) (v : ↑((restrictScalarsInt.obj X).resolutionX i)) : (Hom.hom (Y.resolutionXRestrictScalarsIntIso i).hom) ((Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) (restrictScalarsInt.map f) i)) v) = (Hom.hom (ContinuousCohomology.resolutionMap (ContinuousMonoidHom.id G) f i)) ((Hom.hom (X.resolutionXRestrictScalarsIntIso i).hom) v)

The identification of the resolutions is natural in the representation: on the elements of the resolutions, the map induced by the underlying additive map of f is the map induced by f.

theorem TopRep.cochainsMap_comp_homogeneousCochainsRestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : TopRep k G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) (restrictScalarsInt.map f)) Y.homogeneousCochainsRestrictScalarsIntIso.hom = CategoryTheory.CategoryStruct.comp X.homogeneousCochainsRestrictScalarsIntIso.hom ((TopModuleCat.restrictScalarsInt.mapHomologicalComplex (ComplexShape.up ℕ)).map (ContinuousCohomology.cochainsMap (ContinuousMonoidHom.id G) f))

The identification of the complexes of homogeneous cochains is natural in the representation.

Continuous cohomology

noncomputable def TauCeti.ContCohomology.restrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : continuousCohomology n (TopRep.restrictScalarsInt.obj X) ≅ TopModuleCat.restrictScalarsInt.obj (continuousCohomology n X)

Continuous cohomology does not see the scalars. The continuous cohomology of the underlying additive representation of X is the underlying topological abelian group of the continuous cohomology of X.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) n ≅ TopModuleCat.restrictScalarsInt.obj (ContinuousCohomology.cocycles X n)

The cocycles of the underlying additive representation of X are the underlying topological abelian group of the cocycles of X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso_hom_comp_map_iCycles {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (HomologicalComplex.iCycles X.homogeneousCochains n)) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains n) (X.homogeneousCochainsRestrictScalarsIntIso.hom.f n)

Under cocyclesRestrictScalarsIntIso, a cocycle corresponds to the same homogeneous cochain, read through homogeneousCochainsRestrictScalarsIntIso.

@[simp]

theorem TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso_hom_comp_map_iCycles_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj (X.homogeneousCochains.X n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (HomologicalComplex.iCycles X.homogeneousCochains n)) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains n) (CategoryTheory.CategoryStruct.comp (X.homogeneousCochainsRestrictScalarsIntIso.hom.f n) h)

Under cocyclesRestrictScalarsIntIso, a cocycle corresponds to the same homogeneous cochain, read through homogeneousCochainsRestrictScalarsIntIso.

@[simp]

theorem TauCeti.ContCohomology.π_comp_restrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π (TopRep.restrictScalarsInt.obj X) n) (restrictScalarsIntIso X n).hom = CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.π X n))

restrictScalarsIntIso carries the class of a cocycle of the underlying additive representation to the class of the corresponding cocycle of X.

@[simp]

theorem TauCeti.ContCohomology.π_comp_restrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj (continuousCohomology n X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π (TopRep.restrictScalarsInt.obj X) n) (CategoryTheory.CategoryStruct.comp (restrictScalarsIntIso X n).hom h) = CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.π X n)) h)

restrictScalarsIntIso carries the class of a cocycle of the underlying additive representation to the class of the corresponding cocycle of X.

noncomputable def TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) n).toModuleCat ≃+ ↑(ContinuousCohomology.cocycles X n).toModuleCat

The cocycles of the underlying additive representation of X are the cocycles of X, as an additive equivalence between the carriers.

Equations

• TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv X n = (↑(TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso X n).toContinuousLinearEquiv).toAddEquiv

theorem TauCeti.ContCohomology.cocyclesRestrictScalarsIntEquiv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) n).toModuleCat) : (cocyclesRestrictScalarsIntEquiv X n) v = (CategoryTheory.ConcreteCategory.hom (cocyclesRestrictScalarsIntIso X n).hom) v

The additive equivalence cocyclesRestrictScalarsIntEquiv is cocyclesRestrictScalarsIntIso on elements.

noncomputable def TauCeti.ContCohomology.restrictScalarsIntEquiv {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) : ↑(continuousCohomology n (TopRep.restrictScalarsInt.obj X)).toModuleCat ≃+ ↑(continuousCohomology n X).toModuleCat

The continuous cohomology of the underlying additive representation of X is the continuous cohomology of X, as an additive equivalence between the carriers.

Equations

• TauCeti.ContCohomology.restrictScalarsIntEquiv X n = (↑(TauCeti.ContCohomology.restrictScalarsIntIso X n).toContinuousLinearEquiv).toAddEquiv

theorem TauCeti.ContCohomology.restrictScalarsIntEquiv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (a : ↑(continuousCohomology n (TopRep.restrictScalarsInt.obj X)).toModuleCat) : (restrictScalarsIntEquiv X n) a = (CategoryTheory.ConcreteCategory.hom (restrictScalarsIntIso X n).hom) a

The additive equivalence restrictScalarsIntEquiv is restrictScalarsIntIso on elements.

@[simp]

theorem TauCeti.ContCohomology.restrictScalarsIntEquiv_π {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) n).toModuleCat) : (restrictScalarsIntEquiv X n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (TopRep.restrictScalarsInt.obj X) n)) v) = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) ((cocyclesRestrictScalarsIntEquiv X n) v)

restrictScalarsIntEquiv carries the class of a cocycle of the underlying additive representation to the class of the corresponding cocycle of X.

theorem TauCeti.ContCohomology.coe_iCycles_cocyclesRestrictScalarsIntEquiv {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (n : ℕ) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) n).toModuleCat) : ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains n)) ((cocyclesRestrictScalarsIntEquiv X n) v)) = (TopRep.Hom.hom (X.resolutionXRestrictScalarsIntIso (n + 1)).hom) ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains n)) v)

Under cocyclesRestrictScalarsIntEquiv, the underlying homogeneous cochain of a cocycle is carried by the identification of the resolutions.

theorem TauCeti.ContCohomology.iCycles_cocyclesRestrictScalarsIntEquiv_zero_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 0).toModuleCat) (g₀ : G) : ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 0)) ((cocyclesRestrictScalarsIntEquiv X 0) v)) g₀ = ↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains 0)) v) g₀

In degree zero, cocyclesRestrictScalarsIntEquiv does not change the values of a homogeneous cocycle: both sides are the function C(G, X.V) underlying the cocycle.

theorem TauCeti.ContCohomology.iCycles_cocyclesRestrictScalarsIntEquiv_one_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 1).toModuleCat) (g₀ g₁ : G) : (↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 1)) ((cocyclesRestrictScalarsIntEquiv X 1) v)) g₀) g₁ = (↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains 1)) v) g₀) g₁

In degree one, cocyclesRestrictScalarsIntEquiv does not change the values of a homogeneous cocycle: both sides are the function C(G, C(G, X.V)) underlying the cocycle.

theorem TauCeti.ContCohomology.iCycles_cocyclesRestrictScalarsIntEquiv_two_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) (v : ↑(ContinuousCohomology.cocycles (TopRep.restrictScalarsInt.obj X) 2).toModuleCat) (g₀ g₁ g₂ : G) : ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 2)) ((cocyclesRestrictScalarsIntEquiv X 2) v)) g₀) g₁) g₂ = ((↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopRep.restrictScalarsInt.obj X).homogeneousCochains 2)) v) g₀) g₁) g₂

In degree two, cocyclesRestrictScalarsIntEquiv does not change the values of a homogeneous cocycle.

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap_comp_cocyclesRestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (n : ℕ) {Y : TopRep k G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap (ContinuousMonoidHom.id G) (TopRep.restrictScalarsInt.map f) n) (cocyclesRestrictScalarsIntIso Y n).hom = CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.cocyclesMap (ContinuousMonoidHom.id G) f n))

The identification of the cocycles is natural in the representation: on cocycles, the map induced by the underlying additive map of f is the underlying additive map of the map induced by f.

@[simp]

theorem TauCeti.ContCohomology.cocyclesMap_comp_cocyclesRestrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (n : ℕ) {Y : TopRep k G} (f : X ⟶ Y) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj (ContinuousCohomology.cocycles Y n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cocyclesMap (ContinuousMonoidHom.id G) (TopRep.restrictScalarsInt.map f) n) (CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso Y n).hom h) = CategoryTheory.CategoryStruct.comp (cocyclesRestrictScalarsIntIso X n).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.cocyclesMap (ContinuousMonoidHom.id G) f n)) h)

The identification of the cocycles is natural in the representation: on cocycles, the map induced by the underlying additive map of f is the underlying additive map of the map induced by f.

@[simp]

theorem TauCeti.ContCohomology.coeffMap_comp_restrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (n : ℕ) {Y : TopRep k G} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (TopRep.restrictScalarsInt.map f) n) (restrictScalarsIntIso Y n).hom = CategoryTheory.CategoryStruct.comp (restrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.coeffMap f n))

Continuous cohomology does not see the scalars, naturally. The identification restrictScalarsIntIso is natural in the representation: it carries the coefficient map of the underlying additive map of f to the underlying additive map of the coefficient map of f.

@[simp]

theorem TauCeti.ContCohomology.coeffMap_comp_restrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep k G} (n : ℕ) {Y : TopRep k G} (f : X ⟶ Y) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj (continuousCohomology n Y) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.coeffMap (TopRep.restrictScalarsInt.map f) n) (CategoryTheory.CategoryStruct.comp (restrictScalarsIntIso Y n).hom h) = CategoryTheory.CategoryStruct.comp (restrictScalarsIntIso X n).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.coeffMap f n)) h)

Continuous cohomology does not see the scalars, naturally. The identification restrictScalarsIntIso is natural in the representation: it carries the coefficient map of the underlying additive map of f to the underlying additive map of the coefficient map of f.

theorem TauCeti.ContCohomology.map_comp_restrictScalarsIntIso_hom_of_hom {R : Type v} [Ring R] [TopologicalSpace R] {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [IsTopologicalGroup H] {X : TopRep R G} {Y : TopRep R H} (phi : H →ₜ* G) (f : TopRep.res (↑phi) X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.map phi (TopRep.resRestrictScalarsIntMap (↑phi) f) n) (restrictScalarsIntIso Y n).hom = CategoryTheory.CategoryStruct.comp (restrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.map phi f n))

Scalar restriction commutes with the simultaneous group-and-coefficient map on continuous cohomology.

Discrete coefficients

theorem TauCeti.ContCohomology.ofDiscreteModule_ρ_eq_restrictScalarsInt_obj_ρ {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) [DiscreteTopology ↑X] : (ofDiscreteModule ℤ G ↑X).ρ = (TopRep.restrictScalarsInt.obj X).ρ

For a discrete X, the operators of the underlying additive representation of X are those of the object attached by the discrete coefficient dictionary to X.V with the action read off from X.

theorem TauCeti.ContCohomology.ofDiscreteModule_eq_restrictScalarsInt_obj {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) [DiscreteTopology ↑X] : ofDiscreteModule ℤ G ↑X = TopRep.restrictScalarsInt.obj X

For a discrete X, the underlying additive representation of X is the object attached by the discrete coefficient dictionary to X.V with the action read off from X. Together with restrictScalarsIntIso, this applies every statement about the coefficients TauCeti.ofDiscreteModule ℤ G M to the continuous cohomology of X.

theorem TauCeti.ContCohomology.cast_ofDiscreteModule_eq_restrictScalarsInt_obj {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Monoid G] (X : TopRep k G) [DiscreteTopology ↑X] (x : ↑(ofDiscreteModule ℤ G ↑X)) : cast ⋯ x = have this := x; this

The carrier cast identifying discrete coefficients with their underlying additive representation is the identity.

noncomputable def TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : continuousCohomology n (ofDiscreteModule ℤ G ↑X) ≅ TopModuleCat.restrictScalarsInt.obj (continuousCohomology n X)

The continuous cohomology of a discrete representation over any scalars is that of its carrier as a discrete ℤ-module, with the action read off from X: the composite of ofDiscreteModule_eq_restrictScalarsInt_obj and restrictScalarsIntIso.

Equations

• TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso X n = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.ContCohomology.restrictScalarsIntIso X n

theorem TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : (ofDiscreteModuleRestrictScalarsIntIso X n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (restrictScalarsIntIso X n).hom

The morphism of ofDiscreteModuleRestrictScalarsIntIso is the coefficient transport followed by the scalar-restriction isomorphism.

noncomputable def TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : ↑(continuousCohomology n (ofDiscreteModule ℤ G ↑X)).toModuleCat ≃+ ↑(continuousCohomology n X).toModuleCat

The continuous cohomology of the carrier of a discrete X as a discrete ℤ-module is the continuous cohomology of X, as an additive equivalence between the carriers.

Equations

• TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv X n = (↑(TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntIso X n).toContinuousLinearEquiv).toAddEquiv

theorem TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) (a : ↑(continuousCohomology n (ofDiscreteModule ℤ G ↑X)).toModuleCat) : (ofDiscreteModuleRestrictScalarsIntEquiv X n) a = (restrictScalarsIntEquiv X n) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) a)

ofDiscreteModuleRestrictScalarsIntEquiv is the transport along the equality of objects followed by restrictScalarsIntEquiv.

noncomputable def TauCeti.ContCohomology.ofDiscreteModuleCocyclesRestrictScalarsIntIso {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : ContinuousCohomology.cocycles (ofDiscreteModule ℤ G ↑X) n ≅ TopModuleCat.restrictScalarsInt.obj (ContinuousCohomology.cocycles X n)

The cocycles of the carrier of a discrete X as a discrete ℤ-module are the underlying topological abelian group of the cocycles of X: the composite of ofDiscreteModule_eq_restrictScalarsInt_obj and cocyclesRestrictScalarsIntIso.

Equations

• TauCeti.ContCohomology.ofDiscreteModuleCocyclesRestrictScalarsIntIso X n = CategoryTheory.eqToIso ⋯ ≪≫ TauCeti.ContCohomology.cocyclesRestrictScalarsIntIso X n

theorem TauCeti.ContCohomology.ofDiscreteModuleCocyclesRestrictScalarsIntIso_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) (w : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G ↑X) n).toModuleCat) : (CategoryTheory.ConcreteCategory.hom (ofDiscreteModuleCocyclesRestrictScalarsIntIso X n).hom) w = (cocyclesRestrictScalarsIntEquiv X n) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) w)

ofDiscreteModuleCocyclesRestrictScalarsIntIso is the transport along the equality of objects followed by cocyclesRestrictScalarsIntEquiv.

@[simp]

theorem TauCeti.ContCohomology.π_comp_ofDiscreteModuleRestrictScalarsIntIso_hom {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π (ofDiscreteModule ℤ G ↑X) n) (ofDiscreteModuleRestrictScalarsIntIso X n).hom = CategoryTheory.CategoryStruct.comp (ofDiscreteModuleCocyclesRestrictScalarsIntIso X n).hom (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.π X n))

ofDiscreteModuleRestrictScalarsIntIso carries the class of a cocycle of the carrier to the class of the corresponding cocycle of X.

@[simp]

theorem TauCeti.ContCohomology.π_comp_ofDiscreteModuleRestrictScalarsIntIso_hom_assoc {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) {Z : TopModuleCat ℤ} (h : TopModuleCat.restrictScalarsInt.obj (continuousCohomology n X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (ContinuousCohomology.π (ofDiscreteModule ℤ G ↑X) n) (CategoryTheory.CategoryStruct.comp (ofDiscreteModuleRestrictScalarsIntIso X n).hom h) = CategoryTheory.CategoryStruct.comp (ofDiscreteModuleCocyclesRestrictScalarsIntIso X n).hom (CategoryTheory.CategoryStruct.comp (TopModuleCat.restrictScalarsInt.map (ContinuousCohomology.π X n)) h)

ofDiscreteModuleRestrictScalarsIntIso carries the class of a cocycle of the carrier to the class of the corresponding cocycle of X.

@[simp]

theorem TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv_π {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) (w : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G ↑X) n).toModuleCat) : (ofDiscreteModuleRestrictScalarsIntEquiv X n) ((CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π (ofDiscreteModule ℤ G ↑X) n)) w) = (CategoryTheory.ConcreteCategory.hom (ContinuousCohomology.π X n)) ((CategoryTheory.ConcreteCategory.hom (ofDiscreteModuleCocyclesRestrictScalarsIntIso X n).hom) w)

ofDiscreteModuleRestrictScalarsIntEquiv carries the class of a cocycle of the carrier to the class of the corresponding cocycle of X.

theorem TauCeti.ContCohomology.iCycles_ofDiscreteModuleCocyclesRestrictScalarsIntIso_hom_apply {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (w : ↑(ContinuousCohomology.cocycles (ofDiscreteModule ℤ G ↑X) 1).toModuleCat) (g₀ g₁ : G) : (↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles X.homogeneousCochains 1)) ((CategoryTheory.ConcreteCategory.hom (ofDiscreteModuleCocyclesRestrictScalarsIntIso X 1).hom) w)) g₀) g₁ = (↑((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (ofDiscreteModule ℤ G ↑X).homogeneousCochains 1)) w) g₀) g₁

In degree one, ofDiscreteModuleCocyclesRestrictScalarsIntIso does not change the values of a homogeneous cocycle.

theorem TauCeti.ContCohomology.subsingleton_continuousCohomology_ofDiscreteModule_iff {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : Subsingleton ↑(continuousCohomology n (ofDiscreteModule ℤ G ↑X)).toModuleCat ↔ Subsingleton ↑(continuousCohomology n X).toModuleCat

Hⁿ(G, X) vanishes exactly when the ℤ-cohomology of the carrier of the discrete X vanishes.

theorem TauCeti.ContCohomology.nontrivial_continuousCohomology_ofDiscreteModule_iff {k : Type u_1} [Ring k] [TopologicalSpace k] {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep k G) [DiscreteTopology ↑X] (n : ℕ) : Nontrivial ↑(continuousCohomology n (ofDiscreteModule ℤ G ↑X)).toModuleCat ↔ Nontrivial ↑(continuousCohomology n X).toModuleCat

Hⁿ(G, X) is nontrivial exactly when the ℤ-cohomology of the carrier of the discrete X is nontrivial.