Existence and uniqueness of unramified extensions

Let K be a nonarchimedean local field with residue field of cardinality q, and let Ω be an extension of K. For f ≥ 1 this file defines

TauCeti.unramifiedExtension K Ω f,

the intermediate field of Ω / K generated by the roots of X^{q^f} − X, equivalently by the (q^f − 1)-st roots of unity of Ω. It is finite and Galois over K. When Ω contains a primitive (q^f − 1)-st root of unity ζ, for instance when Ω is separably closed, it is K(ζ), the splitting field of X^{q^f} − X, and it is unramified of degree f over K.

Every unramified intermediate field E of Ω / K is unramifiedExtension K Ω [E : K], for an arbitrary extension Ω. So when Ω is separably closed, such as AlgebraicClosure K, unramifiedExtension K Ω f is the only unramified intermediate field of Ω / K of degree f. These are the finite levels of the maximal unramified extension of K.

The local-field structure carried by an intermediate field is not unique as data, but any two structures compatible with K agree (TauCeti.finiteExtensionValuativeRel_eq). The theorems below are therefore stated for an arbitrary compatible structure, and TauCeti.existsUnique_isUnramified_finrank_eq packages the statement for the canonical structure of TauCeti.finiteIntermediateFieldValuativeRel.

Main definitions

• TauCeti.unramifiedExtension K Ω f: the intermediate field generated by the roots of X^{q^f} − X in Ω.

Main results

• TauCeti.unramifiedExtension_eq_adjoin_setOf_pow_eq_one: for f ≠ 0 it is generated by the (q^f − 1)-st roots of unity of Ω.
• TauCeti.unramifiedExtension_eq_adjoin_simple: it is K(ζ) for any primitive (q^f − 1)-st root of unity ζ of Ω.
• TauCeti.unramifiedExtension_le_of_dvd: it contains the unramified extension of degree d for every d ∣ f, when f ≠ 0.
• TauCeti.map_unramifiedExtension_le: an embedding carries an unramified extension into the unramified extension of the same degree in the target.
• TauCeti.unramifiedExtension_le_restrictScalars_unramifiedExtension: for an extension L/K of nonarchimedean local fields inside Ω, it lies in the unramified extension of L of degree f.
• TauCeti.isGalois_unramifiedExtension: it is Galois over K.
• TauCeti.isUnramified_unramifiedExtension_of_isPrimitiveRoot, TauCeti.isUnramified_unramifiedExtension: it is unramified over K.
• TauCeti.finrank_unramifiedExtension_of_isPrimitiveRoot, TauCeti.finrank_unramifiedExtension: it has degree f over K.
• IntermediateField.eq_unramifiedExtension_finrank: every unramified intermediate field E of Ω / K is unramifiedExtension K Ω [E : K].
• TauCeti.existsUnique_isUnramified_finrank_eq: for f ≥ 1, there is exactly one unramified intermediate field of Ω / K of degree f.

References

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

def TauCeti.unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : IntermediateField K Ω

The unramified extension of degree f of a nonarchimedean local field K inside an extension Ω: the intermediate field generated by the roots of X^{q^f} − X, where q is the cardinality of the residue field of K. When Ω is separably closed and f ≥ 1 it is the unique unramified intermediate field of Ω / K of degree f.

Equations

• TauCeti.unramifiedExtension K Ω f = IntermediateField.adjoin K ((Polynomial.X ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - Polynomial.X).rootSet Ω)

theorem TauCeti.unramifiedExtension_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : unramifiedExtension K Ω f = IntermediateField.adjoin K ((Polynomial.X ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - Polynomial.X).rootSet Ω)

The unramified extension of degree f is the intermediate field generated by the roots of X^{q^f} − X.

@[simp]

theorem TauCeti.rootSet_subset_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : (Polynomial.X ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - Polynomial.X).rootSet Ω ⊆ ↑(unramifiedExtension K Ω f)

Every root of X^{q^f} − X in Ω lies in the unramified extension of degree f.

@[simp]

theorem TauCeti.unramifiedExtension_le_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f : ℕ} {E : IntermediateField K Ω} : unramifiedExtension K Ω f ≤ E ↔ (Polynomial.X ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - Polynomial.X).rootSet Ω ⊆ ↑E

The unramified extension of degree f is the least intermediate field of Ω / K containing the roots of X^{q^f} − X.

@[simp]

theorem TauCeti.unramifiedExtension_zero (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : unramifiedExtension K Ω 0 = ⊥

The unramified extension of degree 0 is K: the polynomial X^{q^0} − X is zero.

theorem TauCeti.unramifiedExtension_le_of_dvd {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f g : ℕ} (hg : g ≠ 0) (h : f ∣ g) : unramifiedExtension K Ω f ≤ unramifiedExtension K Ω g

The unramified extension of degree f lies in that of degree g when f ∣ g and g ≠ 0: a root of X^{q^f} − X is a root of X^{q^g} − X.

theorem TauCeti.map_unramifiedExtension_le {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {E : Type u_3} [Field E] [Algebra K E] (f : ℕ) (ι : Ω →ₐ[K] E) : IntermediateField.map ι (unramifiedExtension K Ω f) ≤ unramifiedExtension K E f

An embedding of extensions of K carries the unramified extension of degree f into the unramified extension of degree f in the target. Equality need not hold, since the target may contain roots of X ^ q ^ f - X that are absent from the source.

theorem TauCeti.unramifiedExtension_le_restrictScalars_unramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] (L : Type u_3) [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra L Ω] [IsScalarTower K L Ω] (f : ℕ) : unramifiedExtension K Ω f ≤ IntermediateField.restrictScalars K (unramifiedExtension L Ω f)

Unramified extensions grow with the ground field. For an extension L/K of nonarchimedean local fields inside Ω, the unramified extension of degree f of K lies in that of L: a root of X^{q^f} − X is a root of X^{q'^f} − X, where q' = q^{f(L/K)} is the cardinality of the residue field of L.

theorem TauCeti.unramifiedExtension_eq_adjoin_setOf_pow_eq_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f : ℕ} (hf : f ≠ 0) : unramifiedExtension K Ω f = IntermediateField.adjoin K {x : Ω | x ^ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1) = 1}

The unramified extension of degree f is generated by the (q^f − 1)-st roots of unity of Ω, for f ≠ 0.

theorem TauCeti.unramifiedExtension_eq_adjoin_simple {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f : ℕ} (hf : f ≠ 0) {ζ : Ω} (hζ : IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1)) : unramifiedExtension K Ω f = K⟮ζ⟯

The unramified extension of degree f is generated by a primitive (q^f − 1)-st root of unity.

theorem TauCeti.exists_isPrimitiveRoot_natCard_pow_sub_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} (hf : f ≠ 0) : ∃ (ζ : Ω), IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1)

A separably closed extension of K contains a primitive (q^f − 1)-st root of unity, for f ≠ 0.

instance TauCeti.finiteDimensional_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : FiniteDimensional K ↥(unramifiedExtension K Ω f)

The unramified extension of degree f is a finite extension of K.

instance TauCeti.isGalois_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : IsGalois K ↥(unramifiedExtension K Ω f)

The unramified extension of degree f is Galois over K, for any extension Ω of K. For f = 0 it is K itself.

theorem TauCeti.isUnramified_unramifiedExtension_of_isPrimitiveRoot {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f : ℕ} (hf : f ≠ 0) {ζ : Ω} (hζ : IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1)) [ValuativeRel ↥(unramifiedExtension K Ω f)] [TopologicalSpace ↥(unramifiedExtension K Ω f)] [IsNonarchimedeanLocalField ↥(unramifiedExtension K Ω f)] [ValuativeExtension K ↥(unramifiedExtension K Ω f)] : IsUnramified K ↥(unramifiedExtension K Ω f)

The unramified extension of degree f is unramified when Ω contains a primitive (q^f − 1)-st root of unity. This holds for any structure of nonarchimedean local field on it compatible with K.

theorem TauCeti.finrank_unramifiedExtension_of_isPrimitiveRoot {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {f : ℕ} (hf : f ≠ 0) {ζ : Ω} (hζ : IsPrimitiveRoot ζ (Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - 1)) : Module.finrank K ↥(unramifiedExtension K Ω f) = f

The unramified extension of degree f has degree f when Ω contains a primitive (q^f − 1)-st root of unity.

theorem IntermediateField.eq_unramifiedExtension_finrank {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] (E : IntermediateField K Ω) [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] [TauCeti.IsUnramified K ↥E] : E = TauCeti.unramifiedExtension K Ω (Module.finrank K ↥E)

Uniqueness of unramified extensions. Every unramified intermediate field E of Ω / K is the unramified extension of degree [E : K], the splitting field of X^{q^{[E : K]}} − X. This holds for any extension Ω of K and any structure of nonarchimedean local field on E compatible with K.

instance TauCeti.isSplittingField_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (f : ℕ) : Polynomial.IsSplittingField K (↥(unramifiedExtension K Ω f)) (Polynomial.X ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f - Polynomial.X)

The unramified extension of degree f is a splitting field of X^{q^f} − X over K.

theorem TauCeti.isUnramified_unramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} (hf : f ≠ 0) [ValuativeRel ↥(unramifiedExtension K Ω f)] [TopologicalSpace ↥(unramifiedExtension K Ω f)] [IsNonarchimedeanLocalField ↥(unramifiedExtension K Ω f)] [ValuativeExtension K ↥(unramifiedExtension K Ω f)] : IsUnramified K ↥(unramifiedExtension K Ω f)

The unramified extension of degree f is unramified. This holds for any structure of nonarchimedean local field on it compatible with K.

@[simp]

theorem TauCeti.finrank_unramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} (hf : f ≠ 0) : Module.finrank K ↥(unramifiedExtension K Ω f) = f

The unramified extension of degree f has degree f.

theorem TauCeti.existsUnique_isUnramified_finrank_eq (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} (hf : f ≠ 0) : ∃! E : IntermediateField K Ω, ∃ (x : FiniteDimensional K ↥E), IsUnramified K ↥E ∧ Module.finrank K ↥E = f

Existence and uniqueness of unramified extensions. For f ≥ 1 there is exactly one intermediate field of Ω / K which is unramified of degree f over K, for its canonical structure of nonarchimedean local field; it is TauCeti.unramifiedExtension K Ω f.