Additive coboundaries of 𝔽ₚ(χ) versus μₚ-coboundaries
ProvedgroupCohomology.mem_coboundaries1_ofChar_iff_exists_rootOfUnityLet and be fields with a -algebra, let be a prime, and write for the group of -algebra automorphisms of . Let be a group homomorphism, and let be a primitive -th root of unity such that for every , where denotes the canonical representative of . Let be any function. The assertion is an equivalence: lies in coboundaries₁ (ofChar χ), that is, is a -coboundary for the one-dimensional representation of over obtained by twisting the trivial representation on by (so acts as multiplication by ), if and only if there exists a unit with and for all .
This is the coboundary half of the dictionary between -valued cohomology of the character and multiplicative Kummer-theoretic cocycles in ; together with the corresponding statement for cocycles it matches classes in with classes in . It is used in the counting of continuous classes for ofChar χ and in the bound on the rank of cocycles attached to the cyclotomic character on unit inertia.
import Mathlib import Definitions.Def_DualSelmer_ExtConditions set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false universe u open CategoryTheory groupCohomology
theorem groupCohomology.mem_coboundaries1_ofChar_iff_exists_rootOfUnity
{K L : Type} [Field K] [Field L] [Algebra K L] {p : ℕ} [Fact p.Prime]
(χ : (L ≃ₐ[K] L) →* (ZMod p)ˣ) {ζ : Lˣ} (hζp : IsPrimitiveRoot ζ p)
(hζ : ∀ g : L ≃ₐ[K] L, g • ζ = ζ ^ (χ g : ZMod p).val) (c : (L ≃ₐ[K] L) → ZMod p) :
c ∈ coboundaries₁ (ofChar χ) ↔
∃ η : Lˣ, η ^ p = 1 ∧ ∀ g : L ≃ₐ[K] L, g • η / η = ζ ^ (c g).val := by sorry