Documentation

TauCeti.NumberTheory.LocalField.Unramified.Rigidity

Rigidity of unramified extensions #

Let K be a nonarchimedean local field, let L/K be a finite unramified extension and let M/K be any finite extension. A K-embedding ΞΉ : L β†’ M induces a 𝓀[K]-embedding of residue fields ΞΉ.residueFieldHom : 𝓀[L] β†’ 𝓀[M]. This file proves that reduction is a bijection

(L →ₐ[K] M) ≃ (𝓀[L] →ₐ[𝓀[K]] 𝓀[M]).

So a K-embedding of an unramified extension is determined by its effect on residue fields, and every embedding of residue fields lifts. In particular, when M/K is unramified as well, a chosen 𝓀[K]-isomorphism 𝓀[L] ≃ 𝓀[M] lifts to a unique K-isomorphism L ≃ M. Without fixing the residue isomorphism there is no uniqueness: L has [L : K] automorphisms over K, one above each automorphism of 𝓀[L] over 𝓀[K].

Write q = #𝓀[K] and f = f(L/K). The extension L is generated over K by a primitive (q^f βˆ’ 1)-st root of unity ΞΆ, and q^f βˆ’ 1 is prime to the residue characteristic. Reduction is therefore injective on the (q^f βˆ’ 1)-st roots of unity of π’ͺ[M], and by Hensel's lemma every such root of unity of 𝓀[M] lifts. An embedding ΞΉ is determined by ΞΉ ΞΆ, which is the unique lift of the residue of ΞΉ ΞΆ. Conversely, given a residue embedding Ο†, the lift ΞΎ of the image under Ο† of the residue of ΞΆ is a root of the minimal polynomial g of ΞΆ over π’ͺ[K]: its residue is a root of the reduction of g, and not of the reduction of the cofactor (X^{q^fβˆ’1} βˆ’ 1) / g, because X^{q^fβˆ’1} βˆ’ 1 is separable over 𝓀[M]. So ΞΆ ↦ ΞΎ defines a K-embedding lifting Ο†, since the residue of ΞΆ generates 𝓀[L].

Main definitions #

Main results #

References #

source
theorem TauCeti.IsUnramified.residueFieldHom_bijective {K : Type u_1} {L : Type u_2} {M : Type u_3} [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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsUnramified K L] :
Function.Bijective AlgHom.residueFieldHom

Embeddings of an unramified extension are determined by their residue maps, and every residue map lifts. For L/K unramified, reduction is a bijection from the K-embeddings L β†’ M to the 𝓀[K]-embeddings 𝓀[L] β†’ 𝓀[M].

source
noncomputable def TauCeti.IsUnramified.residueFieldHomEquiv (K : Type u_1) (L : Type u_2) (M : Type u_3) [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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsUnramified K L] :
(L →ₐ[K] M) ≃ (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation L).integer →ₐ[IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer] IsLocalRing.ResidueField β†₯(ValuativeRel.valuation M).integer)

Reduction of embeddings of an unramified extension. For L/K unramified, passing to residue fields is an equivalence between the K-embeddings L β†’ M and the 𝓀[K]-embeddings 𝓀[L] β†’ 𝓀[M].

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.IsUnramified.residueFieldHomEquiv_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsUnramified K L] (ΞΉ : L →ₐ[K] M) :
    (residueFieldHomEquiv K L M) ΞΉ = ΞΉ.residueFieldHom

    The equivalence IsUnramified.residueFieldHomEquiv sends an embedding to the induced embedding of residue fields.

    source
    @[simp]
    theorem TauCeti.IsUnramified.residueFieldHom_residueFieldHomEquiv_symm {K : Type u_1} {L : Type u_2} {M : Type u_3} [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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsUnramified K L] (Ο† : IsLocalRing.ResidueField β†₯(ValuativeRel.valuation L).integer →ₐ[IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer] IsLocalRing.ResidueField β†₯(ValuativeRel.valuation M).integer) :
    ((residueFieldHomEquiv K L M).symm Ο†).residueFieldHom = Ο†

    The inverse of IsUnramified.residueFieldHomEquiv lifts an embedding of residue fields: the lift of Ο† induces Ο† on residue fields.

    source
    theorem TauCeti.IsUnramified.existsUnique_algEquiv_residueFieldHom_eq {K : Type u_1} {L : Type u_2} {M : Type u_3} [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] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsUnramified K L] [IsUnramified K M] (Ο† : IsLocalRing.ResidueField β†₯(ValuativeRel.valuation L).integer ≃ₐ[IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer] IsLocalRing.ResidueField β†₯(ValuativeRel.valuation M).integer) :
    βˆƒ! e : L ≃ₐ[K] M, (↑e).residueFieldHom = ↑φ

    Rigidity of unramified extensions. Let L/K and M/K be finite unramified extensions. Every 𝓀[K]-isomorphism 𝓀[L] ≃ 𝓀[M] of residue fields lifts to a unique K-isomorphism L ≃ M.