Documentation

TauCeti.NumberTheory.LocalField.MassFormula.Basic

The totally ramified extensions of given degree and their wild exponents #

Let K be a nonarchimedean local field with residue field 𝓀[K]. Serre's mass formula counts the totally ramified extensions of K of degree n inside a fixed separable closure, each weighted by q ^ (-c(L)), where q = Nat.card 𝓀[K], d(L) is the discriminant exponent of L / K and c(L) = d(L) - n + 1 is its wild exponent. This file sets up the objects being counted.

A subextension L of SeparableClosure K carries no topology or valuation of its own. When L / K is finite, the structures finiteIntermediateFieldValuativeRel and finiteIntermediateFieldTopology make it a nonarchimedean local field extending K, and IsTotallyRamified and discriminantExponent apply. The two wrappers below install these structures and extend total ramification and the discriminant exponent to arbitrary subextensions, taking junk values (False and 0) when L / K is infinite; the comparison theorems IntermediateField.isTotallyRamified_iff and IntermediateField.discriminantExponent_eq identify them with the canonical invariants on finite subextensions. The wrappers and the wild exponent live in the IntermediateField namespace, so that they are available as L.IsTotallyRamified, L.discriminantExponent and L.wildExponent.

Working inside SeparableClosure K matters in equal characteristic p: it excludes inseparable extensions such as those generated by a root of X ^ p - Ο€.

Main definitions #

Main results #

References #

source
def IntermediateField.IsTotallyRamified {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) :
Prop

A subextension L of SeparableClosure K is totally ramified over K when it is finite over K and, with the local-field structure finiteIntermediateFieldValuativeRel and finiteIntermediateFieldTopology, it satisfies IsTotallyRamified K L. For L infinite over K this is False.

Instances For
    source
    theorem IntermediateField.isTotallyRamified_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) [hfin : Module.Finite K β†₯L] :
    L.IsTotallyRamified ↔ TauCeti.IsTotallyRamified K β†₯L

    On a finite subextension, IntermediateField.IsTotallyRamified is IsTotallyRamified for the local-field structure finiteIntermediateFieldValuativeRel and finiteIntermediateFieldTopology.

    source
    theorem IntermediateField.IsTotallyRamified.finite {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : IntermediateField K (SeparableClosure K)} (h : L.IsTotallyRamified) :
    Module.Finite K β†₯L

    A totally ramified subextension is finite over K.

    source
    def TauCeti.totallyRamifiedOfDegree (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : β„•) :
    Set (IntermediateField K (SeparableClosure K))

    Serre's Οƒ_K(n): the subextensions of SeparableClosure K that are totally ramified of degree n over K.

    Instances For
      source
      @[simp]
      theorem TauCeti.mem_totallyRamifiedOfDegree_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} :
      L ∈ totallyRamifiedOfDegree K n ↔ Module.finrank K β†₯L = n ∧ L.IsTotallyRamified

      Membership in Οƒ_K(n): degree n and totally ramified over K.

      source
      @[simp]
      theorem TauCeti.totallyRamifiedOfDegree_zero {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
      totallyRamifiedOfDegree K 0 = βˆ…

      Οƒ_K(0) is empty: a finite extension has positive degree.

      source
      @[simp]
      theorem TauCeti.totallyRamifiedOfDegree_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
      totallyRamifiedOfDegree K 1 = {βŠ₯}

      Οƒ_K(1) = {K}: the only subextension of degree one is the bottom one, and it is totally ramified.

      source
      theorem TauCeti.eq_one_of_mem_totallyRamifiedOfDegree_of_le_maximalUnramifiedExtension {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ totallyRamifiedOfDegree K n) (hle : L ≀ maximalUnramifiedExtension K (SeparableClosure K)) :
      n = 1

      An unramified member of Οƒ_K(n) has degree one. A member of Οƒ_K(n) contained in the maximal unramified extension of K is both unramified and totally ramified over K, so its degree n is its ramification index 1.

      source
      noncomputable def IntermediateField.discriminantExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) :
      β„•

      The discriminant exponent d(L) of a subextension L of SeparableClosure K: for L / K finite, discriminantExponent K L for the local-field structure finiteIntermediateFieldValuativeRel and finiteIntermediateFieldTopology; for L / K infinite, the junk value 0.

      Instances For
        source
        theorem IntermediateField.discriminantExponent_eq {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) [hfin : Module.Finite K β†₯L] :
        L.discriminantExponent = TauCeti.discriminantExponent K β†₯L

        On a finite subextension, IntermediateField.discriminantExponent is discriminantExponent for the local-field structure finiteIntermediateFieldValuativeRel and finiteIntermediateFieldTopology.

        source
        theorem IntermediateField.discriminantExponent_of_not_finite {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L : IntermediateField K (SeparableClosure K)} (h : Β¬Module.Finite K β†₯L) :
        L.discriminantExponent = 0

        On an infinite subextension, IntermediateField.discriminantExponent takes the junk value 0.

        source
        noncomputable def IntermediateField.wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) :
        β„•

        The wild exponent c(L) = d(L) - [L : K] + 1 of a subextension L of SeparableClosure K, written d(L) + 1 - [L : K] in truncated subtraction. For L ∈ Οƒ_K(n) the truncation is faithful by IntermediateField.sub_one_le_discriminantExponent, and c(L) is Serre's nonnegative integer d(L) - n + 1.

        Instances For
          source
          theorem IntermediateField.wildExponent_def {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) :
          L.wildExponent = L.discriminantExponent + 1 - Module.finrank K β†₯L

          The defining equation of wildExponent, valid for every subextension: c(L) is d(L) + 1 - [L : K] in truncated subtraction.

          source
          theorem IntermediateField.sub_one_le_discriminantExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) :
          n - 1 ≀ L.discriminantExponent

          The discriminant bound for Οƒ_K(n): the discriminant exponent of a totally ramified extension of degree n is at least n - 1. This is ramificationIndex_sub_one_le_discriminantExponent with e(L / K) = n.

          source
          theorem IntermediateField.natCast_wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) :
          ↑L.wildExponent = ↑L.discriminantExponent - ↑n + 1

          For L ∈ Οƒ_K(n), the wild exponent is d(L) - n + 1 in β„€.

          source
          theorem IntermediateField.wildExponent_add_eq_discriminantExponent_add_one {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) :
          L.wildExponent + n = L.discriminantExponent + 1

          For L ∈ Οƒ_K(n), c(L) + n = d(L) + 1 in β„•, so the weight q ^ (-(d(L) + 1)) factors as q ^ (-n) Β· q ^ (-c(L)).

          source
          theorem IntermediateField.wildExponent_eq_zero_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : β„•} {L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) :
          L.wildExponent = 0 ↔ Β¬ringChar (IsLocalRing.ResidueField β†₯(ValuativeRel.valuation K).integer) ∣ n

          The tame criterion for Οƒ_K(n): for L ∈ Οƒ_K(n), the wild exponent vanishes exactly when the residue characteristic of K does not divide n. Since L / K is totally ramified, d(L) is the different exponent, so this is differentExponent_eq_ramificationIndex_sub_one_iff.

          source
          @[simp]
          theorem IntermediateField.wildExponent_bot {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
          βŠ₯.wildExponent = 0

          The bottom subextension has wild exponent 0.

          source
          @[simp]
          theorem IntermediateField.discriminantExponent_bot {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
          βŠ₯.discriminantExponent = 0

          The bottom subextension has discriminant exponent 0.

          source
          theorem IntermediateField.discriminantExponent_eq_of_algEquiv {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L M : IntermediateField K (SeparableClosure K)} (e : β†₯L ≃ₐ[K] β†₯M) :
          L.discriminantExponent = M.discriminantExponent

          The discriminant exponent is an invariant of the K-isomorphism class, junk case included: this is discriminantExponent_eq_of_algEquiv when L / K is finite, and both sides are 0 otherwise.

          source
          theorem IntermediateField.wildExponent_eq_of_algEquiv {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {L M : IntermediateField K (SeparableClosure K)} (e : β†₯L ≃ₐ[K] β†₯M) :
          L.wildExponent = M.wildExponent

          The wild exponent is an invariant of the K-isomorphism class, junk case included.