Openness of power subgroups of a local field

When the image of a natural number n in a nonarchimedean local field K is nonzero, the n-th powers in Kˣ contain an open deep-unit subgroup. This applies to every nonzero n in mixed characteristic and to exponents prime to the characteristic in equal characteristic. The resulting openness and closedness, and the criterion for a subgroup of finite exponent, are used when passing from finite quotients of Kˣ to continuous characters.

The deep-unit power identity used here is unitFiltration_le_range_powMonoidHom; its proof uses the binomial expansion and completeness of K.

References

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

theorem TauCeti.isOpen_range_powMonoidHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ↑n ≠ 0) : IsOpen ↑(powMonoidHom n).range

The subgroup of n-th powers of a nonarchimedean local field is open whenever (n : K) ≠ 0.

theorem TauCeti.isClosed_range_powMonoidHom {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ↑n ≠ 0) : IsClosed ↑(powMonoidHom n).range

The subgroup of n-th powers is closed whenever (n : K) ≠ 0.

theorem TauCeti.discreteTopology_localSquareClasses (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) : DiscreteTopology (Kˣ ⧸ Subgroup.square Kˣ)

When two is nonzero, the local square-class quotient is discrete, since the squares are open. This theorem applies to the literal quotient, with its quotient topology.

theorem TauCeti.isOpen_of_natCast_exponent_ne_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {H : Subgroup Kˣ} (hH : ↑(Monoid.exponent (Kˣ ⧸ H)) ≠ 0) : IsOpen ↑H

A subgroup of Kˣ is open if the exponent of its quotient is nonzero in K.

theorem TauCeti.isOpen_of_natCast_index_ne_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {H : Subgroup Kˣ} (hH : ↑H.index ≠ 0) : IsOpen ↑H

A subgroup of Kˣ is open if its index is nonzero in K.