Reducing the local Euler characteristic formula to prime coefficients

Let F be a finite extension of ℚ_p. Tate's local Euler characteristic formula χ_F(A) = φ_F(A) is stated for every finite smooth discrete A : GalRep n F. This file reduces it to modules with coefficients in a prime field ZMod ℓ, following NSW (7.3.1) and Milne, Arithmetic Duality Theorems, I, Theorem 2.8.

Two observations make the reduction. First, the continuous cohomology of a discrete module does not see its scalars (TauCeti.ContCohomology.ofDiscreteModuleRestrictScalarsIntEquiv), so a module with ZMod n-scalars that a prime ℓ kills has the same local Euler characteristic and order as the same module with ZMod ℓ-scalars. Second, both invariants are multiplicative in short exact sequences (localEulerCharacteristic_mul_of_exact, localCardNorm_mul_of_exact), and a finite module that a prime ℓ dividing its order does not kill sits in the exact sequence 0 → A[ℓ] → A → A / A[ℓ] → 0 with both ends nonzero and so strictly smaller. Induction on the order of A concludes.

Main results

• localEulerCharacteristic_eq_localCardNorm_of_nsmul_eq_zero: the formula for a module killed by a prime ℓ follows from the formula with ZMod ℓ-coefficients.
• localEulerCharacteristic_eq_localCardNorm_of_forall_prime: the formula for every finite smooth discrete module follows from the formula with prime-field coefficients.

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.localEulerCharacteristic_eq_localCardNorm_of_nsmul_eq_zero (p : ℕ) [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] {n ℓ : ℕ} [NeZero n] [Fact (Nat.Prime ℓ)] (h : ∀ (B : GalRep ℓ F) [inst : Finite ↑B] [inst_1 : Fact (IsSmoothDiscrete (ZMod ℓ) B)], localEulerCharacteristic ⋯ B = localCardNorm p B) (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] (hA : ∀ (x : ↑A), ℓ • x = 0) : localEulerCharacteristic ⋯ A = localCardNorm p A

Changing the coefficients to a prime field. Let A : GalRep n F be finite smooth discrete and killed by a prime ℓ. If Tate's formula χ_F = φ_F holds for every finite smooth discrete module with ZMod ℓ-coefficients, it holds for A: reading A with ZMod ℓ-scalars changes neither its order nor its continuous cohomology groups as abelian groups.

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_forall_prime (p : ℕ) [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] (h : ∀ (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)] (B : GalRep ℓ F) [inst_1 : Finite ↑B] [inst_2 : Fact (IsSmoothDiscrete (ZMod ℓ) B)], localEulerCharacteristic ⋯ B = localCardNorm p B) (n : ℕ) [NeZero n] (A : GalRep n F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod n) A)] : localEulerCharacteristic ⋯ A = localCardNorm p A

Reduction of Tate's local Euler characteristic formula to prime coefficients. If χ_F = φ_F holds for every finite smooth discrete module with coefficients in a prime field, it holds for every finite smooth discrete A : GalRep n F.