Tate's local Euler characteristic formula

For a finite smooth discrete Galois module over a finite compatible extension F of ℚ_p, Tate's formula identifies the local Euler characteristic with the normalized absolute value of the coefficient order. Its cardinality form is #H¹ = #H⁰ · #H² · p ^ ([F : ℚ_p] v_p(#A)); for 𝔽_p coefficients this becomes dim H¹ = dim H⁰ + dim H² + [F : ℚ_p] dim A.

The formula follows by dévissage to prime coefficients and modular Artin induction, followed by Shapiro's lemma and the formula for a quotient of order prime to the coefficient prime.

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, second edition, (7.3.1)–(7.3.4).
• J. S. Milne, Arithmetic Duality Theorems, second edition, I, Theorem 2.8.

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm (p : ℕ) [Fact (Nat.Prime p)] (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (n : ℕ) [NeZero n] (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] : localEulerCharacteristic ⋯ A = localCardNorm p A

Tate's local Euler characteristic formula. The Euler characteristic of a finite smooth discrete Galois module equals the normalized absolute value of its order.

theorem TauCeti.ClassFieldTheory.eulerCharacteristic_mixed (p : ℕ) [Fact (Nat.Prime p)] (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (n : ℕ) (hn : n ≠ 0) (A : GalRep n F) (hA : Finite ↑A) [Fact (IsSmoothDiscrete (ZMod n) A)] : Nat.card ↑(continuousCohomology 1 A).toModuleCat = Nat.card ↑(continuousCohomology 0 A).toModuleCat * Nat.card ↑(continuousCohomology 2 A).toModuleCat * p ^ (Module.finrank ℚ_[p] F * padicValNat p (Nat.card ↑A))

Cardinality form of Tate's local Euler characteristic formula. For a finite smooth discrete module, #H¹ = #H⁰ · #H² · p ^ ([F : ℚ_p] v_p(#A)).

theorem TauCeti.ClassFieldTheory.eulerCharacteristic_finrank_fp (p : ℕ) [Fact (Nat.Prime p)] (F : Type) [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (A : GalRep p F) (hA : Finite ↑A) [Fact (IsSmoothDiscrete (ZMod p) A)] : Module.finrank (ZMod p) ↑(continuousCohomology 1 A).toModuleCat = Module.finrank (ZMod p) ↑(continuousCohomology 0 A).toModuleCat + Module.finrank (ZMod p) ↑(continuousCohomology 2 A).toModuleCat + Module.finrank ℚ_[p] F * Module.finrank (ZMod p) ↑A

Dimension form of Tate's local Euler characteristic formula. For a finite smooth discrete 𝔽_p-module, dim H¹ = dim H⁰ + dim H² + [F : ℚ_p] dim A.