The ring of integers of an extension of local fields is a finite free module

Let L/K be an extension of nonarchimedean local fields whose valuations are compatible, in the sense of ValuativeExtension K L. This file proves that 𝒪[L] is a free 𝒪[K]-module of finite rank [L : K], and in particular that L/K is finite: no finiteness of L/K is assumed anywhere below. This is the basic structural fact about integers in local field extensions: it makes 𝒪[L] a lattice in the K-vector space L, so that ramification index and inertia degree can be read off from 𝒪[L] / 𝓂[K] 𝒪[L], whose 𝓀[K]-dimension is [L : K], leading to the formula e * f = [L : K]. It also identifies L as the fraction field of 𝒪[L] obtained by inverting only the nonzero elements of 𝒪[K].

Main results

• TauCeti.integerRingHasFiniteQuotients: 𝒪[K] has finite quotients by nonzero ideals.
• TauCeti.subsingleton_torsionBy_integerRing, TauCeti.finite_quotSMulTop_integerRing: for n ≠ 0 in K, 𝒪[K] has no n-torsion and 𝒪[K] ⧸ n𝒪[K] is finite.
• TauCeti.integerRingModuleFinite: 𝒪[L] is a finite 𝒪[K]-module.
• TauCeti.integerRingModuleFree: 𝒪[L] is a free 𝒪[K]-module.
• TauCeti.isLocalization_integerRing: L is the localization of 𝒪[L] at the image of the nonzero elements of 𝒪[K].
• TauCeti.finrank_integerRing: the rank of 𝒪[L] over 𝒪[K] is [L : K].
• TauCeti.finite_of_valuativeExtension: L is a finite extension of K.

References

• J.-P. Serre, Corps Locaux, Chapter I, §4, Proposition 10, and Chapter II, §2.
• J. Neukirch, Algebraic Number Theory, Chapter II, §6.

instance TauCeti.integerRingHasFiniteQuotients (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Ring.HasFiniteQuotients ↥(ValuativeRel.valuation K).integer

The ring of integers of a nonarchimedean local field has finite quotients: a nonzero ideal of the discrete valuation ring 𝒪[K] contains a power of 𝓂[K], and the residue field of K is finite.

instance TauCeti.subsingleton_torsionBy_integerRing {K : Type u_1} [Field K] [ValuativeRel K] (n : ℕ) [NeZero ↑n] : Subsingleton ↥(Submodule.torsionBy ℤ ↥(ValuativeRel.valuation K).integer ↑n)

𝒪[K] has no n-torsion when n ≠ 0 in K.

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

When n ≠ 0 in K, the reduction 𝒪[K] ⧸ n𝒪[K] is finite.

theorem TauCeti.finite_quotient_maximalIdeal_smul_integerRing (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Finite (↥(ValuativeRel.valuation L).integer ⧸ IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer • ⊤)

The reduction 𝒪[L] / 𝓂[K] 𝒪[L] is finite: 𝓂[K] 𝒪[L] is a nonzero ideal of 𝒪[L], which has finite quotients.

instance TauCeti.integerRingModuleFinite (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.Finite ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

The ring of integers of an extension of nonarchimedean local fields is a finite module over the ring of integers of the base.

instance TauCeti.integerRingModuleFree (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.Free ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer

The ring of integers of an extension of nonarchimedean local fields is a free module over the ring of integers of the base: it is finite and torsion-free over the principal ideal domain 𝒪[K].

theorem TauCeti.exists_algebraMap_mul_mem_integerRing (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] (x : L) : ∃ (a : ↥(ValuativeRel.valuation K).integer), a ≠ 0 ∧ (algebraMap K L) ↑a * x ∈ (ValuativeRel.valuation L).integer

Every element of L is carried into 𝒪[L] by a nonzero element of 𝒪[K]: a large enough power of a uniformizer of K will do.

theorem TauCeti.isLocalization_integerRing (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : IsLocalization (Algebra.algebraMapSubmonoid (↥(ValuativeRel.valuation L).integer) (nonZeroDivisors ↥(ValuativeRel.valuation K).integer)) L

L is the localization of 𝒪[L] at the image of the nonzero elements of 𝒪[K].

theorem TauCeti.finrank_integerRing (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.finrank ↥(ValuativeRel.valuation K).integer ↥(ValuativeRel.valuation L).integer = Module.finrank K L

The rank of 𝒪[L] as a free 𝒪[K]-module is the degree [L : K].

theorem TauCeti.finite_of_valuativeExtension (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] : Module.Finite K L

An extension of nonarchimedean local fields with compatible valuations is finite.