The ZMod n-module structure on H¹ and its continuous-dual interpretation

For a topological group G acting continuously on a ZMod n-module A, the quotient H¹(G, A) = Z¹/B¹ carries a ZMod n-module structure: scalar n annihilates every A-valued element of the ambient group, hence every continuous 1-cocycle, hence the 1-coboundaries and their cosets, so TauCeti.instModuleH1 transports the module structure to the quotient. This is the same observation that gives the continuous character group its own ZMod n-module structure in TauCeti.Topology.Algebra.ContinuousZModDual, and it needs no profiniteness and no pro-p hypothesis: it holds for every n and every continuous action.

When the action is trivial, a continuous 1-cocycle is a continuous character, so TauCeti.ContCohomology.H1EquivOfSmulEqSelf identifies H¹(G, ZMod n) additively with the continuous character group, and TauCeti.h1EquivContinuousZModDual upgrades that to an isomorphism of ZMod n-modules with the continuous ZMod n-dual TauCeti.continuousZModDual n G that the module structure makes meaningful. The modulus n is arbitrary, so this is a statement about modules; when n is prime, ZMod n is a field and the statement is one about vector spaces. The two application lemmas TauCeti.h1EquivContinuousZModDual_apply_mk and TauCeti.h1EquivContinuousZModDual_symm_apply compute the isomorphism in both directions, so the identification is usable without unfolding it.

Taking n to be a prime p and G a pro-p group makes this the coefficient-level input to the H¹ interpretation of such a group: the pro-p consequence, the identification of H¹(G, 𝔽_p) with the continuous 𝔽_p-dual of the Frattini quotient and the transfer of Burnside's basis theorem, is in TauCeti.Topology.Algebra.Group.Profinite.ProP.H1Dual.

Main definitions

• TauCeti.instModuleH1: H¹(G, A) is a ZMod n-module when A is, for any continuous action.
• TauCeti.h1EquivContinuousZModHom: for a trivial action, H¹(G, A) is the module of continuous homomorphisms from G to the additive group of A.
• TauCeti.h1EquivContinuousZModDual: for a trivial action, H¹(G, ZMod n) is the continuous ZMod n-dual TauCeti.continuousZModDual n G of G, as ZMod n-modules.

Main results

• TauCeti.h1EquivContinuousZModDual_apply_mk: the class of a continuous 1-cocycle is sent to the character it defines.
• TauCeti.h1EquivContinuousZModDual_symm_apply: a continuous character is sent to the class of the 1-cocycle it defines.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 2.8.
• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, (3.9.1).

@[instance_reducible]

noncomputable instance TauCeti.instModuleH1 {n : ℕ} {G : Type u} [Monoid G] [TopologicalSpace G] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] : Module (ZMod n) (ContCohomology.H1 G A)

H¹(G, A) inherits the ZMod n-module structure of A. Scalar n annihilates every continuous A-valued 1-cocycle, so it annihilates the subgroup of 1-coboundaries, and the quotient Z¹/B¹ inherits a ZMod n-module structure. The coefficient action is arbitrary.

noncomputable def TauCeti.h1EquivContinuousZModHom {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (htriv : ∀ (g : G) (a : A), g • a = a) : ContCohomology.H1 G A ≃ₗ[ZMod n] Additive (G →ₜ* Multiplicative A)

For a trivial action on a ZMod n-module A, first cohomology is the ZMod n-module of continuous homomorphisms from G to the additive group of A.

@[simp]

theorem TauCeti.h1EquivContinuousZModHom_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (htriv : ∀ (g : G) (a : A), g • a = a) (x : ContCohomology.H1 G A) : (h1EquivContinuousZModHom htriv) x = (ContCohomology.H1EquivOfSmulEqSelf htriv) x

The underlying additive equivalence of h1EquivContinuousZModHom is H1EquivOfSmulEqSelf.

@[simp]

theorem TauCeti.H1EquivOfSmulEqSelf_h1EquivContinuousZModHom_symm_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {A : Type v} [AddCommGroup A] [Module (ZMod n) A] [TopologicalSpace A] [IsTopologicalAddGroup A] [DistribMulAction G A] [ContinuousSMul G A] (htriv : ∀ (g : G) (a : A), g • a = a) (f : Additive (G →ₜ* Multiplicative A)) : (ContCohomology.H1EquivOfSmulEqSelf htriv) ((h1EquivContinuousZModHom htriv).symm f) = f

Applying H1EquivOfSmulEqSelf to the inverse of the linear equivalence recovers the continuous homomorphism.

noncomputable def TauCeti.h1EquivContinuousZModDual {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod n)] [ContinuousSMul G (ZMod n)] (htriv : ∀ (g : G) (m : ZMod n), g • m = m) : ContCohomology.H1 G (ZMod n) ≃ₗ[ZMod n] continuousZModDual n G

H¹(G, ZMod n) is the continuous ZMod n-dual of G. A class of H¹(G, ZMod n) is sent to the continuous homomorphism G → Multiplicative ZMod n that its cocycle defines, which for trivial coefficients is that cocycle itself, as an isomorphism of ZMod n-modules.

@[simp]

theorem TauCeti.h1EquivContinuousZModDual_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod n)] [ContinuousSMul G (ZMod n)] (htriv : ∀ (g : G) (m : ZMod n), g • m = m) (x : ContCohomology.H1 G (ZMod n)) : (h1EquivContinuousZModDual htriv) x = (ContCohomology.H1EquivOfSmulEqSelf htriv) x

The continuous-dual equivalence has the same underlying map as H1EquivOfSmulEqSelf.

theorem TauCeti.h1EquivContinuousZModDual_apply_mk {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod n)] [ContinuousSMul G (ZMod n)] (htriv : ∀ (g : G) (m : ZMod n), g • m = m) (f : ↥(ContCohomology.Z1 G (ZMod n))) (g : G) : (Additive.toMul ((h1EquivContinuousZModDual htriv) ↑f)) g = Multiplicative.ofAdd (↑f g)

The image of a class of H¹(G, ZMod n) is the character its cocycle defines: evaluated at g it is the cocycle's value at g, read in the multiplicative encoding of ZMod n.

@[simp]

theorem TauCeti.h1EquivContinuousZModDual_symm_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod n)] [ContinuousSMul G (ZMod n)] (htriv : ∀ (g : G) (m : ZMod n), g • m = m) (φ : continuousZModDual n G) : (h1EquivContinuousZModDual htriv).symm φ = ↑((ContCohomology.Z1EquivOfSmulEqSelf htriv).symm φ)

The inverse image of a continuous character is the class of the 1-cocycle it defines.