Finite generation of the p-adic completion of units

For a prime p and a field L, the completed multiplicative module A(L) = lim_m Lˣ/(Lˣ)^(p^m) is a finitely generated ℤ_p-module as soon as Lˣ/(Lˣ)^p is finite. In particular, for a nonarchimedean local field L in which p ≠ 0, such as a finite extension of ℚ_p, the module A(L) is finitely generated over ℤ_p, and hence over the group algebra ℤ_p[Gal(L/K)] for any field K below L. This is the finiteness hypothesis under which the integral cancellation theorems for ℤ_p[G]-modules apply to A(L).

Implementation notes

The generators are the classes in A(L) of representatives of Lˣ/(Lˣ)^p. Every unit is, in A(L), a ℤ_p-combination of them plus a p^m-multiple, so every element of A(L) is matched at each level m by some combination. Since the level-m coordinate of a combination depends on the coefficients only modulo p^m, the coefficient vectors matching a given element at level m form a decreasing sequence of nonempty closed subsets of the compact space of coefficient vectors, and a vector in their intersection represents the element exactly.

Main results

• TauCeti.module_finite_padicCompletionUnits_of_finiteIndex: A(L) is a finitely generated ℤ_p-module when (Lˣ)^p has finite index in Lˣ.
• TauCeti.span_range_padicCompletionUnitsOf_eq_top: under the same hypothesis, the classes of the units of L span A(L) over ℤ_p.
• TauCeti.exists_eq_padicCompletionUnitsOf_add_pow_smul: under the same hypothesis, every element of A(L) is the class of a unit plus a p ^ m-multiple, for every m.
• TauCeti.module_finite_padicCompletionUnits_padicInt: A(L) is a finitely generated ℤ_p-module for a nonarchimedean local field L with (p : L) ≠ 0.
• TauCeti.module_finite_padicCompletionUnits_monoidAlgebra_of_finiteIndex: A(L) is a finitely generated ℤ_p[Gal(L/K)]-module when (Lˣ)^p has finite index in Lˣ.
• TauCeti.padicCompletionUnits_module_finite: for a nonarchimedean local field L with (p : L) ≠ 0, A(L) is a finitely generated ℤ_p[Gal(L/K)]-module.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, §VII.4.

theorem TauCeti.module_finite_padicCompletionUnits_of_finiteIndex (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [(powMonoidHom p).range.FiniteIndex] : Module.Finite ℤ_[p] (Additive ↥(padicCompletionUnits p L))

Finite generation of A(L). If the subgroup (Lˣ)^p of p-th powers has finite index in Lˣ, then the p-adic completion A(L) = lim_m Lˣ/(Lˣ)^(p^m) is a finitely generated ℤ_p-module.

theorem TauCeti.span_range_padicCompletionUnitsOf_eq_top (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [(powMonoidHom p).range.FiniteIndex] : Submodule.span ℤ_[p] (Set.range fun (u : Lˣ) => Additive.ofMul ((padicCompletionUnitsOf p L) u)) = ⊤

If (Lˣ)^p has finite index in Lˣ, the classes of the units of L span A(L) as a ℤ_p-module.

theorem TauCeti.exists_eq_padicCompletionUnitsOf_add_pow_smul (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [(powMonoidHom p).range.FiniteIndex] (m : ℕ) (x : Additive ↥(padicCompletionUnits p L)) : ∃ (u : Lˣ) (y : Additive ↥(padicCompletionUnits p L)), x = Additive.ofMul ((padicCompletionUnitsOf p L) u) + ↑p ^ m • y

If (Lˣ)^p has finite index in Lˣ, then for every m each element of A(L) is the class of a unit of L plus a p ^ m-multiple.

theorem TauCeti.module_finite_padicCompletionUnits_monoidAlgebra_of_finiteIndex (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [(powMonoidHom p).range.FiniteIndex] (K : Type u_2) [Field K] [Algebra K L] : Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) (Additive ↥(padicCompletionUnits p L))

When (Lˣ)^p has finite index, A(L) is finite over the group algebra of any field automorphism group Gal(L/K).

theorem TauCeti.module_finite_padicCompletionUnits_padicInt (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (hpL : ↑p ≠ 0) : Module.Finite ℤ_[p] (Additive ↥(padicCompletionUnits p L))

For a nonarchimedean local field L in which p ≠ 0, for instance a finite extension of ℚ_p, the completed multiplicative module A(L) is a finitely generated ℤ_p-module.

theorem TauCeti.padicCompletionUnits_module_finite (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] (hpL : ↑p ≠ 0) (K : Type u_2) [Field K] [Algebra K L] : Module.Finite (MonoidAlgebra ℤ_[p] Gal(L/K)) (Additive ↥(padicCompletionUnits p L))

A(L) is a finitely generated ℤ_p[Gal(L/K)]-module. For a nonarchimedean local field L in which p ≠ 0 and any field K below L, the completed multiplicative module A(L) is finitely generated over the integral group algebra ℤ_p[Gal(L/K)].