Dyadic roots of unity in unramified extensions

An unramified extension of ℚ₂ contains no primitive fourth root of unity. Indeed, if ζ were primitive of order four, then (ζ - 1)² = -2ζ. Roots of unity have normalized valuation zero, whereas unramifiedness makes the normalized valuation of 2 equal to one. Taking valuations in the displayed identity would therefore express 1 as twice an integer.

Consequently the 2-power roots of unity in every finite unramified extension of ℚ₂ are just {1, -1}. This is useful when a concrete unramified field is presented by a polynomial, since it reduces the roots-of-unity computation to proving unramifiedness.

Main result

• TauCeti.localRootOfUnityOrder_two_of_isUnramified: the group of 2-power roots of unity in an unramified extension of ℚ₂ has order two.

References

• J.-P. Serre, Local Fields, Chapter IV, §2.

theorem TauCeti.localRootOfUnityOrder_two_of_isUnramified (L : Type u_1) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra ℚ_[2] L] [ValuativeExtension ℚ_[2] L] [IsUnramified ℚ_[2] L] (h2 : 2 ≠ 0) : localRootOfUnityOrder 2 L ⋯ = 2

The 2-power roots of unity in an unramified extension of ℚ₂ have order two.

A primitive fourth root ζ would give (ζ - 1)² = -2ζ. The left-hand side has even normalized valuation, while the right-hand side has valuation one because roots of unity have valuation zero and the extension is unramified.