Existence of the Tate module of a finite layer

Let L/K be a finite Galois extension of p-adic fields. The Tate module of the layer (TauCeti.LayerTateModule) exists: it is the splitting module of the class u of the class module, carried to A(L) along local reciprocity. Tate's hypotheses for u on the p-subgroups of Gal(L/K) are NSW (3.6.4) at G_K, whose input is scd_p G_K = 2 (TauCeti.isZero_groupCohomology_one_res_padicCompletionUnits, TauCeti.natCard_groupCohomology_two_res_padicCompletionUnits); the restriction of u generates on each p-subgroup because u has the full p-part of #Gal(L/K) as its order (groupCohomology.zmultiples_map_subtype_eq_top).

Main statements

• TauCeti.nonempty_layerTateModule: the Tate module of a finite Galois layer of p-adic fields exists.

Implementation notes

Local reciprocity and Mathlib's representations are stated for fields in Type. For fields in an arbitrary universe the layer is first moved to its copy Shrink L / Shrink K in Type, and the Tate module of the copy is carried back along the induced isomorphisms of Galois groups and of A(L) (TauCeti.padicCompletionUnitsCongr, TauCeti.LayerTateModule.nonempty_of_equiv).

References

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

theorem TauCeti.nonempty_layerTateModule (p : ℕ) [Fact (Nat.Prime p)] (K L : Type u) [Field L] [Field K] [Algebra K L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] [Algebra ℚ_[p] K] [IsScalarTower ℚ_[p] K L] [IsGalois K L] : Nonempty (LayerTateModule p L K)

Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)). For a finite Galois extension L/K of p-adic fields there is a finitely generated ℤ_p[Gal(L/K)]-module of projective dimension at most one which is an extension of the augmentation ideal by A(L).