Level-constant classes in H¹(χ) count K^×/(K^×)ᵖ
ProvedgroupCohomology.natCard_continuousClasses_ofChar_eq_natCard_units_quotLet be fields with Galois, let be a prime, write for the group of -algebra automorphisms of , and let be a group homomorphism. Here ofChar χ denotes the one-dimensional representation of over given by , i.e. the trivial representation on twisted by . Assume given , a primitive -th root of unity, such that for every , and assume that every acquires a -th root in , i.e. for each there is with . Let adm be a -submodule of whose elements are characterised as follows: adm if and only if is the image under the canonical projection H1π of some -cocycle for which there exists an intermediate field of , finite-dimensional over , with for all and all in the fixing subgroup of . Then the cardinality of adm equals the cardinality of modulo the image of the -th power homomorphism powMonoidHom p on , both computed as Nat.card (so the common value is if either side is infinite).
This is Kummer theory in the form adapted to the full (possibly infinite) Galois group: the subgroup of classes in represented by a cocycle constant on cosets of for some finite subextension — the classes of finite level — is in bijection with . It is used in the computation of the local terms entering the dual Selmer group estimate, being cited in the specialisation of this count to the cyclotomic character at a prime.
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.natCard_continuousClasses_ofChar_eq_natCard_units_quot
{K L : Type} [Field K] [Field L] [Algebra K L] [IsGalois 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)
(hroots : ∀ a : Kˣ, ∃ α : Lˣ, algebraMap K L (a : K) = (α : L) ^ p)
(adm : Submodule (ZMod p) (H1 (ofChar χ)))
(hadm : ∀ x, x ∈ adm ↔ ∃ c : cocycles₁ (ofChar χ),
(∃ E : IntermediateField K L, FiniteDimensional K E ∧
∀ g s : L ≃ₐ[K] L, s ∈ E.fixingSubgroup → c.val (g * s) = c.val g) ∧ (H1π _).hom c = x) :
Nat.card adm = Nat.card (Kˣ ⧸ (powMonoidHom p : Kˣ →* Kˣ).range) := by sorry