Tate's local Euler characteristic formula, prime-to-ℓ case

Let F/ℚ_p be finite, ℓ a prime, and A a finite smooth discrete ZMod ℓ-representation of G_F on which an open normal subgroup of index prime to ℓ acts trivially. This file proves Tate's formula χ_F(A) = φ_F(A) for such A (localEulerCharacteristic_eq_localCardNorm_of_index_coprime):

#H⁰(F, A) · #H²(F, A) / #H¹(F, A) = ‖#A‖_F.

This is the case of the formula to which the modular Artin theorem and Shapiro's lemma reduce the general one (localEulerCharacteristic_eq_localCardNorm_of_indFDRep).

Shrink the subgroup to an open normal W that also fixes μ_ℓ, with index still prime to ℓ (exists_openNormalSubgroup_le_muNRep_ρ_eq_self_of_coprime), and write A, and μ_ℓ as M, as inflations of representations of G = G_F ⧸ W. Then, by the coprime index,

• dim H⁰(F, A) = dim Aᴳ (finrank_continuousCohomology_zero_fdGalRepOfQuotient);
• dim H¹(F, A) = dim (H¹(W, 𝔽_ℓ) ⊗ A)ᴳ (finrank_continuousCohomology_one_fdGalRepOfQuotient);
• dim H²(F, A) = dim (M^∨ ⊗ A)ᴳ (finrank_continuousCohomology_two_fdGalRepOfQuotient).

Equivariant Kummer theory computes the middle term at the fixed field L of W: dim (H¹(W, 𝔽_ℓ) ⊗ A)ᴳ = dim (M^∨ ⊗ A)ᴳ + dim Aᴳ + [ℓ = p] [F : ℚ_p] dim A (finrank_invariants_kummerH1FiniteRepresentation_tprod_of_isUnit and finrank_invariants_kummerH1FiniteRepresentation_tprod_of_finitePadicExtension, stated for Gal(L/F) and read here through G ≃* Gal(L/F)). Comparing with ‖ℓ‖_F, which is 1 for ℓ ≠ p and p^{-[F : ℚ_p]} for ℓ = p, gives χ_F(A) = φ_F(A).

Main results

• TauCeti.ClassFieldTheory.finrank_continuousCohomology_zero_fdGalRepOfQuotient: dim H⁰(F, A) = dim Aᴳ for an inflated representation.
• TauCeti.ClassFieldTheory.finrank_continuousCohomology_one_fdGalRepOfQuotient: dim H¹(F, A) = dim (H¹(W, 𝔽_ℓ) ⊗ A)ᴳ for an inflated representation, W of index prime to ℓ.
• TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_index_coprime: χ_F(A) = φ_F(A) when an open normal subgroup of index prime to ℓ acts trivially on A.

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 statement and the outline of its proof are adapted from split 6 of the pull-request split plan in LOOKAHEAD.md on the Tau Ceti lookahead branch lookahead/ClassFieldTheory/euler-characteristic-mixed of roed-math/TauCeti, commit 217e838c7c3ccfe5f1c3874537459b0527c37625.

theorem TauCeti.ClassFieldTheory.instContinuousSMulZMod_tauCeti_1 {n : ℕ} {H : Type u_1} [Monoid H] [TopologicalSpace H] : ContinuousSMul H (ZMod n)

theorem TauCeti.ClassFieldTheory.finrank_continuousCohomology_zero_fdGalRepOfQuotient {F : Type} [Field F] {W : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (A : FDRep (ZMod ℓ) (Field.absoluteGaloisGroup F ⧸ ↑W.toOpenSubgroup)) : Module.finrank (ZMod ℓ) ↑(continuousCohomology 0 ((fdGalRepOfQuotient ℓ F W).obj A)).toModuleCat = Module.finrank (ZMod ℓ) ↥(Representation.invariants A.ρ)

dim H⁰(F, A) = dim Aᴳ for an inflated representation: H⁰ is the module of invariants (ContinuousCohomology.zeroIso), and an element is fixed by G_F exactly when it is fixed by its quotient G = G_F ⧸ W.

theorem TauCeti.ClassFieldTheory.finrank_continuousCohomology_one_fdGalRepOfQuotient {F : Type} [Field F] {W : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hW : (↑W.toOpenSubgroup).index.Coprime ℓ) (A : FDRep (ZMod ℓ) (Field.absoluteGaloisGroup F ⧸ ↑W.toOpenSubgroup)) : Module.finrank (ZMod ℓ) ↑(continuousCohomology 1 ((fdGalRepOfQuotient ℓ F W).obj A)).toModuleCat = Module.finrank (ZMod ℓ) ↥(h1ConjRepresentation.tprod A.ρ).invariants

dim H¹(F, A) = dim (H¹(W, 𝔽_ℓ) ⊗ A)ᴳ for an inflated representation, when the index of W is prime to ℓ: restriction to W identifies H¹(F, A) with the G-invariants of H¹(W, A) = H¹(W, 𝔽_ℓ) ⊗ A (finrank_H1_eq_finrank_representationInvariants), G = G_F ⧸ W acting on H¹(W, 𝔽_ℓ) by conjugation.

theorem TauCeti.ClassFieldTheory.localEulerCharacteristic_eq_localCardNorm_of_index_coprime (p : ℕ) [Fact (Nat.Prime p)] {F : Type} [Field F] [CharZero F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [FinitePadicExtension F p] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (A : GalRep ℓ F) [Finite ↑A] [Fact (IsSmoothDiscrete (ZMod ℓ) A)] (N : OpenNormalSubgroup (Field.absoluteGaloisGroup F)) (hN : (↑N.toOpenSubgroup).index.Coprime ℓ) (hA : ∀ g ∈ N, ∀ (x : ↑A), (A.ρ g) x = x) : localEulerCharacteristic ⋯ A = localCardNorm p A

Tate's local Euler characteristic formula, prime-to-ℓ case. Let F/ℚ_p be finite and ℓ a prime. If an open normal subgroup of G_F of index prime to ℓ acts trivially on a finite smooth discrete ZMod ℓ-representation A, then χ_F(A) = φ_F(A), that is #H⁰(F, A) · #H²(F, A) / #H¹(F, A) = ‖#A‖_F.