The maximal unramified extension

Let K be a nonarchimedean local field with residue field of cardinality q, and let Ω be an extension of K. This file defines the maximal unramified extension

TauCeti.maximalUnramifiedExtension K Ω,

the union K^{ur} of the unramified extensions K_f = TauCeti.unramifiedExtension K Ω f of all degrees f. It is Galois over K and generated by the roots of the polynomials X^{q^f} − X. When Ω is separably closed, a finite intermediate field of Ω / K lies in K^{ur} exactly when it is unramified over K.

For Ω separably closed, the arithmetic Frobenius of K^{ur} / K,

TauCeti.maximalUnramifiedFrobenius K Ω : Gal(K^{ur}/K),

is the unique automorphism raising every root of every X^{q^f} − X to the q-th power. It restricts to the arithmetic Frobenius TauCeti.frobeniusAlgEquiv of each K_f, and it is a topological generator of Gal(K^{ur}/K): the subgroup it generates is dense for the Krull topology. These are the inputs for identifying Gal(K^{ur}/K) with the profinite integers, Frobenius corresponding to 1.

Main definitions

• TauCeti.maximalUnramifiedExtension K Ω: the union of the unramified extensions K_f.
• TauCeti.maximalUnramifiedFrobenius K Ω: the arithmetic Frobenius of K^{ur} / K.

Main results

• TauCeti.maximalUnramifiedExtension_eq_adjoin: K^{ur} is generated by the roots of the polynomials X^{q^f} − X for f ≠ 0.
• TauCeti.mem_maximalUnramifiedExtension_of_pow_eq_one: K^{ur} contains the roots of unity of order prime to the residue characteristic.
• TauCeti.mem_maximalUnramifiedExtension_of_pow_eq: for p ∤ m, the m-th roots of a unit of 𝒪[K] are unramified.
• TauCeti.isGalois_maximalUnramifiedExtension: K^{ur} is Galois over K.
• IntermediateField.le_maximalUnramifiedExtension_iff: for Ω separably closed, a finite intermediate field lies in K^{ur} exactly when it is unramified over K.
• TauCeti.maximalUnramifiedFrobenius_apply_of_pow_natCard_pow_eq_self, TauCeti.eq_maximalUnramifiedFrobenius_iff: Frobenius is the unique automorphism raising the roots of the polynomials X^{q^f} − X to the q-th power; its n-th power raises them to the q^n-th power (TauCeti.maximalUnramifiedFrobenius_pow_apply_of_pow_natCard_pow_eq_self).
• TauCeti.coe_maximalUnramifiedFrobenius_apply_of_mem, TauCeti.coe_maximalUnramifiedFrobenius_zpow_apply_of_mem: it and its integral powers restrict to the arithmetic Frobenius of each K_f and its powers.
• TauCeti.fixedField_zpowers_maximalUnramifiedFrobenius, TauCeti.topologicalClosure_zpowers_maximalUnramifiedFrobenius: it is a topological generator of Gal(K^{ur}/K).
• TauCeti.X_pow_sub_C_irreducible_unramifiedExtension, TauCeti.X_pow_sub_C_irreducible_maximalUnramifiedExtension: a uniformizer π of K has no nontrivial root in K^{ur}: for every m ≠ 0, X ^ m − π is irreducible over each K_f when Ω is separably closed, and over K^{ur} when Ω is algebraically closed.

References

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

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

The maximal unramified extension K^{ur} of a nonarchimedean local field K inside an extension Ω: the union of the unramified extensions TauCeti.unramifiedExtension K Ω f of all degrees f. When Ω is separably closed, its finite subextensions are exactly the unramified finite extensions of K inside Ω.

Equations

• TauCeti.maximalUnramifiedExtension K Ω = ⨆ (f : ℕ), TauCeti.unramifiedExtension K Ω f

theorem TauCeti.maximalUnramifiedExtension_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : maximalUnramifiedExtension K Ω = ⨆ (f : ℕ), unramifiedExtension K Ω f

The maximal unramified extension is the union of the unramified extensions of all degrees.

theorem TauCeti.unramifiedExtension_le_maximalUnramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] (f : ℕ) : unramifiedExtension K Ω f ≤ maximalUnramifiedExtension K Ω

The unramified extension of each degree lies in the maximal unramified extension.

@[simp]

theorem TauCeti.maximalUnramifiedExtension_le_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {E : IntermediateField K Ω} : maximalUnramifiedExtension K Ω ≤ E ↔ ∀ (f : ℕ), unramifiedExtension K Ω f ≤ E

The maximal unramified extension is the least intermediate field containing the unramified extensions of all degrees.

@[simp]

theorem TauCeti.mem_maximalUnramifiedExtension_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {x : Ω} : x ∈ maximalUnramifiedExtension K Ω ↔ ∃ (f : ℕ), f ≠ 0 ∧ x ∈ unramifiedExtension K Ω f

An element lies in the maximal unramified extension exactly when it lies in the unramified extension of some degree f ≠ 0.

theorem TauCeti.maximalUnramifiedExtension_eq_adjoin (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : maximalUnramifiedExtension K Ω = IntermediateField.adjoin K {x : Ω | ∃ (f : ℕ), f ≠ 0 ∧ x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ f = x}

The maximal unramified extension is generated by the roots of the polynomials X^{q^f} − X for f ≠ 0, where q is the cardinality of the residue field of K.

theorem TauCeti.mem_maximalUnramifiedExtension_of_pow_eq_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {n : ℕ} (hn : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n) {ζ : Ω} (hζ : ζ ^ n = 1) : ζ ∈ maximalUnramifiedExtension K Ω

Roots of unity of order prime to p are unramified. If the residue characteristic of K does not divide n, every n-th root of unity of Ω lies in the maximal unramified extension, since n divides q ^ φ(n) − 1 for the cardinality q of the residue field.

theorem TauCeti.mem_maximalUnramifiedExtension_of_pow_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {m : ℕ} (hm : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ m) {u : Kˣ} (hu : u ∈ unitFiltration K 0) {x : Ω} (hx : x ^ m = (algebraMap K Ω) ↑u) : x ∈ maximalUnramifiedExtension K Ω

Radicals of units are unramified. If the residue characteristic of K does not divide m, every m-th root in Ω of a unit u of 𝒪[K] lies in the maximal unramified extension: u is a root of unity ζ of order q − 1 times a principal unit v, and v = w ^ m for some w ∈ K, so that x / w is a root of unity of order m (q − 1), prime to the residue characteristic.

instance TauCeti.isGalois_maximalUnramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : IsGalois K ↥(maximalUnramifiedExtension K Ω)

The maximal unramified extension is Galois over K, as a union of Galois extensions.

theorem IntermediateField.le_maximalUnramifiedExtension {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.maximalUnramifiedExtension K Ω

An unramified intermediate field of Ω / K lies in the maximal unramified extension. This holds for any extension Ω of K and any structure of nonarchimedean local field on E compatible with K.

theorem IntermediateField.le_maximalUnramifiedExtension_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : IntermediateField K Ω) [ValuativeRel ↥E] [TopologicalSpace ↥E] [IsNonarchimedeanLocalField ↥E] [ValuativeExtension K ↥E] : E ≤ TauCeti.maximalUnramifiedExtension K Ω ↔ TauCeti.IsUnramified K ↥E

The finite subextensions of the maximal unramified extension are its unramified subextensions. For Ω separably closed, an intermediate field E of Ω / K carrying a structure of nonarchimedean local field compatible with K lies in K^{ur} exactly when it is unramified over K.

The arithmetic Frobenius of K^{ur}

noncomputable def TauCeti.maximalUnramifiedFrobenius (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : Gal(↥(maximalUnramifiedExtension K Ω)/K)

The arithmetic Frobenius of the maximal unramified extension K^{ur} / K, for Ω separably closed: the unique automorphism raising every root of every polynomial X^{q^f} − X, f ≠ 0, to the q-th power, where q is the cardinality of the residue field of K. It restricts to the arithmetic Frobenius TauCeti.frobeniusAlgEquiv of each unramified extension of finite degree.

Equations

• TauCeti.maximalUnramifiedFrobenius K Ω = (TauCeti.maximalUnramifiedFrobeniusAux✝ K Ω).restrictNormal' ↥(TauCeti.maximalUnramifiedExtension K Ω)

theorem TauCeti.maximalUnramifiedFrobenius_apply_of_pow_natCard_pow_eq_self {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {x : ↥(maximalUnramifiedExtension K Ω)} {g : ℕ} (hg : g ≠ 0) (hx : x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ g = x) : (maximalUnramifiedFrobenius K Ω) x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

The equation of Frobenius on K^{ur}. Arithmetic Frobenius raises every root of X^{q^g} − X in K^{ur}, for g ≠ 0, to the q-th power.

theorem TauCeti.maximalUnramifiedFrobenius_pow_apply_of_pow_natCard_pow_eq_self {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {x : ↥(maximalUnramifiedExtension K Ω)} {g : ℕ} (hg : g ≠ 0) (hx : x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ g = x) (n : ℕ) : (maximalUnramifiedFrobenius K Ω ^ n) x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ n

The equation of the powers of Frobenius on K^{ur}. The n-th power of arithmetic Frobenius raises every root of X^{q^g} − X in K^{ur}, for g ≠ 0, to the q^n-th power.

theorem TauCeti.eq_maximalUnramifiedFrobenius_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {σ : Gal(↥(maximalUnramifiedExtension K Ω)/K)} : σ = maximalUnramifiedFrobenius K Ω ↔ ∀ (x : ↥(maximalUnramifiedExtension K Ω)) (g : ℕ), g ≠ 0 → x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ^ g = x → σ x = x ^ Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)

Uniqueness of Frobenius on K^{ur}. An automorphism of K^{ur} / K is the arithmetic Frobenius exactly when it raises every root of every polynomial X^{q^g} − X, g ≠ 0, lying in K^{ur} to the q-th power.

theorem TauCeti.coe_maximalUnramifiedFrobenius_apply_of_mem {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} [ValuativeRel ↥(unramifiedExtension K Ω f)] [TopologicalSpace ↥(unramifiedExtension K Ω f)] [IsNonarchimedeanLocalField ↥(unramifiedExtension K Ω f)] [ValuativeExtension K ↥(unramifiedExtension K Ω f)] [IsUnramified K ↥(unramifiedExtension K Ω f)] {x : Ω} (hx : x ∈ unramifiedExtension K Ω f) : ↑((maximalUnramifiedFrobenius K Ω) ⟨x, ⋯⟩) = ↑(frobeniusAlgEquiv ⟨x, hx⟩)

Compatibility of Frobenius with the finite levels. On the unramified extension K_f of any degree f, the arithmetic Frobenius of K^{ur} acts as the arithmetic Frobenius of K_f / K. This holds for any structure of nonarchimedean local field on K_f compatible with K.

theorem TauCeti.coe_maximalUnramifiedFrobenius_zpow_apply_of_mem {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {f : ℕ} [ValuativeRel ↥(unramifiedExtension K Ω f)] [TopologicalSpace ↥(unramifiedExtension K Ω f)] [IsNonarchimedeanLocalField ↥(unramifiedExtension K Ω f)] [ValuativeExtension K ↥(unramifiedExtension K Ω f)] [IsUnramified K ↥(unramifiedExtension K Ω f)] (n : ℤ) {x : Ω} (hx : x ∈ unramifiedExtension K Ω f) : ↑((maximalUnramifiedFrobenius K Ω ^ n) ⟨x, ⋯⟩) = ↑((frobeniusAlgEquiv ^ n) ⟨x, hx⟩)

Compatibility of the powers of Frobenius with the finite levels. On the unramified extension K_f of any degree f, the n-th power of the arithmetic Frobenius of K^{ur} acts as the n-th power of the arithmetic Frobenius of K_f / K, for every integer n.

theorem TauCeti.fixedField_zpowers_maximalUnramifiedFrobenius {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : IntermediateField.fixedField (Subgroup.zpowers (maximalUnramifiedFrobenius K Ω)) = ⊥

Frobenius generates Gal(K^{ur}/K) topologically, algebraic form. The elements of K^{ur} fixed by the arithmetic Frobenius are those of K.

theorem TauCeti.topologicalClosure_zpowers_maximalUnramifiedFrobenius {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : (Subgroup.zpowers (maximalUnramifiedFrobenius K Ω)).topologicalClosure = ⊤

Frobenius is a topological generator of Gal(K^{ur}/K): the subgroup it generates is dense for the Krull topology.

theorem TauCeti.X_pow_sub_C_irreducible_unramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {π : Kˣ} (hπ : IsUniformizer K π) {m : ℕ} (hm : m ≠ 0) {f : ℕ} (hf : f ≠ 0) : Irreducible (Polynomial.X ^ m - Polynomial.C ((algebraMap K ↥(unramifiedExtension K Ω f)) ↑π))

A uniformizer stays a uniformizer in K_f, so it has no nontrivial root there: for a uniformizer π of K and m ≠ 0, the polynomial X ^ m − π is irreducible over the unramified extension K_f of each degree f ≠ 0.

Radicals of a uniformizer over K^{ur}

theorem TauCeti.X_pow_sub_C_irreducible_maximalUnramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] [IsAlgClosed Ω] {π : Kˣ} (hπ : IsUniformizer K π) {m : ℕ} (hm : m ≠ 0) : Irreducible (Polynomial.X ^ m - Polynomial.C ((algebraMap K ↥(maximalUnramifiedExtension K Ω)) ↑π))

A uniformizer has no nontrivial root in K^{ur}: for a uniformizer π of K and m ≠ 0, the polynomial X ^ m − π is irreducible over the maximal unramified extension. Any factor has its finitely many coefficients in a single K_f, over which X ^ m − π is irreducible. So K^{ur}(π^{1/m}) has degree m over K^{ur}.