The integral decomposition of an extension of the augmentation ideal by A(L)

Let L/K be a finite Galois extension of p-adic fields with group G = Gal(L/K), let N = [K : ℚ_p], and let A(L) = lim_m Lˣ/(Lˣ)^(p^m) be the p-adic completion of Lˣ, a ℤ_p[G]-module. Let Y be a ℤ_p[G]-module of projective dimension at most one which is an extension

0 → A(L) → Y → I_G → 0

of the augmentation ideal I_G of ℤ_p[G] by A(L). The Tate module I_{G_K} / I_{G_L} I_{G_K} of the layer (NSW (5.6.5)) is such a module: its projective dimension is at most one by Tate's theorem for the fundamental class of L/K.

This file proves that every such Y is isomorphic to M₀ ⊕ ℤ_p[G]^N, where M₀ = ℤ_p[G]² / ℤ_p[G]·(σ - a, τ - b) is the tame-frame module of a generating pair σ, τ of G with sharp exponents a, b (TauCeti.exists_tameFrame_exponents). This is the isomorphism (∗∗) in the proof of NSW (7.4.1). It is an integral statement: Y is generated by N + 2 elements, since M₀ is a quotient of ℤ_p[G]², and no such count can be read off the rational representation of Y.

The proof applies the cancellation theory of ℤ_p[G]-modules.

• The p-power torsion of Y is that of A(L), because I_G ⊆ ℤ_p[G] is torsion-free, and this is the p-power torsion of M₀ for sharp exponents (TauCeti.tameFrameModule_torsion_linearEquiv). Both Y and M₀ have projective dimension at most one, so they are stably isomorphic (TauCeti.exists_projective_prod_linearEquiv_of_torsion).
• Rationally, the extensions 0 → A(L) → Y → I_G → 0 and 0 → I_G → ℤ_p[G] → ℤ_p → 0 split (TauCeti.MonoidAlgebra.nonempty_tensor_linearEquiv_prod_of_exact). With the rational decomposition A(L) ⊗ ℚ_p ≃ ℚ_p[G]^N ⊕ ℚ_p (TauCeti.nonempty_padicCompletionUnits_tensorRat_linearEquiv) and M₀ ⊗ ℚ_p ≃ ℚ_p[G] (TauCeti.nonempty_tameFrameModule_tensorRat_linearEquiv), this gives Y ⊗ ℚ_p ≃ (M₀ ⊕ ℤ_p[G]^N) ⊗ ℚ_p.
• A stable isomorphism together with this rational identity is an isomorphism (TauCeti.nonempty_linearEquiv_prod_of_stable).

When σ, τ generate G and τ has order prime to p, sharp exponents exist, and the decomposition makes Y a quotient of ℤ_p[G]^(N + 2) = ℤ_p[G]² ⊕ ℤ_p[G]^N by a copy of ℤ_p[G]. Comparing the induced presentation of I_G with the one by any generating family g of size N + 2 (TauCeti.exists_relationModule_surjective_of_exact), the relation module of g, which is R^ab(p) for the presentation of G on g by Lyndon's theorem, maps onto A(L) with kernel ℤ_p[G]: the integral sequence 0 → ℤ_p[G] → R^ab(p) → A(L) → 0 of the proof of NSW (7.4.1).

Main results

• TauCeti.nonempty_linearEquiv_tameFrameModule_prod: an extension of I_G by A(L) of projective dimension at most one is isomorphic to M₀ ⊕ ℤ_p[G]^N.
• TauCeti.exists_relationModule_surjective_of_tameFrame_of_exact: given such a Y, on a layer with a generating pair σ, τ, τ of order prime to p, the relation module of every generating family of size N + 2 maps onto A(L) with kernel ℤ_p[G].

References

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

theorem TauCeti.nonempty_linearEquiv_tameFrameModule_prod {p : ℕ} [Fact (Nat.Prime p)] {L : Type u_1} [Field L] {K : Type u_2} [Field K] [Algebra K L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] [Algebra ℚ_[p] K] [IsScalarTower ℚ_[p] K L] [IsGalois K L] {Y : Type u_3} {P₀ : Type u_4} {P₁ : Type u_5} [AddCommGroup Y] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) Y] [AddCommGroup P₀] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [Module.Projective (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [AddCommGroup P₁] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] [Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] [Module.Projective (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] {d : P₁ →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] P₀} {ρ : P₀ →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Y} (hdρ : Function.Exact ⇑d ⇑ρ) (hd : Function.Injective ⇑d) (hρ : Function.Surjective ⇑ρ) {ι : Additive ↥(padicCompletionUnits p L) →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Y} {π : Y →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] ↥(RingHom.ker (MonoidAlgebra.augmentation ℤ_[p] Gal(L/K)))} (hιπ : Function.Exact ⇑ι ⇑π) (hι : Function.Injective ⇑ι) (hπ : Function.Surjective ⇑π) (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 ≃ₗ[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 an extension of I_G by A(L) (the isomorphism (∗∗) in the proof of NSW (7.4.1), for the Tate module of a tame layer). Let L/K be a finite Galois extension of p-adic fields with group G, and N = [K : ℚ_p]. Let Y be a ℤ_p[G]-module with a resolution 0 → P₁ → P₀ → Y → 0 by finitely generated projective ℤ_p[G]-modules, which is an extension 0 → A(L) → Y → I_G → 0 of the augmentation ideal by the p-adic completion A(L) of Lˣ. Let σ, τ generate G and let a, b be sharp exponents for them: σ, τ act on the p-power roots of unity of L as the a-th and b-th powers, and ℤ_p[G] ⧸ (σ - a, τ - b) has order q(L). Then Y ≃ M₀ ⊕ ℤ_p[G]^N, for M₀ the tame-frame module of σ, τ, a, b.

theorem TauCeti.exists_relationModule_surjective_of_tameFrame_of_exact {p : ℕ} [Fact (Nat.Prime p)] {L : Type u_1} [Field L] {K : Type u_2} [Field K] [Algebra K L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] [Algebra ℚ_[p] K] [IsScalarTower ℚ_[p] K L] [IsGalois K L] {Y : Type u_3} {P₀ : Type u_4} {P₁ : Type u_5} [AddCommGroup Y] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) Y] [AddCommGroup P₀] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [Module.Projective (MonoidAlgebra ℤ_[p] Gal(L/K)) P₀] [AddCommGroup P₁] [Module (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] [Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] [Module.Projective (MonoidAlgebra ℤ_[p] Gal(L/K)) P₁] {d : P₁ →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] P₀} {ρ : P₀ →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Y} (hdρ : Function.Exact ⇑d ⇑ρ) (hd : Function.Injective ⇑d) (hρ : Function.Surjective ⇑ρ) {ι : Additive ↥(padicCompletionUnits p L) →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] Y} {π : Y →ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] ↥(RingHom.ker (MonoidAlgebra.augmentation ℤ_[p] Gal(L/K)))} (hιπ : Function.Exact ⇑ι ⇑π) (hι : Function.Injective ⇑ι) (hπ : Function.Surjective ⇑π) (h : Finite ↥(pPowerRootsOfUnity p 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 Y be a ℤ_p[G]-module with a resolution 0 → P₁ → P₀ → Y → 0 by finitely generated projective ℤ_p[G]-modules, which is an extension 0 → A(L) → Y → I_G → 0 of the augmentation ideal by the p-adic completion A(L) of Lˣ. 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 of g maps onto A(L) with kernel isomorphic to ℤ_p[G].