The integral decomposition of a Tate module of a local field layer

For a finite Galois layer, a Tate module is an extension of the augmentation ideal by the completed multiplicative group, with projective dimension at most one. This file applies the integral decomposition theorem to that bundled data, giving the module decomposition that yields the generator bound in the proof of the full local absolute Galois group rank.

Since a Tate module of every finite Galois layer of p-adic fields exists (TauCeti.nonempty_layerTateModule), the relation-module surjection derived from the decomposition holds on every layer with a generating tame frame, with no module Y as input.

Main results

• TauCeti.LayerTateModule.nonempty_linearEquiv_tameFrameModule_prod: a Tate module of the layer is isomorphic to M₀ ⊕ ℤ_p[G]^N, for M₀ the tame-frame module of a generating pair with sharp exponents and N = [K : ℚ_p].
• TauCeti.exists_relationModule_surjective_of_tameFrame: on a layer whose Galois group G is generated by a pair σ, τ with τ of order prime to p, the relation module of every generating family of G of size N + 2 maps ℤ_p[G]-linearly onto A(L) with kernel isomorphic to ℤ_p[G].

References

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

theorem TauCeti.LayerTateModule.nonempty_linearEquiv_tameFrameModule_prod {p : ℕ} [Fact (Nat.Prime p)] {L K : 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] (Y : LayerTateModule p L K) (h : Finite ↥(pPowerRootsOfUnity p L)) (σ τ : Gal(L/K)) (hgen : Subgroup.closure {σ, τ} = ⊤) (a b : ℕ) (ha : ∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑σ) ζ = ζ ^ a) (hb : ∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑τ) ζ = ζ ^ b) (hcard : Nat.card (MonoidAlgebra ℤ_[p] Gal(L/K) ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b}) = localRootOfUnityOrder p L h) : Nonempty (Y.carrier ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] TameFrameModule ℤ_[p] Gal(L/K) σ τ ↑a ↑b × (Fin (Module.finrank ℚ_[p] K) → MonoidAlgebra ℤ_[p] Gal(L/K)))

The integral decomposition of a Tate module. For a finite Galois extension of p-adic fields L/K, a Tate module of the layer is isomorphic to the tame-frame module of any generating pair with sharp exponents, together with N = [K : ℚ_p] copies of the group algebra.

theorem TauCeti.exists_relationModule_surjective_of_tameFrame {p : ℕ} [Fact (Nat.Prime p)] {L K : 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] (σ τ : Gal(L/K)) (hgen : Subgroup.closure {σ, τ} = ⊤) (hτ : ¬p ∣ orderOf τ) {g : Fin (Module.finrank ℚ_[p] K + 2) → Gal(L/K)} (hg : Subgroup.closure (Set.range g) = ⊤) : ∃ (β : ↥(MonoidAlgebra.relationModule ℤ_[p] Gal(L/K) g) →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Additive ↥(padicCompletionUnits p L)), Function.Surjective ⇑β ∧ Nonempty (↥β.ker ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] MonoidAlgebra ℤ_[p] Gal(L/K))

The relation-module surjection on a tame layer (the first half of the proof of NSW (7.4.1)). Let L/K be a finite Galois extension of p-adic fields with group G, and N = [K : ℚ_p]. Let σ, τ generate G, with the order of τ prime to p. Then for every generating family g of G of size N + 2, the relation module R^ab_{N+2}(p) of g maps ℤ_p[G]-linearly onto the p-adic completion A(L) of Lˣ, with kernel isomorphic to ℤ_p[G].