H² of an inflated representation by duality

Let F be a nonarchimedean local field, V an open normal subgroup of G_F with finite quotient G = G_F ⧸ V, and ℓ a prime invertible in F. Suppose that V acts trivially on μ_ℓ, so that μ_ℓ is the inflation of a representation M of G. For a finite-dimensional representation A of G over 𝔽_ℓ, inflated to G_F by fdGalRepOfQuotient, this file computes H²(F, A) in terms of the representation theory of the finite group G:

#H²(F, A) = #H⁰(F, Hom(A, μ_ℓ)) = #Hom_{G_F}(A, μ_ℓ) = #Hom_G(A, M),
dim H²(F, A) = dim Hom_G(A, M) = dim Hom_G(M, A) = dim (M^∨ ⊗ A)^G  (ℓ ∤ #G).

The first line is local Tate duality in degrees (0, 2) and the invariants of the Tate dual (natCard_continuousCohomology_two_eq_natCard_hom), followed by the full faithfulness of inflation. In the second line, ℓ ∤ #G makes 𝔽_ℓ[G] semisimple, and the intertwiners in the two directions are then equally many (FDRep.finrank_hom_comm); the intertwiners M → A are the invariants of M^∨ ⊗ A (FDRep.finrank_invariants_dual_tprod).

Such an M exists as soon as V acts trivially on μ_ℓ (exists_fdGalRepOfQuotient_iso_muNRep). In the dévissage proving Tate's local Euler characteristic formula, once the modular Artin theorem has reduced to ℓ ∤ #G and μ_ℓ has been adjoined to the fixed field of V, this expresses dim H² through the invariants of a tensor product with μ_ℓ^{-1}, the form in which dim H¹ is also computed.

Main results

• TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_fdGalRepOfQuotient: #H²(F, A) = #Hom_G(A, M), for every n invertible in F.
• TauCeti.ClassFieldTheory.finrank_continuousCohomology_two_fdGalRepOfQuotient: dim H²(F, A) = dim (M^∨ ⊗ A)^G for a prime ℓ not dividing #G.

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.

theorem TauCeti.ClassFieldTheory.natCard_continuousCohomology_two_fdGalRepOfQuotient {n : ℕ} {F : Type} [Field F] {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] (hn : IsUnit ↑n) {M : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} (e : (fdGalRepOfQuotient n F V).obj M ≅ muNRep n F) (A : FDRep (ZMod n) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : Nat.card ↑(continuousCohomology 2 ((fdGalRepOfQuotient n F V).obj A)).toModuleCat = Nat.card (A ⟶ M)

#H²(F, A) = #Hom_G(A, μₙ) for an inflated representation. Let n be invertible in F and M a representation of G = G_F ⧸ V inflating to μₙ. For every finite-dimensional representation A of G, the order of H²(F, A) is the number of intertwiners A → M: local duality in degrees (0, 2) (natCard_continuousCohomology_two_eq_natCard_hom) counts the G_F-equivariant maps A → μₙ, and inflation, being fully faithful, identifies them with the intertwiners A → M.

theorem TauCeti.ClassFieldTheory.finrank_continuousCohomology_two_fdGalRepOfQuotient {F : Type} [Field F] {V : OpenNormalSubgroup (Field.absoluteGaloisGroup F)} [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hℓ : IsUnit ↑ℓ) (hV : (↑V.toOpenSubgroup).index.Coprime ℓ) {M : FDRep (ZMod ℓ) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)} (e : (fdGalRepOfQuotient ℓ F V).obj M ≅ muNRep ℓ F) (A : FDRep (ZMod ℓ) (Field.absoluteGaloisGroup F ⧸ ↑V.toOpenSubgroup)) : Module.finrank (ZMod ℓ) ↑(continuousCohomology 2 ((fdGalRepOfQuotient ℓ F V).obj A)).toModuleCat = Module.finrank (ZMod ℓ) ↥((Representation.dual M.ρ).tprod A.ρ).invariants

dim H²(F, A) = dim (μ_ℓ^{-1} ⊗ A)^G for an inflated representation. Let ℓ be a prime invertible in F, V an open normal subgroup of G_F of index prime to ℓ, and M a representation of G = G_F ⧸ V inflating to μ_ℓ. For every finite-dimensional representation A of G over 𝔽_ℓ, dim H²(F, A) = dim Hom_G(A, M) (natCard_continuousCohomology_two_fdGalRepOfQuotient), which is dim Hom_G(M, A) because ℓ ∤ #G (FDRep.finrank_hom_comm), that is dim (M^∨ ⊗ A)^G (FDRep.finrank_invariants_dual_tprod).