Principal units are pro-p

Let K be a nonarchimedean local field with residue characteristic p. This file proves that every positive-depth subgroup U(K,m+1), in particular the group U(K,1) of principal units, is pro-p.

The finite-level input is the unit filtration. Every quotient U(K,m+1) / U(K,m+n+1) has order q ^ n, where q is the cardinality of the residue field (TauCeti.natCard_unitFiltration_succ_quotient_add_succ). Since q is a power of p, these quotients are p-groups. The subgroups U(K,n) form a neighbourhood basis of 1, so every continuous finite quotient of U(K,m+1) is a quotient of one of these finite-level p-groups.

Main results

• TauCeti.isPGroup_unitFiltration_succ_quotient_add_succ: every positive-depth finite-level quotient U(K,m+1) / U(K,m+n+1) is a p-group.
• TauCeti.isProP_unitFiltration_succ: every positive-depth subgroup U(K,m+1) is pro-p.
• TauCeti.unitFiltration_one_isProP: the principal-unit group is pro-p.

References

• J.-P. Serre, Corps Locaux, Chapter II, §5.
• J. Neukirch, Algebraic Number Theory, Chapter II, §5, Proposition 5.3.

theorem TauCeti.isPGroup_unitFiltration_succ_quotient_add_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (m n : ℕ) : IsPGroup p (↥(unitFiltration K (m + 1)) ⧸ (unitFiltration K (m + n + 1)).subgroupOf (unitFiltration K (m + 1)))

Every positive-depth finite-level quotient U(K,m+1) / U(K,m+n+1) is a p-group when p is the residue characteristic. No primality hypothesis is needed: the residue field is finite, so its characteristic is automatically prime.

theorem TauCeti.isProP_unitFiltration_succ {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) [CharP (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) p] (m : ℕ) : IsProP p ↥(unitFiltration K (m + 1))

Every positive-depth unit-filtration subgroup U(K,m+1) of a nonarchimedean local field is pro-p, where p is the characteristic of the residue field. Equivalently, every continuous finite quotient of U(K,m+1) is a p-group. Primality of p need not be assumed: it follows from CharP 𝓀[K] p, since the residue field is finite.

theorem TauCeti.unitFiltration_one_isProP {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (p : ℕ) (hp : ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) = p) : IsProP p ↥(unitFiltration K 1)

The principal units of a nonarchimedean local field are pro-p. Here p is the characteristic of the residue field. Equivalently, every continuous finite quotient of U(K,1) is a p-group. This is the depth-one case of isProP_unitFiltration_succ.