Numerical forms of the local Euler characteristic formula

For a finite smooth discrete Galois representation over a finite extension of ℚ_p, the local Euler characteristic and the normalized absolute value of the coefficient order are positive rational numbers. This file converts their equality into the usual cardinality formula

#H¹ = #H⁰ · #H² · p ^ ([F : ℚ_p] v_p(#A)).

For coefficients over 𝔽_p, it also converts that equality into the corresponding formula in dimensions. These results separate the final elementary calculation from the representation- theoretic proof of the equality of the two invariants.

Main results

• natCard_continuousCohomology_one_eq_mul_of_localEulerCharacteristic_eq_localCardNorm: the cardinality formula following from χ_F(A) = φ_F(A).
• finrank_continuousCohomology_one_eq_add_of_localEulerCharacteristic_eq_localCardNorm: its 𝔽_p-dimension form, dim H¹ = dim H⁰ + dim H² + [F : ℚ_p] dim A.

References

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

theorem TauCeti.ClassFieldTheory.natCard_continuousCohomology_one_eq_mul_of_localEulerCharacteristic_eq_localCardNorm (p : ℕ) [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (n : ℕ) [NeZero n] (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (h : localEulerCharacteristic ⋯ A = localCardNorm p 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))

The cardinality form of the local Euler characteristic formula. Equality of the local Euler characteristic and the normalized absolute value of the coefficient order implies #H¹ = #H⁰ · #H² · p ^ ([F : ℚ_p] v_p(#A)).

theorem TauCeti.ClassFieldTheory.finrank_continuousCohomology_one_eq_add_of_localEulerCharacteristic_eq_localCardNorm (p : ℕ) [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (A : GalRep p F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod p) A)] (h : localEulerCharacteristic ⋯ A = localCardNorm 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

The 𝔽_p-dimension form of the local Euler characteristic formula. Equality of the local Euler characteristic and the normalized absolute value of the coefficient order implies dim H¹ = dim H⁰ + dim H² + [F : ℚ_p] dim A.