H²(G, M) as a ZMod n-module

Multiplication by n is zero on any ZMod n-module, so n kills the coefficients of H²(G, M), hence H²(G, M) itself (TauCeti.ContCohomology.nsmul_H2_eq_zero), which makes it a ZMod n-module in turn (TauCeti.ContCohomology.instModuleZModH2). The coefficients are left general, so that the instance also covers coefficients such as the invariants M ^ N carried by the cohomology of a quotient group, and M = ZMod n itself is the case that makes H²(G, ZMod n) a ZMod n-module, and for n a prime p an 𝔽_p-vector space, so that Module.rank, Module.finrank and Module.Finite apply to it. For a pro-p group G that dimension is the relation rank of G.

The module structure is the canonical one: Module (ZMod n) A is a subsingleton on an abelian group A (ZMod.instSubsingletonModule), so it agrees with every other way of producing one, and scalar multiplication by a natural number is the iterated sum (Nat.cast_smul_eq_nsmul).

Main results

• TauCeti.ContCohomology.instModuleZModH2: H²(G, M) is a ZMod n-module whenever M is.
• TauCeti.ContCohomology.zmod_smul_mk: on the class of a cocycle, a scalar c : ZMod n acts as the c.val-fold sum of the cocycle.

@[instance_reducible]

instance TauCeti.ContCohomology.instModuleZModH2 {n : ℕ} {G : Type u} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [Module (ZMod n) M] : Module (ZMod n) (H2 G M)

H²(G, M) is a ZMod n-module whenever the coefficients M are; in particular H²(G, ZMod n) is one, for any continuous action of G on ZMod n.

Equations

• TauCeti.ContCohomology.instModuleZModH2 = AddCommGroup.zmodModule ⋯

theorem TauCeti.ContCohomology.zmod_smul_mk {n : ℕ} {G : Type u} [Monoid G] [TopologicalSpace G] [ContinuousMul G] {M : Type v} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction G M] [ContinuousSMul G M] [NeZero n] [Module (ZMod n) M] (c : ZMod n) (z : ↥(Z2 G M)) : c • ↑z = ↑(c.val • z)

Scalar multiplication by c : ZMod n on the class of a 2-cocycle is the class of its c.val-fold sum: the scalar action of ZMod n on H²(G, M) is computed on cocycles through the natural-number action.