The conductor and the upper numbering

Let M/K be a finite abelian extension of nonarchimedean local fields with group G and upper ramification groups G^v. For a natural number v, the step U(K,v) of the unit filtration consists of norms from M exactly when G^v = 1 (unitFiltration_le_normGroup_iff_upperRamificationGroup_eq_bot). Hence the conductor exponent c(M/K), the least n with U(K,n) ⊆ N_{M/K}(Mˣ), is the least n with G^n = 1, and for a homomorphism χ on G the conductor exponent of the fixed field of ker χ is the Artin conductor exponent f(χ), the least n with G^n ⊆ ker χ (conductorExponent_fixedField_ker). This is the dictionary between the conductor of a character of Kˣ cut out by local class field theory and the Artin conductor of the corresponding character of the Galois group. Together with the local conductor–discriminant formula TauCeti.LocalFieldsRamification.finsum_artinConductorExponent_eq_discriminantExponent, it is the local input for expressing a discriminant through the conductors of the cyclic subextensions.

Main results

• TauCeti.ClassFieldTheory.unitFiltration_le_normGroup_iff_upperRamificationGroup_eq_bot: for M/K abelian, U(K,v) ⊆ N_{M/K}(Mˣ) exactly when G^v = 1.
• TauCeti.ClassFieldTheory.conductorExponent_le_iff_upperRamificationGroup_eq_bot: c(M/K) ≤ n exactly when G^n = 1.
• TauCeti.ClassFieldTheory.conductorExponent_fixedField_ker: the conductor exponent of the fixed field of ker χ is the Artin conductor exponent of χ.

References

• J.-P. Serre, Corps Locaux, Chapter V, §6 and Chapter XV, §2.
• J. Neukirch, Algebraic Number Theory, Chapter V, §6 and Chapter VII, §11.

theorem TauCeti.ClassFieldTheory.unitFiltration_le_normGroup_iff_upperRamificationGroup_eq_bot (K M : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsAbelianGalois K M] (v : ℕ) : unitFiltration K v ≤ normGroup K M ↔ LocalFieldsRamification.upperRamificationGroup K M ⟨↑v, ⋯⟩ = ⊥

The conductor in the upper numbering. For a finite abelian extension M/K of nonarchimedean local fields and a natural number v, every element of U(K,v) is a norm from M exactly when the upper ramification group G^v of M/K is trivial.

theorem TauCeti.ClassFieldTheory.conductorExponent_le_iff_upperRamificationGroup_eq_bot (K M : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsAbelianGalois K M] {n : ℕ} : conductorExponent K M ≤ n ↔ LocalFieldsRamification.upperRamificationGroup K M ⟨↑n, ⋯⟩ = ⊥

The conductor exponent of an abelian extension in the upper numbering: c(M/K) ≤ n exactly when the upper ramification group G^n of M/K is trivial. Thus c(M/K) is the least natural number n with G^n = 1.

theorem TauCeti.ClassFieldTheory.conductorExponent_fixedField_ker (K M : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field M] [ValuativeRel M] [TopologicalSpace M] [IsNonarchimedeanLocalField M] [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsAbelianGalois K M] {A : Type u_1} [MulOneClass A] (χ : Gal(M/K) →* A) : conductorExponent K ↥(IntermediateField.fixedField χ.ker) = LocalFieldsRamification.artinConductorExponent K M χ

The conductor of a character is its Artin conductor. For a finite abelian extension M/K of nonarchimedean local fields and a homomorphism χ on Gal(M/K), the conductor exponent of the fixed field of ker χ — the least n such that U(K,n) consists of norms from it — is the Artin conductor exponent f(χ), the least n with G^n ⊆ ker χ.