The maximal unramified subextension of a finite extension of local fields

Let L/K be a finite extension of nonarchimedean local fields with compatible valuations, with q = #𝓀[K], e = e(L/K) and f = f(L/K). The residue field of L has q^f elements, so L contains a primitive (q^f − 1)-st root of unity, and the intermediate field L₀ = TauCeti.unramifiedExtension K L f generated by the roots of X^{q^f} − X is unramified of degree f over K. It is the maximal unramified subextension of L/K: every unramified intermediate field lies in it, and L/L₀ is totally ramified of degree e. This factors an arbitrary finite extension L/K as a totally ramified extension of an unramified one, which is how results about totally ramified extensions, such as the Eisenstein description of the ring of integers, extend to all finite extensions.

The statements about an intermediate field E of L/K hold for any structure of nonarchimedean local field on E compatible with K; L is then a valuative extension of E by the instance IntermediateField.valuativeExtension_of_isNonarchimedeanLocalField.

Main results

• TauCeti.exists_isPrimitiveRoot_natCard_pow_inertiaDegree_sub_one: L contains a primitive (q^f − 1)-st root of unity.
• TauCeti.finrank_unramifiedExtension_inertiaDegree and TauCeti.isUnramified_unramifiedExtension_inertiaDegree: L₀/K is unramified of degree f.
• TauCeti.le_unramifiedExtension_inertiaDegree_of_isUnramified: every unramified intermediate field of L/K lies in L₀.
• TauCeti.eq_unramifiedExtension_inertiaDegree_iff: L₀ is the unique intermediate field which is unramified over K and over which L is totally ramified.
• TauCeti.IsUnramified.unramifiedExtension_inertiaDegree_eq_top: L₀ = L when L/K is unramified.
• TauCeti.isTotallyRamified_unramifiedExtension_inertiaDegree, TauCeti.ramificationIndex_unramifiedExtension_inertiaDegree and TauCeti.finrank_unramifiedExtension_inertiaDegree_eq_ramificationIndex: L/L₀ is totally ramified, with ramification index and degree e.
• TauCeti.map_unramifiedExtension_inertiaDegree_le: maximal unramified subextensions are covariant in towers.
• TauCeti.map_unramifiedExtension_inertiaDegree_eq_iff: the maximal unramified subextension is unchanged in a tower exactly when the top step is totally ramified.

References

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

theorem TauCeti.exists_isPrimitiveRoot_natCard_pow_inertiaDegree_sub_one (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] : ∃ (ζ : L), IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ inertiaDegree K L - 1)

L contains a primitive (q^f − 1)-st root of unity, where q = #𝓀[K] and f = f(L/K): its residue field has q^f elements.

@[simp]

theorem TauCeti.finrank_unramifiedExtension_inertiaDegree (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 K ↥(unramifiedExtension K L (inertiaDegree K L)) = inertiaDegree K L

The maximal unramified subextension has degree f. The intermediate field of L/K generated by the roots of X^{q^f} − X, for f = f(L/K), has degree f over K.

theorem TauCeti.isUnramified_unramifiedExtension_inertiaDegree (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] [ValuativeRel ↥(unramifiedExtension K L (inertiaDegree K L))] [TopologicalSpace ↥(unramifiedExtension K L (inertiaDegree K L))] [IsNonarchimedeanLocalField ↥(unramifiedExtension K L (inertiaDegree K L))] [ValuativeExtension K ↥(unramifiedExtension K L (inertiaDegree K L))] : IsUnramified K ↥(unramifiedExtension K L (inertiaDegree K L))

The maximal unramified subextension is unramified. The intermediate field of L/K generated by the roots of X^{q^f} − X, for f = f(L/K), is unramified over K, for any structure of nonarchimedean local field on it compatible with K.

theorem TauCeti.le_unramifiedExtension_inertiaDegree_of_isUnramified {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] (E : IntermediateField K L) [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] [IsUnramified K ↥E] : E ≤ unramifiedExtension K L (inertiaDegree K L)

Maximality. Every unramified intermediate field of L/K, for any structure of nonarchimedean local field on it compatible with K, lies in the unramified extension of degree f(L/K) inside L.

@[simp]

theorem TauCeti.finrank_unramifiedExtension_inertiaDegree_eq_ramificationIndex (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 (↥(unramifiedExtension K L (inertiaDegree K L))) L = ramificationIndex K L

The top step of the factorization has degree e. The degree of L over the unramified extension of degree f(L/K) inside L is the ramification index e(L/K).

theorem TauCeti.isTotallyRamified_unramifiedExtension_inertiaDegree (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] [ValuativeRel ↥(unramifiedExtension K L (inertiaDegree K L))] [TopologicalSpace ↥(unramifiedExtension K L (inertiaDegree K L))] [IsNonarchimedeanLocalField ↥(unramifiedExtension K L (inertiaDegree K L))] [ValuativeExtension K ↥(unramifiedExtension K L (inertiaDegree K L))] : IsTotallyRamified (↥(unramifiedExtension K L (inertiaDegree K L))) L

The top step of the factorization is totally ramified. L is totally ramified over the unramified extension of degree f(L/K) inside L, for any structure of nonarchimedean local field on the latter compatible with K.

@[simp]

theorem TauCeti.ramificationIndex_unramifiedExtension_inertiaDegree (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] [ValuativeRel ↥(unramifiedExtension K L (inertiaDegree K L))] [TopologicalSpace ↥(unramifiedExtension K L (inertiaDegree K L))] [IsNonarchimedeanLocalField ↥(unramifiedExtension K L (inertiaDegree K L))] [ValuativeExtension K ↥(unramifiedExtension K L (inertiaDegree K L))] : ramificationIndex (↥(unramifiedExtension K L (inertiaDegree K L))) L = ramificationIndex K L

The top step of the factorization has ramification index e. The ramification index of L over the unramified extension of degree f(L/K) inside L is e(L/K).

theorem TauCeti.eq_unramifiedExtension_inertiaDegree_iff {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] (E : IntermediateField K L) [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] : E = unramifiedExtension K L (inertiaDegree K L) ↔ IsUnramified K ↥E ∧ IsTotallyRamified (↥E) L

Uniqueness of the unramified--totally ramified factorization. An intermediate field E is the maximal unramified subextension of L/K exactly when E/K is unramified and L/E is totally ramified.

theorem TauCeti.IsUnramified.unramifiedExtension_inertiaDegree_eq_top (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] [IsUnramified K L] : unramifiedExtension K L (inertiaDegree K L) = ⊤

An unramified extension is its own maximal unramified subextension. If L/K is unramified, then L is generated over K by the roots of X^{q^f} − X, for f = f(L/K).

theorem TauCeti.map_unramifiedExtension_inertiaDegree_le (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] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] [ValuativeExtension K M] : IntermediateField.map (IsScalarTower.toAlgHom K L M) (unramifiedExtension K L (inertiaDegree K L)) ≤ unramifiedExtension K M (inertiaDegree K M)

Maximal unramified subextensions are covariant in towers. The image in M of the maximal unramified subextension of L/K lies in the maximal unramified subextension of M/K.

theorem TauCeti.map_unramifiedExtension_inertiaDegree_eq_iff (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] (M : Type u_3) [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] [ValuativeExtension L M] [ValuativeExtension K M] : IntermediateField.map (IsScalarTower.toAlgHom K L M) (unramifiedExtension K L (inertiaDegree K L)) = unramifiedExtension K M (inertiaDegree K M) ↔ IsTotallyRamified L M

Tower compatibility of the unramified--totally ramified factorization. The maximal unramified subextension is unchanged in a tower M/L/K exactly when the top step M/L is totally ramified.