Base change and composita of unramified extensions of local fields

This file proves that unramifiedness of extensions of nonarchimedean local fields is stable under base change and under composita. Let L/K be unramified, and let M/F/K be a tower in which M is generated over F by the image of a K-embedding ι : L →ₐ[K] M. Then M/F is unramified. Combined with transitivity in towers, this shows that the compositum, inside any extension M of K, of two unramified extensions of K is unramified over K. These are the facts that make the unramified subextensions of an algebraic closure a directed family, whose union is the maximal unramified extension.

Both results rest on the criterion by generators of TauCeti.NumberTheory.LocalField.Unramified.Criterion: an unramified L/K is generated by an element a of 𝒪[L] at which its minimal polynomial over 𝒪[K] has unit derivative, and the image of a then witnesses the same criterion for M/F.

Main results

• TauCeti.IsUnramified.of_adjoin_range_eq_top: base change; if L/K is unramified and M is generated over F by the image of L, then M/F is unramified.
• TauCeti.IsUnramified.of_fieldRange_sup_fieldRange_eq_top: composita; if M is the compositum of the images of two unramified extensions of K, then M/K is unramified.
• TauCeti.IsUnramified.of_algEquiv: a local field K-isomorphic to an unramified extension of K is unramified over K.

References

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

theorem TauCeti.IsUnramified.of_adjoin_range_eq_top {K : Type u_1} {L : Type u_2} {F : Type u_3} {M : Type u_4} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Field F] [ValuativeRel F] [TopologicalSpace F] [IsNonarchimedeanLocalField F] [Algebra K F] [ValuativeExtension K F] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra F M] [ValuativeExtension F M] [Algebra K M] [IsScalarTower K F M] [IsUnramified K L] (ι : L →ₐ[K] M) (h : IntermediateField.adjoin F (Set.range ⇑ι) = ⊤) : IsUnramified F M

Base change of an unramified extension. Let L/K be an unramified extension and M/F/K a tower of nonarchimedean local fields. If M is generated over F by the image of a K-embedding ι : L →ₐ[K] M, then M/F is unramified.

theorem TauCeti.IsUnramified.of_fieldRange_sup_fieldRange_eq_top {K : Type u_1} {L₁ : Type u_2} {L₂ : Type u_3} {M : Type u_4} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L₁] [ValuativeRel L₁] [TopologicalSpace L₁] [IsNonarchimedeanLocalField L₁] [Algebra K L₁] [ValuativeExtension K L₁] [Field L₂] [ValuativeRel L₂] [TopologicalSpace L₂] [IsNonarchimedeanLocalField L₂] [Algebra K L₂] [ValuativeExtension K L₂] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [IsUnramified K L₁] [IsUnramified K L₂] (ι₁ : L₁ →ₐ[K] M) (ι₂ : L₂ →ₐ[K] M) (h : ι₁.fieldRange ⊔ ι₂.fieldRange = ⊤) : IsUnramified K M

The compositum of unramified extensions is unramified. If a finite extension M of a nonarchimedean local field K is the compositum of the images of two K-embeddings of unramified extensions L₁/K and L₂/K, then M/K is unramified.

theorem TauCeti.IsUnramified.of_algEquiv {K : Type u_1} {L₁ : Type u_2} {M : Type u_4} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L₁] [ValuativeRel L₁] [TopologicalSpace L₁] [IsNonarchimedeanLocalField L₁] [Algebra K L₁] [ValuativeExtension K L₁] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [IsUnramified K L₁] (e : L₁ ≃ₐ[K] M) : IsUnramified K M

Unramifiedness is invariant under isomorphism. A nonarchimedean local field which is K-isomorphic to an unramified extension of K is unramified over K.