Continuous 1-cocycles on a free pro-p group

Let F = freeProP p X be the free pro-p group on a type X, and let M be a profinite abelian pro-p group with a continuous action of F. A continuous 1-cocycle c : F → M, that is a continuous crossed homomorphism c (g * h) = g • c h + c g, is the same thing as a continuous homomorphic section g ↦ ⟨c g, g⟩ of the semidirect product M ⋊ F → F. The semidirect product is the extension attached to the trivial factor set, it is profinite and pro-p, and such an extension of F has a continuous homomorphic section with any prescribed values on the generators (GroupExtension.exists_splitting_continuous_freeProP_forall_apply_of_eq). Since a cocycle is determined by its values on a topological generating set, this identifies the continuous 1-cocycles of F with the functions on the generators:

Z¹(F, M) ≃+ (X → M), by evaluation at the generators (TauCeti.freeProP.Z1Equiv).

Consequently a surjective continuous equivariant map M → N of coefficient modules induces a surjection Z¹(F, M) → Z¹(F, N), hence H¹(F, M) → H¹(F, N): a cocycle into N lifts to a cocycle into M by lifting its values on the generators.

No finiteness of X is needed, and M need not be discrete: any profinite abelian pro-p coefficient module with a continuous action is allowed, exactly as for the vanishing of H² in TauCeti.Topology.Algebra.Group.Profinite.Free.Cohomology. The coefficient module is written additively; the pro-p hypothesis is on Multiplicative M.

Main results

• TauCeti.freeProP.eq_of_mem_Z1_of_forall_of: continuous 1-cocycles on F agreeing on the generators are equal.
• TauCeti.freeProP.exists_mem_Z1_forall_apply_of_eq: every function on the generators extends to a continuous 1-cocycle on F.
• TauCeti.freeProP.Z1Equiv: evaluation at the generators is an additive equivalence Z¹(F, M) ≃+ (X → M).
• TauCeti.freeProP.cocyclesMap1_surjective, TauCeti.freeProP.explicitCoeff1_surjective: a surjective coefficient map induces surjections on Z¹ and H¹ of F.

References

• J.-P. Serre, Galois Cohomology, Ch. I, §3.4 and §4.2.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Ch. III, §9.

theorem TauCeti.freeProP.eq_of_mem_Z1_of_forall_of {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [T1Space M] {c₁ c₂ : freeProP p X → M} (h₁ : c₁ ∈ ContCohomology.Z1 (freeProP p X) M) (h₂ : c₂ ∈ ContCohomology.Z1 (freeProP p X) M) (h : ∀ (x : X), c₁ (of x) = c₂ (of x)) : c₁ = c₂

Two continuous 1-cocycles on a free pro-p group that agree on the generators are equal.

theorem TauCeti.freeProP.exists_mem_Z1_forall_apply_of_eq {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) (v : X → M) : ∃ c ∈ ContCohomology.Z1 (freeProP p X) M, ∀ (x : X), c (of x) = v x

Continuous 1-cocycles on a free pro-p group take prescribed values on the generators. For F = freeProP p X and M a profinite abelian pro-p group with a continuous action of F, every function X → M is the restriction to the generators of a continuous 1-cocycle F → M. The cocycle is read off a continuous homomorphic section F → M ⋊ F of the semidirect product, which the universal property of F supplies with the prescribed values.

noncomputable def TauCeti.freeProP.Z1Equiv {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) : ↥(ContCohomology.Z1 (freeProP p X) M) ≃+ (X → M)

Evaluation at the generators identifies the continuous 1-cocycles of a free pro-p group with the functions on the generators, Z¹(F, M) ≃+ (X → M).

Equations

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

@[simp]

theorem TauCeti.freeProP.Z1Equiv_apply {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) (c : ↥(ContCohomology.Z1 (freeProP p X) M)) (x : X) : (Z1Equiv hM) c x = ↑c (of x)

@[simp]

theorem TauCeti.freeProP.Z1Equiv_symm_apply_of {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) (v : X → M) (x : X) : ↑((Z1Equiv hM).symm v) (of x) = v x

theorem TauCeti.freeProP.cocyclesMap1_surjective {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) {N : Type u} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction (freeProP p X) N] [T1Space N] (f : M →+ N) (hf : Continuous ⇑f) (hequiv : ∀ (g : freeProP p X) (m : M), f ((ContinuousMonoidHom.id (freeProP p X)) g • m) = g • f m) (hsurj : Function.Surjective ⇑f) : Function.Surjective ⇑(ContCohomology.cocyclesMap1 (freeProP p X) M (freeProP p X) N (ContinuousMonoidHom.id (freeProP p X)) f hf hequiv)

A surjective coefficient map induces a surjection on the continuous 1-cocycles of a free pro-p group. For f : M → N continuous, equivariant and surjective, every continuous 1-cocycle c : F → N is f ∘ c' for a continuous 1-cocycle c' : F → M: lift the values of c on the generators through f, take the cocycle c' with those values, and compare f ∘ c' with c on the generators.

theorem TauCeti.freeProP.explicitCoeff1_surjective {p : ℕ} {X M : Type u} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] [DistribMulAction (freeProP p X) M] [ContinuousSMul (freeProP p X) M] [CompactSpace M] [TotallyDisconnectedSpace M] (hM : IsProP p (Multiplicative M)) {N : Type u} [AddCommGroup N] [TopologicalSpace N] [IsTopologicalAddGroup N] [DistribMulAction (freeProP p X) N] [ContinuousSMul (freeProP p X) N] [T1Space N] (f : M →+[freeProP p X] N) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : Function.Surjective ⇑(ContCohomology.explicitCoeff1 (freeProP p X) M f hf)

A surjective coefficient map induces a surjection on H¹ of a free pro-p group: the coefficient map H¹(F, M) → H¹(F, N) induced by a continuous surjective equivariant homomorphism f : M →+[F] N is surjective, because it already is on cocycles (TauCeti.freeProP.cocyclesMap1_surjective).