The first cohomology of a finite Galois layer through equivariant Kummer theory

Let L/K be a finite Galois extension of nonarchimedean local fields, embedded in Kˢ by σ, let G = Gal(L/K), and let ℓ be a prime invertible in K such that σ(L) contains the ℓth roots of unity μ_ℓ. Equivariant Kummer theory identifies the conjugation representation of G on H¹(Gal(Kˢ/σ(L)), 𝔽_ℓ) with μ_ℓ^∨ ⊗ Lˣ ⧸ (Lˣ)^ℓ. This file computes, for every finite-dimensional representation A of G over 𝔽_ℓ with ℓ ∤ #G,

dim (H¹ ⊗ A)ᴳ = dim (μ_ℓ^∨ ⊗ A)ᴳ + dim Aᴳ + [ℓ = p] [K : ℚ_p] dim A.

The ingredients are:

• σ identifies the ℓ-torsion μ_ℓ(L) of Lˣ with μ_ℓ(Kˢ) as representations of G (TauCeti.torsionByUnitsEquivKummerCoeff);
• the class of Lˣ ⧸ (Lˣ)^ℓ in G₀(𝔽_ℓ[G]) is 1 + [μ_ℓ] + [ℓ = p] [K : ℚ_p] [𝔽_ℓ[G]] (TauCeti.exactK0_powerClassRepresentation_of_isUnit, TauCeti.exactK0_powerClassRepresentation_eq_add_finrank_smul);
• the tensor-invariant count TauCeti.finrankTensorInvariantsK0_dual_mul_one_add_add for the line μ_ℓ.

This is the arithmetic heart of the cyclic prime-to-ℓ case of Tate's local Euler characteristic formula: dim H¹(K, A) = dim (H¹(L, 𝔽_ℓ) ⊗ A)ᴳ, dim H²(K, A) = dim (μ_ℓ^∨ ⊗ A)ᴳ and dim H⁰(K, A) = dim Aᴳ.

Main results

• TauCeti.finrank_invariants_kummerH1FiniteRepresentation_tprod_of_isUnit: the count away from the residue characteristic.
• TauCeti.finrank_invariants_kummerH1FiniteRepresentation_tprod_of_finitePadicExtension: the count at the residue characteristic ℓ = p.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., proof of (7.3.1).
• J. S. Milne, Arithmetic Duality Theorems, 2nd ed., I, proof of Theorem 2.8.

The invariant count

@[instance_reducible]

noncomputable def TauCeti.instDistribMulActionAbsoluteGaloisGroupZMod_1 {K : Type} [Field K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] : DistribMulAction (AbsoluteGaloisGroup K) (ZMod ℓ)

The absolute Galois group acts trivially on the constant coefficient module.

theorem TauCeti.instContinuousSMulAbsoluteGaloisGroupZMod_1 {K : Type} [Field K] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] : ContinuousSMul (AbsoluteGaloisGroup K) (ZMod ℓ)

theorem TauCeti.finrank_invariants_kummerH1FiniteRepresentation_tprod_of_isUnit {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (sigma : L →ₐ[K] SeparableClosure K) {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hN : ∀ g ∈ sigma.fieldRange.fixingSubgroup, ∀ (xi : KummerCoeff K ℓ), g • xi = xi) [NeZero ↑(Nat.card Gal(L/K))] (hℓ : IsUnit ↑ℓ) (A : FDRep (ZMod ℓ) Gal(L/K)) : Module.finrank (ZMod ℓ) ↥((kummerH1FiniteRepresentation sigma ℓ).tprod A.ρ).invariants = Module.finrank (ZMod ℓ) ↥((kummerCoeffFiniteRepresentation sigma ℓ hN).dual.tprod A.ρ).invariants + Module.finrank (ZMod ℓ) ↥(Representation.invariants A.ρ)

The first cohomology of a finite Galois layer, away from the residue characteristic. If ℓ is a unit of 𝒪[L] and σ(L) contains the ℓth roots of unity, then for every finite-dimensional representation A of G = Gal(L/K) over 𝔽_ℓ with ℓ ∤ #G, dim (H¹(Gal(Kˢ/σ(L)), 𝔽_ℓ) ⊗ A)ᴳ = dim (μ_ℓ^∨ ⊗ A)ᴳ + dim Aᴳ.

theorem TauCeti.finrank_invariants_kummerH1FiniteRepresentation_tprod_of_finitePadicExtension {K : Type} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : Type} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (sigma : L →ₐ[K] SeparableClosure K) {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hN : ∀ g ∈ sigma.fieldRange.fixingSubgroup, ∀ (xi : KummerCoeff K ℓ), g • xi = xi) [NeZero ↑(Nat.card Gal(L/K))] [FinitePadicExtension K ℓ] [FinitePadicExtension L ℓ] (A : FDRep (ZMod ℓ) Gal(L/K)) : Module.finrank (ZMod ℓ) ↥((kummerH1FiniteRepresentation sigma ℓ).tprod A.ρ).invariants = Module.finrank (ZMod ℓ) ↥((kummerCoeffFiniteRepresentation sigma ℓ hN).dual.tprod A.ρ).invariants + Module.finrank (ZMod ℓ) ↥(Representation.invariants A.ρ) + Module.finrank ℚ_[ℓ] K * Module.finrank (ZMod ℓ) ↑A.V

The first cohomology of a finite Galois layer, at the residue characteristic. If K and L are finite extensions of ℚ_p and σ(L) contains the pth roots of unity, then for every finite-dimensional representation A of G = Gal(L/K) over 𝔽_p with p ∤ #G, dim (H¹(Gal(Kˢ/σ(L)), 𝔽_p) ⊗ A)ᴳ = dim (μ_p^∨ ⊗ A)ᴳ + dim Aᴳ + [K : ℚ_p] dim A.