The free quotient of the p-adic completion of units

For a finite extension L of ℚ_[p], the p-adic completion A(L) = lim_m Lˣ/(Lˣ)^(p^m) of TauCeti.padicCompletionUnits is, modulo its ℤ_p-torsion, a free ℤ_p-module of rank [L : ℚ_p] + 1. The [L : ℚ_p] comes from the principal units and the 1 from the valuation. Together with the computation of the torsion (TauCeti.torsion_padicCompletionUnits), this determines A(L) as a ℤ_p-module.

The free part is exhibited by an explicit lattice of finite index. Choose a depth i beyond the convergence radius of the logarithm, so that the exponential identifies the additive group 𝓂[L] ^ i with the deep units U(L,i) (TauCeti.deepUnitExpLogEquiv). Let b be a basis of the ring of integers 𝒪[L] over that of ℚ_[p], which is ℤ_[p]. The classes in A(L) of p and of the deep units exp (p ^ i * b_k) define a ℤ_p-linear map ℤ_p ^ ([L : ℚ_p] + 1) → A(L), using that the class of exp (c • x) is c times the class of exp x for c ∈ ℤ_p. This map is injective: a relation in A(L) is, at each finite level, an equation p ^ a * exp x = y ^ (p ^ m) in Lˣ, and a fixed power y ^ M lies in U(L,i) · p ^ ℤ (TauCeti.exists_forall_pow_eq_mem_unitFiltration_mul_zpow), so comparing valuations and logarithms forces the coefficients to be divisible by arbitrarily large powers of p. Conversely, the same power M times p ^ i carries the class of every unit, hence all of A(L), into its image. The algebraic conclusion is TauCeti.nonempty_quotient_torsion_linearEquiv_of_injective_of_smul_mem_range.

Main results

• TauCeti.padicCompletionUnits_quotient_torsion_linearEquiv: for a finite extension L of ℚ_[p], A(L) modulo its ℤ_p-torsion is ℤ_p-linearly isomorphic to ℤ_p ^ ([L : ℚ_p] + 1).
• TauCeti.finrank_padicCompletionUnits: consequently A(L) has ℤ_p-rank [L : ℚ_p] + 1.
• TauCeti.linearIndependent_padicCompletionUnitsOf: the classes in A(L) of p and of deep units whose logarithms are linearly independent over ℚ_p are linearly independent over ℤ_p.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (5.7).
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, §VII.4.

The deep exponential, read in A(L)

Relations at a finite level

The lattice map

Deep units with independent logarithms

theorem TauCeti.linearIndependent_padicCompletionUnitsOf (p : ℕ) [Fact (Nat.Prime p)] {L : Type u_1} [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [FinitePadicExtension L p] {i : ℕ} (hi : absoluteRamificationIndex L p < (p - 1) * i) {ι : Type u_2} [Finite ι] {u : ι → Lˣ} (hu : ∀ (j : ι), u j ∈ unitFiltration L i) (hlog : LinearIndependent ℚ_[p] fun (j : ι) => NormedSpace.log ↑(u j)) {ϖ : Lˣ} (hϖ : ↑ϖ = ↑p) : LinearIndependent ℤ_[p] fun (o : Option ι) => Additive.ofMul ((padicCompletionUnitsOf p L) (o.elim ϖ u))

Deep units with independent logarithms are independent in A(L). Let u be a finite family of deep units of L, in U(L,i) with e(L/ℚ_p) < (p - 1) * i, whose logarithms are linearly independent over ℚ_p. Then the classes in A(L) of p and of the u j are linearly independent over ℤ_p.

theorem TauCeti.padicCompletionUnits_quotient_torsion_linearEquiv (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_2) [Field L] [Algebra ℚ_[p] L] [Module.Finite ℚ_[p] L] : Nonempty ((Additive ↥(padicCompletionUnits p L) ⧸ Submodule.torsion ℤ_[p] (Additive ↥(padicCompletionUnits p L))) ≃ₗ[ℤ_[p]] Fin (Module.finrank ℚ_[p] L + 1) → ℤ_[p])

The free quotient of A(L). For a finite extension L of ℚ_[p], the p-adic completion A(L) = lim_m Lˣ/(Lˣ)^(p^m) of its multiplicative group is, modulo its ℤ_p-torsion, a free ℤ_p-module of rank [L : ℚ_p] + 1.

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

The rank of A(L). For a finite extension L of ℚ_[p], the completed multiplicative module A(L) has ℤ_p-rank [L : ℚ_p] + 1: its torsion does not contribute to the rank, and its free quotient has that rank.