Topology of the p-adic completion of a local multiplicative group

For a mixed-characteristic nonarchimedean local field L, this file proves that padicCompletionUnits p L is a profinite pro-p group. Its topology is the subspace topology from the product of the finite discrete power-class groups. The canonical map from Lˣ has dense range: a compatible family can be matched on any finite collection of coordinates by a representative of its largest coordinate.

Main results

• TauCeti.padicCompletionUnitsCompactSpace: A(L) is compact.
• TauCeti.isProP_padicCompletionUnits: A(L) is pro-p.
• TauCeti.continuous_padicCompletionUnitsAut: field automorphisms act continuously on A(L).
• TauCeti.padicCompletionUnitsContinuousSMul: the intrinsic ℤ_p-action is jointly continuous.
• TauCeti.denseRange_padicCompletionUnitsOf: Lˣ is dense in A(L).

instance TauCeti.padicCompletionUnitsContinuousSMul (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] : ContinuousSMul ℤ_[p] (Additive ↥(padicCompletionUnits p L))

The intrinsic ℤ_p-module action on the completed multiplicative group is jointly continuous: at level m it depends only on the scalar modulo p^m and the level-m coordinate. The local-field hypotheses make the power-class groups discrete in their quotient topology.

theorem TauCeti.continuous_padicCompletionUnitsAut (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] (K : Type u_2) [Field K] [Algebra K L] (σ : Gal(L/K)) : Continuous ⇑((padicCompletionUnitsAut p L K) σ)

The coordinatewise action of a field automorphism on the multiplicative p-adic completion is continuous.

instance TauCeti.padicCompletionUnitsCompactSpace (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] : CompactSpace ↥(padicCompletionUnits p L)

The completed multiplicative group of a mixed-characteristic local field is compact, as a closed subset of a product of finite discrete groups.

theorem TauCeti.isProP_padicCompletionUnits (p : ℕ) [Fact (Nat.Prime p)] (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [CharZero L] : IsProP p ↥(padicCompletionUnits p L)

The completed multiplicative group of a mixed-characteristic local field is pro-p: each power-class group Lˣ/(Lˣ)^(p^m) is a p-group.

theorem TauCeti.denseRange_padicCompletionUnitsOf (p : ℕ) (L : Type u_1) [Field L] [TopologicalSpace L] : DenseRange ⇑(padicCompletionUnitsOf p L)

The canonical map Lˣ → A(L) has dense range.