Local Field

Results named in Tau Ceti's TauCeti.NumberTheory.LocalField modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremDedekind's different theorem, the tame case#

d(L/K) = e(L/K) - 1 exactly when L/K is tamely ramified.

TauCeti.differentExponent_eq_ramificationIndex_sub_one_iff.{u_1, u_2} (K : Type u_1) (L : Type u_2)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L]
  [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Algebra.IsSeparable K L] :
  TauCeti.differentExponent K L = TauCeti.ramificationIndex K L - 1 ↔ TauCeti.IsTamelyRamified K L
Lean

Formalized in Tau Ceti as TauCeti.differentExponent_eq_ramificationIndex_sub_one_iff.

Other forms

Dedekind's different theorem for the discriminant in the tame case. Formalized in Tau Ceti as TauCeti.discriminantExponent_eq_inertiaDegree_mul_ramificationIndex_sub_one_iff.

TauCeti.discriminantExponent_eq_inertiaDegree_mul_ramificationIndex_sub_one_iff.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] :
  TauCeti.discriminantExponent K L =
      TauCeti.inertiaDegree K L * (TauCeti.ramificationIndex K L - 1) ↔
    TauCeti.IsTamelyRamified K L
Sources
LeanTauCeti.differentExponent_eq_ramificationIndex_sub_one_iff · TauCeti.discriminantExponent_eq_inertiaDegree_mul_ramificationIndex_sub_one_iff
Uses 3 · Used by 25
Statement usesTauCeti.relDiscr
Proof usesDedekind's different theorem, the tame case, as an exponent · TauCeti.algebraicExtensionNormedField
Used byThe criterion of Néron, Ogg and Shafarevich for potential good reduction (Silverman AEC VII.7.3) · The criterion of Néron, Ogg and Shafarevich with finite coefficients (Serre–Tate) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Hilbert reciprocity · Local reciprocity for the Weil group · Quadratic reciprocity is Hilbert reciprocity for two odd primes · The global class formation · The global invariant · The global invariant is injective · The local class formation · The local invariant · Serre's mass formula for quadratic extensions in odd residue characteristic · Serre's mass formula for the quadratic extensions of ℚ_2 · The totally ramified quadratic extensions of ℚ_2 · Iwasawa's theorem · Tame inertia is procyclic · Tame inertia is the prime-to-p Tate module · The Galois group of the maximal unramified extension is the profinite integers · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Hilbert's product formula · Tate's duality on an open subgroup acting trivially on μₙ · The Kronecker–Weber theorem · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The upper bound of Dedekind's different theorem

TheoremThe finite level of the generator theorem (NSW, proof of (7.4.1))#

For a finite extension K of ℚ_p, every finite quotient of G_K through which the commutator subgroup of wild inertia dies is generated by [K : ℚ_p] + 2 elements. The generators form a tuple, in which repetitions are allowed: the quotient may have fewer than [K : ℚ_p] + 2 elements.

TauCeti.exists_generating_tuple_quotient (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K]
  [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K]
  (U : OpenNormalSubgroup (Field.absoluteGaloisGroup K))
  (hU : ⁅TauCeti.wildInertiaSubgroup K, TauCeti.wildInertiaSubgroup K⁆ ≤ ↑U.toOpenSubgroup) :
  ∃ x, Subgroup.closure (Set.range x) = ⊤
Lean

Formalized in Tau Ceti as TauCeti.exists_generating_tuple_quotient.

Sources
LeanTauCeti.exists_generating_tuple_quotient
Uses 29 · Used by 1
Statement usesThe wild inertia subgroup
Proof usesArtin's theorem · Artin's theorem for a finite group of automorphisms · Corestriction through Shapiro's lemma · Dedekind's different theorem, the tame case · Dimension shifting in every positive degree · Euler's theorem on an n-th root of unity · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The first half of Dedekind's different theorem · The first isomorphism theorem for a surjective strict homomorphism of topological groups · Fitting's lemma · Hensel's lemma for the norm · The Kummer isomorphism · The local class formation · The local invariant · Local reciprocity for A(L) · Local Tate duality in degree one · Lyndon's theorem for the relation module (NSW (5.6.6)) · Maschke's theorem after base change · Restriction through Shapiro's lemma · Schanuel's lemma in automorphism form · Shapiro's lemma in degree one · The strict cohomological dimension through integral coefficients (NSW (3.3.4)), as vanishing predicates · Swan's theorem for ℤ_p[G] (NSW (5.6.10)(ii)) · Tate's theorem · Tate's theorem for a class formation, in every integer degree · TauCeti.algebraicExtensionNormedField · TauCeti.ClassFieldTheory.tateTheorem · The third isomorphism theorem for coset spaces
Used byThe generator rank of a local absolute Galois group (NSW (7.4.1))

TheoremThe first half of Dedekind's different theorem#

e(L/K) - 1 ≤ d(L/K).

TauCeti.ramificationIndex_sub_one_le_differentExponent.{u_1, u_2} (K : Type u_1) (L : Type u_2)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L]
  [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Algebra.IsSeparable K L] :
  TauCeti.ramificationIndex K L - 1 ≤ TauCeti.differentExponent K L
Lean

Formalized in Tau Ceti as TauCeti.ramificationIndex_sub_one_le_differentExponent.

Other forms

The first half of Dedekind's different theorem, for the discriminant. Formalized in Tau Ceti as TauCeti.inertiaDegree_mul_ramificationIndex_sub_one_le_discriminantExponent.

TauCeti.inertiaDegree_mul_ramificationIndex_sub_one_le_discriminantExponent.{u_1, u_2}
  (K : Type u_1) (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L] :
  TauCeti.inertiaDegree K L * (TauCeti.ramificationIndex K L - 1) ≤ TauCeti.discriminantExponent K L
Sources
LeanTauCeti.ramificationIndex_sub_one_le_differentExponent · TauCeti.inertiaDegree_mul_ramificationIndex_sub_one_le_discriminantExponent
Uses 3 · Used by 26
Statement usesTauCeti.relDiscr
Proof usesDedekind's different theorem, the tame case, as an exponent · TauCeti.algebraicExtensionNormedField
Used byThe criterion of Néron, Ogg and Shafarevich for potential good reduction (Silverman AEC VII.7.3) · The criterion of Néron, Ogg and Shafarevich with finite coefficients (Serre–Tate) · The m-Selmer group of an elliptic curve over a number field is finite (Silverman X.4.2) · Hilbert reciprocity · Local reciprocity for the Weil group · Quadratic reciprocity is Hilbert reciprocity for two odd primes · The global class formation · The global invariant · The global invariant is injective · The local class formation · The local invariant · Serre's first mass formula · Serre's mass formula for quadratic extensions in odd residue characteristic · Serre's mass formula for the quadratic extensions of ℚ_2 · The totally ramified quadratic extensions of ℚ_2 · Iwasawa's theorem · Tame inertia is procyclic · Tame inertia is the prime-to-p Tate module · The Galois group of the maximal unramified extension is the profinite integers · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · Hilbert's product formula · Tate's duality on an open subgroup acting trivially on μₙ · The Kronecker–Weber theorem · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The upper bound of Dedekind's different theorem

TheoremThe Gram formula for the Kummer cup over ℚ₂#

In square-class coordinates along -1, 2, 5, the cup is x₀ y₀ + x₁ y₂ + x₂ y₁ times the nonzero class (-1) ∪ (-1). The scalar lies in ZMod 2.

TauCeti.kummerCup_padicTwo (x y : TauCeti.SquareClassGroup ℚ_[2]) :
  ((TauCeti.kummerCup ℚ_[2]) x) y =
    ((TauCeti.padicTwoSquareClassBasis.repr x) 0 * (TauCeti.padicTwoSquareClassBasis.repr y) 0 +
          (TauCeti.padicTwoSquareClassBasis.repr x) 1 *
            (TauCeti.padicTwoSquareClassBasis.repr y) 2 +
        (TauCeti.padicTwoSquareClassBasis.repr x) 2 * (TauCeti.padicTwoSquareClassBasis.repr y) 1) •
      ((TauCeti.kummerCup ℚ_[2]) (TauCeti.squareClass (-1))) (TauCeti.squareClass (-1))
Lean

Formalized in Tau Ceti as TauCeti.kummerCup_padicTwo.

Sources
LeanTauCeti.kummerCup_padicTwo
Uses 5
Statement usesThe Kummer isomorphism
Proof usesA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Serre's formula for the Artin conductor · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField

TheoremHasse--Arf in prime degree#

Every upper ramification break of a finite Galois extension of prime degree is an integer.

TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_finrank_prime.{u_1, u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L]
  [IsGalois K L] {u : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain}
  (hu : TauCeti.LocalFieldsRamification.UpperJump K L u)
  (hdegree : Nat.Prime (Module.finrank K L)) : ∃ z, ↑u = ↑z
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_finrank_prime.

Other forms

Hasse--Arf. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.hasseArf.

TauCeti.LocalFieldsRamification.hasseArf.{u, v} (K : Type u) (L : Type v) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L]
  [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L]
  [Module.Finite K L] [IsAbelianGalois K L]
  {w : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain}
  (hw : TauCeti.LocalFieldsRamification.UpperJump K L w) : ∃ z, ↑w = ↑z

Hasse--Arf for cyclic extensions of prime-power degree. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_isPGroup.

TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_isPGroup.{u, v} {K : Type u}
  {L : Type v} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] [IsCyclic Gal(L/K)] {p : ℕ}
  [Fact (Nat.Prime p)] (hp : IsPGroup p Gal(L/K))
  {u : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain}
  (hu : TauCeti.LocalFieldsRamification.UpperJump K L u) : ∃ z, ↑u = ↑z

Hasse--Arf for elementary abelian extensions. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_exponent_prime.

TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_exponent_prime.{u_1, u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L]
  [IsAbelianGalois K L] {u : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain}
  (hu : TauCeti.LocalFieldsRamification.UpperJump K L u)
  (hp : Nat.Prime (Monoid.exponent Gal(L/K))) : ∃ z, ↑u = ↑z
Sources
LeanTauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_finrank_prime · TauCeti.LocalFieldsRamification.hasseArf · TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_isPGroup · TauCeti.LocalFieldsRamification.UpperJump.exists_eq_intCast_of_exponent_prime
Uses 7 · Used by 1
Proof usesHensel's lemma for the norm · Herbrand's theorem in the upper numbering · Hilbert's formula, truncated · Hilbert's Theorem 90 for cyclic extensions · TauCeti.algebraicExtensionNormedField · TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField · The third isomorphism theorem for coset spaces
Used bySerre's formula for the Artin conductor

TheoremHilbert's formula, truncated#

for a finite Galois extension L/K of nonarchimedean local fields, ∑_{i < m} (#G_i - 1) ≤ d(L/K) for every m.

TauCeti.sum_range_card_lowerRamificationGroup_sub_one_le_differentExponent.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] (m : ℕ) :
  ∑ i ∈ Finset.range m,
      (Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i) - 1) ≤
    TauCeti.differentExponent K L
Lean

Formalized in Tau Ceti as TauCeti.sum_range_card_lowerRamificationGroup_sub_one_le_differentExponent.

Other forms

Hilbert's formula for the different exponent. Formalized in Tau Ceti as TauCeti.differentExponent_eq_finsum_lowerRamificationGroup.

TauCeti.differentExponent_eq_finsum_lowerRamificationGroup.{u_1, u_2} (K : Type u_1) (L : Type u_2)
  [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Field L]
  [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] :
  TauCeti.differentExponent K L =
    ∑ᶠ (i : ℕ), (Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i) - 1)

Hilbert's formula, as a finite sum. Formalized in Tau Ceti as TauCeti.differentExponent_eq_sum_range_lowerRamificationGroup.

TauCeti.differentExponent_eq_sum_range_lowerRamificationGroup.{u_1, u_2} (K : Type u_1)
  (L : Type u_2) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
  [Field L] [ValuativeRel L] [TopologicalSpace L] [IsNonarchimedeanLocalField L] [Algebra K L]
  [ValuativeExtension K L] [Module.Finite K L] [IsGalois K L] {N : ℕ}
  (hN : TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑N = ⊥) :
  TauCeti.differentExponent K L =
    ∑ i ∈ Finset.range N,
      (Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i) - 1)
Sources
LeanTauCeti.sum_range_card_lowerRamificationGroup_sub_one_le_differentExponent · TauCeti.differentExponent_eq_finsum_lowerRamificationGroup · TauCeti.differentExponent_eq_sum_range_lowerRamificationGroup
Uses 2 · Used by 2
Proof usesHilbert's counting identity · TauCeti.algebraicExtensionNormedField
Used byHilbert's formula for a number-field different exponent · Hasse--Arf in prime degree

TheoremThe local square theorem bounds the defect of a unit#

A unit of 𝒪[K] approximated by a square to order 2 v_K(2) + 1 is a square, so the defect exponent of a nonsquare unit is at most 2 v_K(2). In odd residue characteristic the bound is 0.

TauCeti.defectExponent_le_two_mul_natCastValuation.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] (h2 : 2 ≠ 0) {u : Kˣ}
  (hu : (ValuativeRel.valuation K) ↑u = 1) (hsq : ¬IsSquare u) :
  TauCeti.defectExponent u ≤ ↑↑(2 * TauCeti.natCastValuation K 2 h2)
Lean

Formalized in Tau Ceti as TauCeti.defectExponent_le_two_mul_natCastValuation.

Sources
LeanTauCeti.defectExponent_le_two_mul_natCastValuation

TheoremSerre's quotient formula for the lower index#

For an intermediate field L of M/K normal over K and σ' : Gal(L/K), e(M/L) · i_{L/K}(σ') = ∑_{σ|_L = σ'} i_{M/K}(σ), the sum running over the automorphisms of M/K restricting to σ'.

TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_eq_sum.{u_1, u_2, u_3}
  {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M]
  [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L]
  [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M]
  [ValuativeExtension K M] [Module.Finite K M] [IsGalois K M] [IsScalarTower K L M]
  (σ' : Gal(L/K)) :
  ↑(TauCeti.ramificationIndex L M) *
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) σ' =
    ∑ σ with σ.restrictNormal L = σ',
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_eq_sum.

Other forms

Serre's quotient formula for the lower index, over a coset. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum.

TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum.{u_1, u_2,
    u_3}
  {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Field M] [ValuativeRel M] [TopologicalSpace M]
  [IsNonarchimedeanLocalField M] [Algebra K L] [ValuativeExtension K L] [Module.Finite K L]
  [Normal K L] [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M]
  [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] [IsGalois L M] (σ : Gal(M/K)) :
  ↑(TauCeti.ramificationIndex L M) *
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L) =
    ∑ τ,
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer)
        (σ * AlgEquiv.restrictScalars K τ)
Sources
LeanTauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_eq_sum · TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum
Uses 2 · Used by 1
Proof usesSerre's criterion · TauCeti.algebraicExtensionNormedField
Used bySerre's lemma on the lower index of a quotient

TheoremThe upper bound of Dedekind's different theorem#

If the ramification index e(L/K) is nonzero in L, the different exponent of L/K is at most e(L/K) − 1 + v_L(e(L/K)).

TauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation.{u_1, u_2}
  {K : Type u_1} {L : Type u_2} [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] [Field L] [ValuativeRel L] [TopologicalSpace L]
  [IsNonarchimedeanLocalField L] [Algebra K L] [ValuativeExtension K L] [Algebra.IsSeparable K L]
  (he : ↑(TauCeti.ramificationIndex K L) ≠ 0) :
  TauCeti.differentExponent K L ≤
    TauCeti.ramificationIndex K L - 1 +
      TauCeti.natCastValuation L (TauCeti.ramificationIndex K L) he
Lean

Formalized in Tau Ceti as TauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation.

Sources
LeanTauCeti.differentExponent_le_ramificationIndex_sub_one_add_natCastValuation
Uses 3 · Used by 2
Proof usesDedekind's different theorem, the tame case · The first half of Dedekind's different theorem · TauCeti.algebraicExtensionNormedField
Used byThe wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n · Hermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.