Power classes of local units

For a nonarchimedean local field K, the unit group of its integer ring has #μ_n(K) · q ^ v_K(n) classes modulo n-th powers, provided n is nonzero in K. The valuation splitting unitsEquivIntProd separates the factor n in the existing field power-class count card_powerClasses from the contribution of the units.

In particular, away from the residue characteristic the unit power-class count is #μ_n(K), and it is n when K contains the n-th roots of unity. This is the local count used in comparing an S-unit quotient with a product of local unit quotients.

References

• J. S. Milne, Class Field Theory, VII, proof of Lemma 6.9.
• J.-P. Serre, Local Fields, Chapter V, §3.

theorem TauCeti.card_integerUnitPowerClasses {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : ↑n ≠ 0) : Nat.card ((↥(ValuativeRel.valuation K).integer)ˣ ⧸ (powMonoidHom n).range) = Nat.card ↥(rootsOfUnity n K) * Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ natCastValuation K n hn

Power classes of local units. For n nonzero in K, the unit group of the integer ring has #μ_n(K) · q ^ v_K(n) classes modulo n-th powers.

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

For n nonzero in K, the n-th powers of the integer-ring units have finite index.

instance TauCeti.instFiniteIndexRangePowMonoidHomIntegerUnits {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero ↑n] : (powMonoidHom n).range.FiniteIndex

For n nonzero in K, the power-map range on integer-ring units has finite index.

instance TauCeti.finite_powerClassQuotient_integerUnits {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} [NeZero ↑n] : Finite (powerClassQuotient (↥(ValuativeRel.valuation K).integer)ˣ n)

For n nonzero in K, the power-class quotient of the integer-ring units is finite.

theorem TauCeti.card_integerUnitPowerClasses_of_isUnit {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : IsUnit ↑n) : Nat.card ((↥(ValuativeRel.valuation K).integer)ˣ ⧸ (powMonoidHom n).range) = Nat.card ↥(rootsOfUnity n K)

Away from the residue characteristic, the unit group has as many n-th power classes as there are n-th roots of unity in the field.