Local conductors

Let K be a nonarchimedean local field with unit filtration U(K,n). The steps U(K,n) form a basis of open neighbourhoods of 1 in Kˣ consisting of subgroups, so every open subgroup of Kˣ contains one of them, and so does the kernel of every continuous character Kˣ → ℂˣ. The least such step is the conductor.

• For a finite separable extension L/K the norm group N_{L/K}(Lˣ) is open, and the conductor exponent c(L/K) is the least n with U(K,n) ⊆ N_{L/K}(Lˣ). The conductor of L/K is the ideal 𝔪_K ^ c(L/K) of 𝒪[K].
• For a continuous character χ : Kˣ → ℂˣ, the character conductor exponent is the least n with U(K,n) ⊆ ker χ. Attainment uses that ℂˣ has no small subgroups: continuity alone does not suffice, as the identity of Kˣ is trivial on no step of the filtration.

Both are attained minima (unitFiltration_conductorExponent_le_normGroup, unitFiltration_characterConductorExp_le_ker), characterized by conductorExponent_le_iff and characterConductorExp_le_iff.

The conductor detects ramification. If L/K is unramified, the norm maps the units of L onto those of K, so the conductor exponent is 0. Conversely, for a finite abelian extension, local reciprocity gives [Kˣ : N_{L/K}(Lˣ)] = [L : K]. If the units of K are norms, the norm group contains every element whose valuation is a multiple of the residue degree f, since the norm of a uniformizer of L has valuation f. Its index is then at most f, so [L : K] = f and L/K is unramified (conductorExponent_eq_zero_iff). The abelian hypothesis cannot be dropped: by norm limitation a nonabelian extension has the norm group of its maximal abelian subextension, which may be unramified while the extension itself is not.

Main definitions

• TauCeti.ClassFieldTheory.conductorExponent K L: the least n with U(K,n) ⊆ N_{L/K}(Lˣ).
• TauCeti.ClassFieldTheory.conductorIdeal K L: the conductor 𝔪_K ^ c(L/K) of L/K.
• TauCeti.ClassFieldTheory.characterConductorExp K χ: the least n with U(K,n) ⊆ ker χ.

Main results

• TauCeti.ClassFieldTheory.conductorExponent_le_iff: c(L/K) ≤ n exactly when U(K,n) ⊆ N_{L/K}(Lˣ).
• TauCeti.ClassFieldTheory.conductorExponent_eq_zero_of_isUnramified: an unramified extension has conductor exponent 0.
• TauCeti.ClassFieldTheory.conductorExponent_eq_zero_iff: a finite abelian extension has conductor exponent 0 exactly when it is unramified.
• TauCeti.ClassFieldTheory.characterConductorExp_le_iff: the character conductor exponent of χ is at most n exactly when χ is trivial on U(K,n).

References

• J.-P. Serre, Local Fields, Chapter XV, §2.
• J. Neukirch, Algebraic Number Theory, Chapter V, §1.

The conductor of a finite extension

noncomputable def TauCeti.ClassFieldTheory.conductorExponent (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : ℕ

The conductor exponent of a finite separable extension L/K of a nonarchimedean local field: the least n such that the step U(K,n) of the unit filtration consists of norms from L. Such an n exists because the norm group is open (exists_unitFiltration_le_normGroup), so the minimum is attained (unitFiltration_conductorExponent_le_normGroup).

noncomputable def TauCeti.ClassFieldTheory.conductorIdeal (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : Ideal ↥(ValuativeRel.valuation K).integer

The conductor of a finite separable extension L/K of a nonarchimedean local field: the ideal 𝔪_K ^ c(L/K) of 𝒪[K], where c(L/K) is the conductor exponent.

theorem TauCeti.ClassFieldTheory.conductorIdeal_def (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : conductorIdeal K L = IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ conductorExponent K L

The conductor is the power of the maximal ideal given by the conductor exponent.

@[simp]

theorem TauCeti.ClassFieldTheory.conductorIdeal_eq_top_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : conductorIdeal K L = ⊤ ↔ conductorExponent K L = 0

The conductor is the unit ideal exactly when the conductor exponent is 0.

theorem TauCeti.ClassFieldTheory.unitFiltration_conductorExponent_le_normGroup (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] : unitFiltration K (conductorExponent K L) ≤ normGroup K L

The conductor exponent is attained: U(K, c(L/K)) consists of norms from L.

theorem TauCeti.ClassFieldTheory.conductorExponent_le_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] {n : ℕ} : conductorExponent K L ≤ n ↔ unitFiltration K n ≤ normGroup K L

The characterizing property of the conductor exponent: c(L/K) ≤ n exactly when every element of U(K,n) is a norm from L.

Ramification and the conductor

theorem TauCeti.ClassFieldTheory.conductorExponent_eq_zero_of_isUnramified (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_2) [Field L] [Algebra K L] [FiniteDimensional K L] [Algebra.IsSeparable K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [ValuativeExtension K L] [IsUnramified K L] : conductorExponent K L = 0

An unramified extension has conductor exponent 0: its norm maps the units of L onto the units of K.

The unramified criterion for abelian extensions

theorem TauCeti.ClassFieldTheory.isUnramified_of_conductorExponent_eq_zero (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [ValuativeExtension K L] [IsAbelianGalois K L] (h : conductorExponent K L = 0) : IsUnramified K L

A finite abelian extension with conductor exponent 0 is unramified.

@[simp]

theorem TauCeti.ClassFieldTheory.conductorExponent_eq_zero_iff (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : Type u_1) [Field L] [Algebra K L] [FiniteDimensional K L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [ValuativeExtension K L] [IsAbelianGalois K L] : conductorExponent K L = 0 ↔ IsUnramified K L

The unramified criterion for the conductor: a finite abelian extension of nonarchimedean local fields has conductor exponent 0, that is, every unit of K is a norm, exactly when it is unramified.

The conductor of a character

theorem TauCeti.ClassFieldTheory.exists_unitFiltration_le_ker (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Kˣ →ₜ* ℂˣ) : ∃ (n : ℕ), unitFiltration K n ≤ χ.ker

A continuous character Kˣ → ℂˣ is trivial on a step of the unit filtration: the steps are arbitrarily small subgroups, and ℂˣ has no small subgroups.

noncomputable def TauCeti.ClassFieldTheory.characterConductorExp (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Kˣ →ₜ* ℂˣ) : ℕ

The conductor exponent of a continuous character χ : Kˣ → ℂˣ: the least n such that χ is trivial on the step U(K,n) of the unit filtration. The minimum is attained (unitFiltration_characterConductorExp_le_ker).

theorem TauCeti.ClassFieldTheory.unitFiltration_characterConductorExp_le_ker (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Kˣ →ₜ* ℂˣ) : unitFiltration K (characterConductorExp K χ) ≤ χ.ker

The character conductor exponent is attained: χ is trivial on U(K, characterConductorExp K χ).

theorem TauCeti.ClassFieldTheory.characterConductorExp_le_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Kˣ →ₜ* ℂˣ) {n : ℕ} : characterConductorExp K χ ≤ n ↔ unitFiltration K n ≤ χ.ker

The characterizing property of the character conductor exponent: it is at most n exactly when χ is trivial on U(K,n).

@[simp]

theorem TauCeti.ClassFieldTheory.characterConductorExp_eq_zero_iff (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (χ : Kˣ →ₜ* ℂˣ) : characterConductorExp K χ = 0 ↔ unitFiltration K 0 ≤ χ.ker

A continuous character has conductor exponent 0 exactly when it is unramified, that is, trivial on the units U(K,0) of 𝒪[K].