The low-degree cohomology of A(L)

Let L/K be a finite Galois extension of p-adic fields with group G = Gal(L/K), and let A(L) = lim_m Lˣ/(Lˣ)^(p^m) be the p-adic completion of Lˣ, a ℤ_p-representation of G. Through local reciprocity (TauCeti.padicCompletionUnitsEquivAbelianizationProP), A(L) is the class module V^ab(p) of G_K ⧸ V ≃ G, where V = G_L, equivariantly (TauCeti.padicCompletionUnitsEquivAbelianizationProP_smul). As scd_p G_K = 2 (NSW (7.2.5)), NSW (3.6.4) computes the low-degree cohomology of the class module, and this file reads it on A(L):

• for every subgroup S of G, H¹(S, A(L)) = 0 and H²(S, A(L)) is cyclic of order the p-part of #S; in particular H²(S, A(L)) has order #S when S is a p-group;
• H²(G, A(L)) is cyclic of order the p-part of #G, and one class generates after restriction to every subgroup.

These are the inputs of Tate's theorem for A(L) on the p-subgroups of G.

Main statements

• TauCeti.isZero_groupCohomology_one_res_padicCompletionUnits: H¹(S, A(L)) = 0.
• TauCeti.exists_zmultiples_eq_top_groupCohomology_two_res_padicCompletionUnits: H²(S, A(L)) is cyclic of order p ^ v_p(#S).
• TauCeti.exists_zmultiples_eq_top_restriction_groupCohomology_two_padicCompletionUnits: one class restricts to a generator on every subgroup.
• TauCeti.natCard_groupCohomology_two_res_padicCompletionUnits: #H²(S, A(L)) = #S for a p-subgroup S.
• TauCeti.exists_zmultiples_eq_top_groupCohomology_two_padicCompletionUnits: H²(G, A(L)) is cyclic of order p ^ v_p(#G).

References

• J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (3.6.4) and (7.2.5).

theorem TauCeti.isZero_groupCohomology_one_res_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (S : Subgroup Gal(L/K)) : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype (Rep.of (padicCompletionUnitsRepresentation p L K))) 1)

H¹ of A(L) vanishes on every subgroup (NSW (3.6.4), read through local reciprocity): H¹(S, A(L)) = 0 for every subgroup S of Gal(L/K).

theorem TauCeti.exists_zmultiples_eq_top_groupCohomology_two_res_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [IsGalois K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (S : Subgroup Gal(L/K)) : ∃ (u : ↑(groupCohomology (Rep.res S.subtype (Rep.of (padicCompletionUnitsRepresentation p L K))) 2)), AddSubgroup.zmultiples u = ⊤ ∧ Nat.card ↑(groupCohomology (Rep.res S.subtype (Rep.of (padicCompletionUnitsRepresentation p L K))) 2) = p ^ padicValNat p (Nat.card ↥S)

H² of A(L) on a subgroup is cyclic of order the p-part of the subgroup (NSW (3.6.4), read through local reciprocity): for every subgroup S of Gal(L/K), some class u generates H²(S, A(L)), and this group has order p ^ v_p(#S).

theorem TauCeti.exists_zmultiples_eq_top_restriction_groupCohomology_two_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : ∃ (u : ↑(groupCohomology (Rep.of (padicCompletionUnitsRepresentation p L K)) 2)), ∀ (S : Subgroup Gal(L/K)), AddSubgroup.zmultiples ((CategoryTheory.ConcreteCategory.hom (groupCohomology.map S.subtype (CategoryTheory.CategoryStruct.id (Rep.res S.subtype (Rep.of (padicCompletionUnitsRepresentation p L K)))) 2)) u) = ⊤

One class of A(L) generates after every restriction (NSW (3.6.4)). Unlike choosing separate generators for the subgroups, this supplies the compatible class required by the Tate splitting-module construction. The class is transported from the class module through local reciprocity.

theorem TauCeti.natCard_groupCohomology_two_res_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [IsGalois K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (S : Subgroup Gal(L/K)) (hS : IsPGroup p ↥S) : Nat.card ↑(groupCohomology (Rep.res S.subtype (Rep.of (padicCompletionUnitsRepresentation p L K))) 2) = Nat.card ↥S

H² of A(L) on a p-subgroup has the order of the subgroup (NSW (3.6.4), read through local reciprocity): #H²(S, A(L)) = #S for every p-subgroup S of Gal(L/K).

theorem TauCeti.exists_zmultiples_eq_top_groupCohomology_two_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (K L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [IsGalois K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] [Algebra ℚ_[p] K] [Algebra ℚ_[p] L] [IsScalarTower ℚ_[p] K L] [Module.Finite ℚ_[p] L] [ValuativeExtension ℚ_[p] L] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] : ∃ (u : ↑(groupCohomology (Rep.of (padicCompletionUnitsRepresentation p L K)) 2)), AddSubgroup.zmultiples u = ⊤ ∧ Nat.card ↑(groupCohomology (Rep.of (padicCompletionUnitsRepresentation p L K)) 2) = p ^ padicValNat p (Nat.card Gal(L/K))

H²(Gal(L/K), A(L)) is cyclic of order the p-part of [L : K] (NSW (3.6.4), read through local reciprocity): some class u generates H²(Gal(L/K), A(L)), and this group has order p ^ v_p(#Gal(L/K)). The generator is the image of the class u_{G_K/V}(p) of the class module.