The lattice of finite unramified extensions

Let K be a nonarchimedean local field and let Ω be a separably closed extension of K. The finite unramified intermediate fields of Ω / K are classified by their positive degrees: the degree-f field is TauCeti.unramifiedExtension K Ω f, and

unramifiedExtension K Ω f ≤ unramifiedExtension K Ω g ↔ f ∣ g.

Consequently these fields form a lattice: meet corresponds to the greatest common divisor of the degrees, and join corresponds to their least common multiple. This file packages the classification as an equivalence with ℕ+ and equips the finite unramified subextensions with their intrinsic inclusion order and lattice operations.

Main definitions

• TauCeti.FiniteUnramifiedSubextension: a finite unramified intermediate field of a fixed separably closed extension.
• TauCeti.unramifiedExtensionPNat: the finite unramified subextension of a positive degree.
• TauCeti.finiteUnramifiedSubextensionDegreeEquiv: the classification by positive degrees.

Main results

• TauCeti.unramifiedExtension_le_unramifiedExtension_iff: inclusion is divisibility of degrees.
• TauCeti.FiniteUnramifiedSubextension.le_iff_degree_dvd: the order characterization for arbitrary finite unramified subextensions.
• TauCeti.FiniteUnramifiedSubextension.degree_inf and TauCeti.FiniteUnramifiedSubextension.degree_sup: the degrees of meet and join are given by Nat.gcd and Nat.lcm.

References

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

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

The degree-f unramified extension is contained in the degree-g unramified extension exactly when f divides g. Both degrees are required to be positive because the index 0 is reserved for the trivial field, rather than a degree-zero extension.

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

A finite unramified subextension of Ω / K, using the canonical local-field structure on finite intermediate fields. The local-field structures remain named definitions rather than global instances, avoiding instance diamonds on the intermediate-field carrier.

Equations

• TauCeti.IsFiniteUnramifiedSubextension K Ω E = ∃ (hE : Module.Finite K ↥E), TauCeti.IsUnramified K ↥E

theorem TauCeti.isFiniteUnramifiedSubextension_iff_exists_eq_unramifiedExtension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : IntermediateField K Ω) : IsFiniteUnramifiedSubextension K Ω E ↔ ∃ (f : ℕ+), E = unramifiedExtension K Ω ↑f

A finite intermediate field is unramified exactly when it is a canonical unramified extension of some positive degree. The degree, and hence the extension, is unique by unramifiedExtension_le_unramifiedExtension_iff.

@[reducible, inline]

abbrev TauCeti.FiniteUnramifiedSubextension (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] : Type u_2

The type of finite unramified intermediate fields of a fixed separably closed extension.

Equations

• TauCeti.FiniteUnramifiedSubextension K Ω = { E : IntermediateField K Ω // TauCeti.IsFiniteUnramifiedSubextension K Ω E }

theorem TauCeti.FiniteUnramifiedSubextension.ext (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] {E F : FiniteUnramifiedSubextension K Ω} (h : ↑E = ↑F) : E = F

Two finite unramified subextensions are equal when their underlying intermediate fields are equal.

theorem TauCeti.FiniteUnramifiedSubextension.ext_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {Ω : Type u_2} [Field Ω] [Algebra K Ω] {E F : FiniteUnramifiedSubextension K Ω} : E = F ↔ ↑E = ↑F

def TauCeti.unramifiedExtensionPNat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (f : ℕ+) : FiniteUnramifiedSubextension K Ω

The unramified extension attached to a positive integer, regarded as a finite unramified subextension.

Equations

• TauCeti.unramifiedExtensionPNat K Ω f = ⟨TauCeti.unramifiedExtension K Ω ↑f, ⋯⟩

@[simp]

theorem TauCeti.coe_unramifiedExtensionPNat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (f : ℕ+) : ↑(unramifiedExtensionPNat K Ω f) = unramifiedExtension K Ω ↑f

The underlying field of the finite unramified subextension of degree f.

noncomputable def TauCeti.finiteUnramifiedSubextensionDegreeEquiv (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : FiniteUnramifiedSubextension K Ω ≃ ℕ+

The classification of finite unramified subextensions by their positive degrees.

Equations

• TauCeti.finiteUnramifiedSubextensionDegreeEquiv K Ω = (TauCeti.unramifiedExtensionEquivFiniteUnramifiedSubextension✝ K Ω).symm

noncomputable def TauCeti.FiniteUnramifiedSubextension.degree (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : FiniteUnramifiedSubextension K Ω) : ℕ+

The degree of a finite unramified subextension.

Equations

• TauCeti.FiniteUnramifiedSubextension.degree K Ω E = (TauCeti.finiteUnramifiedSubextensionDegreeEquiv K Ω) E

theorem TauCeti.FiniteUnramifiedSubextension.finiteUnramifiedSubextensionDegreeEquiv_apply (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : FiniteUnramifiedSubextension K Ω) : (finiteUnramifiedSubextensionDegreeEquiv K Ω) E = degree K Ω E

The degree classification sends a finite unramified subextension to its degree.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.degree_unramifiedExtensionPNat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (f : ℕ+) : degree K Ω (unramifiedExtensionPNat K Ω f) = f

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.finiteUnramifiedSubextensionDegreeEquiv_symm_apply (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (f : ℕ+) : (finiteUnramifiedSubextensionDegreeEquiv K Ω).symm f = unramifiedExtensionPNat K Ω f

The inverse degree classification sends f to the canonical unramified extension of degree f.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.coe_degree (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : FiniteUnramifiedSubextension K Ω) : ↑(degree K Ω E) = Module.finrank K ↥↑E

The positive degree of a finite unramified subextension is its vector-space dimension over the base field.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.unramifiedExtension_finrank (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E : FiniteUnramifiedSubextension K Ω) : unramifiedExtension K Ω (Module.finrank K ↥↑E) = ↑E

A finite unramified subextension is the canonical unramified extension of its vector-space degree over the base field.

theorem TauCeti.FiniteUnramifiedSubextension.le_iff_degree_dvd (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] {E F : FiniteUnramifiedSubextension K Ω} : E ≤ F ↔ ↑(degree K Ω E) ∣ ↑(degree K Ω F)

Inclusion of finite unramified subextensions is divisibility of their degrees.

@[instance_reducible]

noncomputable instance TauCeti.FiniteUnramifiedSubextension.instLattice (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] : Lattice (FiniteUnramifiedSubextension K Ω)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.degree_inf_pnat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E F : FiniteUnramifiedSubextension K Ω) : degree K Ω (E ⊓ F) = ((↑(degree K Ω E)).gcd ↑(degree K Ω F)).toPNat'

The positive degree of a meet is the positive natural associated to the greatest common divisor of the two degrees. This records the defining meet equation of the lattice instance.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.degree_sup_pnat (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E F : FiniteUnramifiedSubextension K Ω) : degree K Ω (E ⊔ F) = ((↑(degree K Ω E)).lcm ↑(degree K Ω F)).toPNat'

The positive degree of a join is the positive natural associated to the least common multiple of the two degrees. This records the defining join equation of the lattice instance.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.degree_inf (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E F : FiniteUnramifiedSubextension K Ω) : Module.finrank K ↥↑(E ⊓ F) = (Module.finrank K ↥↑E).gcd (Module.finrank K ↥↑F)

The degree of a meet of finite unramified subextensions is the greatest common divisor of the two degrees.

@[simp]

theorem TauCeti.FiniteUnramifiedSubextension.degree_sup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω] [IsSepClosed Ω] (E F : FiniteUnramifiedSubextension K Ω) : Module.finrank K ↥↑(E ⊔ F) = (Module.finrank K ↥↑E).lcm (Module.finrank K ↥↑F)

The degree of a join of finite unramified subextensions is the least common multiple of the two degrees.