Additivity of the local Euler characteristic

This file proves that the three-term local Euler characteristic χ_F is multiplicative in short exact sequences: if 0 → A → B → C → 0 is exact, then χ_F(B) = χ_F(A) χ_F(C). Thus χ_F respects the relations defining the Grothendieck group of finite smooth discrete Galois representations, and by dévissage along a composition series the value of χ_F on any finite representation is the product of its values on the simple constituents. This is the reduction that underlies Tate's local Euler characteristic formula χ_F(A) = [𝒪_F : #A · 𝒪_F]⁻¹.

Main results

• TauCeti.ClassFieldTheory.localEulerCharacteristic_mul_of_exact: multiplicativity in a short exact sequence 0 → A → B → C → 0 with B finite and smooth discrete and C discrete.

References

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

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_mul_of_exact {n : ℕ} {F : Type} [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) {A B C : GalRep n F} [Finite ↑B] [Fact (IsSmoothDiscrete (ZMod n) B)] [DiscreteTopology ↑C] (f : A ⟶ B) (g : B ⟶ C) (hf : Function.Injective ⇑(TopRep.Hom.hom f)) (hfg : Function.Exact ⇑(TopRep.Hom.hom f) ⇑(TopRep.Hom.hom g)) (hg : Function.Surjective ⇑(TopRep.Hom.hom g)) : localEulerCharacteristic ⋯ B = localEulerCharacteristic ⋯ A * localEulerCharacteristic ⋯ C

Additivity of the local Euler characteristic. If 0 → A → B → C → 0 is an exact sequence of representations with B finite and smooth discrete and C discrete, then χ_F(B) = χ_F(A) χ_F(C). Finiteness of A and C and smoothness of A and C follow from the sequence (TauCeti.IsSmoothDiscrete.of_injective, TauCeti.IsSmoothDiscrete.of_surjective). Discreteness of C is assumed: the topology of C is part of its data, and a continuous surjection from a discrete module need not have discrete target.