The rationalization of the completed multiplicative module

For a finite extension L of ℚ_[p], the completed multiplicative module A(L) = lim_m Lˣ/(Lˣ)^(p^m) of TauCeti.padicCompletionUnits has ℤ_p-rank [L : ℚ_p] + 1 (TauCeti.finrank_padicCompletionUnits), so its rationalization A(L) ⊗[ℤ_p] ℚ_p is a ℚ_p-vector space of dimension [L : ℚ_p] + 1. This file records that dimension and determines the Galois structure of the rationalization.

Over a finite Galois layer L/K of p-adic fields with group G = Gal(L/K) and N = [K : ℚ_p], the rationalization is the ℚ_p[G]-module ℚ_p[G]^N ⊕ ℚ_p (NSW (7.4.4)(i)); as a ℤ_p[G]-module it is written (ℤ_p[G]^N × ℤ_p[G] ⧸ I_G) ⊗[ℤ_p] ℚ_p, with the trivial module ℤ_p[G] ⧸ I_G in place of ℚ_p so that no second module structure is installed on ℚ_p (TauCeti.nonempty_padicCompletionUnits_tensorRat_linearEquiv).

The decomposition comes from an integral lattice of full rank. A normal basis σ ↦ σ α of L/K and a ℚ_p-basis b of K give the ℚ_p-basis b_k σ(α) of L; choose deep units u_k whose logarithms are nonzero ℚ_p-multiples of b_k α. The logarithm commutes with G, so the logarithms of the conjugates σ(u_k) are linearly independent over ℚ_p, and the classes of the σ(u_k) and of p are linearly independent over ℤ_p in A(L) (TauCeti.linearIndependent_padicCompletionUnitsOf). Hence the ℤ_p[G]-linear map ℤ_p[G]^N × ℤ_p[G] ⧸ I_G → A(L) sending the k-th basis vector to the class of u_k and 1 to the class of p, which is fixed by G, is injective. Both sides have ℤ_p-rank N · [L : K] + 1, so it becomes an isomorphism after tensoring with ℚ_p.

The dimension count is also where the Galois hypothesis enters: the right side has dimension N · #G + 1, the left [L : ℚ_p] + 1 = N · [L : K] + 1, and these agree exactly when #Aut_K(L) = [L : K]. So over a layer whose automorphism group is smaller than its degree, no ℤ_p[G]-linear isomorphism between the two sides exists (TauCeti.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv_of_card_lt). Finiteness of Aut_K(L) is therefore not a substitute for L/K being Galois in the decomposition; the non-Galois cubic ℚ₅(∛5) of TauCeti.NonGaloisCubic is an explicit instance.

Main results

• TauCeti.finrank_padicCompletionUnits_tensorRat: A(L) ⊗[ℤ_p] ℚ_p has ℤ_p-rank, hence ℚ_p-dimension, [L : ℚ_p] + 1.
• TauCeti.nonempty_padicCompletionUnits_tensorRat_linearEquiv: the rational decomposition A(L) ⊗ ℚ_p ≃ (ℤ_p[G]^N × ℤ_p[G] ⧸ I_G) ⊗ ℚ_p of ℤ_p[G]-modules over a finite Galois layer L/K of p-adic fields, that is A(L) ⊗ ℚ_p ≃ ℚ_p[G]^N ⊕ ℚ_p.
• TauCeti.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv_of_card_lt: over a finite layer L/K of p-adic fields with #Aut_K(L) < [L : K], A(L) ⊗ ℚ_p is not ℤ_p[Aut_K(L)]-isomorphic to (ℤ_p[Aut_K(L)]^N × ℤ_p[Aut_K(L)] ⧸ I) ⊗ ℚ_p.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (7.4.4) and the proof of (7.4.1).
• K. Iwasawa, On Galois groups of local fields, Trans. Amer. Math. Soc. 80 (1955), 448–469.

theorem TauCeti.finrank_padicCompletionUnits_tensorRat (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] : Module.finrank ℤ_[p] (TensorProduct ℤ_[p] (Additive ↥(padicCompletionUnits p L)) ℚ_[p]) = Module.finrank ℚ_[p] L + 1

The dimension of the rationalization of A(L). For a finite extension L of ℚ_[p], the ℤ_p-rank of A(L) ⊗[ℤ_p] ℚ_p is [L : ℚ_p] + 1. Since ℤ_p acts on this ℚ_p-vector space through ℚ_p, this is also its ℚ_p-dimension.

The rational decomposition

theorem TauCeti.nonempty_padicCompletionUnits_tensorRat_linearEquiv (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] : Nonempty (TensorProduct ℤ_[p] (Additive ↥(padicCompletionUnits p L)) ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] TensorProduct ℤ_[p] ((Fin (Module.finrank ℚ_[p] K) → MonoidAlgebra ℤ_[p] Gal(L/K)) × MonoidAlgebra ℤ_[p] Gal(L/K) ⧸ RingHom.ker (MonoidAlgebra.augmentation ℤ_[p] Gal(L/K))) ℚ_[p])

The rational decomposition of A(L) (NSW (7.4.4)(i)). Let L/K be a finite Galois layer of p-adic fields, with L finite over ℚ_p, group G = Gal(L/K), N = [K : ℚ_p] and augmentation ideal I_G. Then the rationalization A(L) ⊗[ℤ_p] ℚ_p of the completed multiplicative module is isomorphic to (ℤ_p[G]^N × ℤ_p[G] ⧸ I_G) ⊗[ℤ_p] ℚ_p as a left ℤ_p[G]-module, that is, A(L) ⊗ ℚ_p ≃ ℚ_p[G]^N ⊕ ℚ_p: N copies of the regular representation and one trivial representation.

theorem TauCeti.not_nonempty_padicCompletionUnits_tensorRat_linearEquiv_of_card_lt (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] (h : Nat.card Gal(L/K) < Module.finrank K L) : ¬Nonempty (TensorProduct ℤ_[p] (Additive ↥(padicCompletionUnits p L)) ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] TensorProduct ℤ_[p] ((Fin (Module.finrank ℚ_[p] K) → MonoidAlgebra ℤ_[p] Gal(L/K)) × MonoidAlgebra ℤ_[p] Gal(L/K) ⧸ RingHom.ker (MonoidAlgebra.augmentation ℤ_[p] Gal(L/K))) ℚ_[p])

Rejection test for the Galois hypothesis of the rational decomposition. Let L/K be a finite layer of p-adic fields whose automorphism group Aut_K(L) has fewer elements than the degree [L : K], as happens for a non-Galois layer. Then A(L) ⊗ ℚ_p is not ℤ_p[Aut_K(L)]-isomorphic to (ℤ_p[Aut_K(L)]^N × ℤ_p[Aut_K(L)] ⧸ I) ⊗ ℚ_p, for N = [K : ℚ_p] and I the augmentation ideal: the left side has ℚ_p-dimension [L : ℚ_p] + 1 = N · [L : K] + 1 and the right side N · #Aut_K(L) + 1. So the Galois hypothesis of the decomposition A(L) ⊗ ℚ_p ≃ ℚ_p[Gal(L/K)]^N ⊕ ℚ_p cannot be weakened to finiteness of the automorphism group.