Principal fractional ideals of a nonarchimedean local field

The fractional ideals of the ring of integers 𝒪[K] of a valued field K that are generated by one element are ordered by the valuation: x 𝒪[K] ≤ y 𝒪[K] exactly when v(x) ≤ v(y). For a nonarchimedean local field, whose ring of integers is a discrete valuation ring, the principal fractional ideal generated by x ≠ 0 is the power 𝓂[K] ^ v_K(x) of the maximal ideal, for the normalized valuation v_K.

Main results

• TauCeti.spanSingleton_le_spanSingleton_iff_valuation_le: inclusion of principal fractional ideals is the order of the valuation.
• Units.spanSingleton_eq_maximalIdeal_zpow: x 𝒪[K] = 𝓂[K] ^ v_K(x).

theorem TauCeti.spanSingleton_le_spanSingleton_iff_valuation_le {K : Type u_1} [Field K] [ValuativeRel K] {x y : K} : (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) x ≤ (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) y ↔ (ValuativeRel.valuation K) x ≤ (ValuativeRel.valuation K) y

Inclusion of principal fractional ideals of the ring of integers of a valued field is the reverse of divisibility, that is, the order of the valuation.

theorem Units.spanSingleton_eq_maximalIdeal_zpow {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (x : Kˣ) : (FractionalIdeal.spanSingleton (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) ↑x = ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ^ Multiplicative.toAdd ((TauCeti.normalizedValuation K) x)

The principal fractional ideal generated by x : Kˣ is 𝓂[K] ^ v_K(x).