Local fields and ramification

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremIwasawa's theorem#

the tame quotient of the absolute Galois group of K is isomorphic, as a topological group, to the profinite group ⟨σ, τ | σ τ σ⁻¹ = τ ^ q⟩.

TauCeti.nonempty_continuousMulEquiv_iwasawaGroup.{u} (K : Type u) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
  Nonempty (TauCeti.tameQuotient K ≃ₜ* TauCeti.IwasawaGroup K)
Lean

Formalized in Tau Ceti as TauCeti.nonempty_continuousMulEquiv_iwasawaGroup.

Sources
LeanTauCeti.nonempty_continuousMulEquiv_iwasawaGroup
Uses 8
Statement usesThe wild inertia subgroup
Proof usesDedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · The Galois group of the maximal unramified extension is the profinite integers · The profinite power · Tame inertia is the prime-to-p Tate module · TauCeti.algebraicExtensionNormedField

TheoremTauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField#

An upper break of a finite abelian extension is detected in a cyclic subextension. The subextension can be chosen with trivial upper ramification groups at every later index, so the specified break is its last break. Its local-field structures are the canonical ones induced from the base field.

TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField.{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) :
  TauCeti.LocalFieldsRamification.UpperJump K L u ↔
    ∃ F,
      IsCyclic Gal(↥F/K) ∧
        TauCeti.LocalFieldsRamification.UpperJump K (↥F) u ∧
          ∀ (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain),
            u < v → TauCeti.LocalFieldsRamification.upperRamificationGroup K (↥F) v = ⊥
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField.

Sources
LeanTauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField
Uses 2 · Used by 1
Statement usesTauCeti.algebraicExtensionNormedField
Proof usesHerbrand's theorem in the upper numbering
Used byHasse--Arf in prime degree

TheoremHerbrand's theorem in the upper numbering#

For a tower M/L/K of Galois extensions, the image of the upper ramification group G^v of M/K under restriction to L is the upper ramification group of L/K at the same index: (G/H)^v = G^v H / H for H = Gal(M/L).

TauCeti.LocalFieldsRamification.map_restrictNormalHom_upperRamificationGroup.{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]
  [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M]
  [IsScalarTower K L M] [IsGalois K L] [IsGalois K M]
  (v : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) :
  Subgroup.map (AlgEquiv.restrictNormalHom L)
      (TauCeti.LocalFieldsRamification.upperRamificationGroup K M v) =
    TauCeti.LocalFieldsRamification.upperRamificationGroup K L v
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.map_restrictNormalHom_upperRamificationGroup.

Other forms

Herbrand's theorem. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.map_restrictNormalHom_lowerRamificationGroupReal.

TauCeti.LocalFieldsRamification.map_restrictNormalHom_lowerRamificationGroupReal.{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] [IsGalois L M]
  [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] [Normal K M]
  (u : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) :
  Subgroup.map (AlgEquiv.restrictNormalHom L)
      (TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K M ↑u) =
    TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K L
      ↑(TauCeti.LocalFieldsRamification.herbrand L M u)

Herbrand's theorem in counting form. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroupReal_herbrand_mul.

TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroupReal_herbrand_mul.{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]
  [Algebra L M] [ValuativeExtension L M] [Module.Finite L M] [Algebra K M] [ValuativeExtension K M]
  [IsScalarTower K L M] [Normal K L] [IsGalois L M] [Normal K M]
  (u : ↑TauCeti.LocalFieldsRamification.RamificationIndexDomain) :
  Nat.card
        ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K L
            ↑(TauCeti.LocalFieldsRamification.herbrand L M u)) *
      Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroupReal L M ↑u) =
    Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroupReal K M ↑u)
Sources
LeanTauCeti.LocalFieldsRamification.map_restrictNormalHom_upperRamificationGroup · TauCeti.LocalFieldsRamification.map_restrictNormalHom_lowerRamificationGroupReal · TauCeti.LocalFieldsRamification.natCard_lowerRamificationGroupReal_herbrand_mul
Uses 2 · Used by 2
Proof usesSerre's lemma on the lower index of a quotient · TauCeti.algebraicExtensionNormedField
Used byTauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField · Hasse--Arf in prime degree

TheoremTauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne#

Lower numbering fails to commute with this restriction: the image at depth three is the whole quadratic Galois group, but the quadratic lower group at depth three is trivial.

TauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne :
  Subgroup.map TauCeti.DyadicCyclotomicEight.restrictSqrtTwo
      (TauCeti.LocalFieldsRamification.lowerRamificationGroup ℚ_[2] TauCeti.DyadicCyclotomicEight
        3) ≠
    TauCeti.LocalFieldsRamification.lowerRamificationGroup ℚ_[2] TauCeti.DyadicSqrtTwo 3
Lean

Formalized in Tau Ceti as TauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne.

Sources
LeanTauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne
Uses 2
Proof usesSerre's criterion · TauCeti.algebraicExtensionNormedField

DefinitionTame inertia is the prime-to-p Tate module#

the tame character induces an isomorphism of topological groups I_K / P_K ≃ₜ* ℤ̂^{(p')}(1) from the tame inertia group, the quotient of the inertia subgroup by the wild inertia subgroup.

TauCeti.quotientWildInertiaSubgroupEquiv.{u_1} (K : Type u_1) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
  ↥(TauCeti.inertiaSubgroup K) ⧸
      (TauCeti.wildInertiaSubgroup K).subgroupOf (TauCeti.inertiaSubgroup K) ≃ₜ*
    TauCeti.PrimeToPTateModule
      (ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) (AlgebraicClosure K)
Lean

Formalized in Tau Ceti as TauCeti.quotientWildInertiaSubgroupEquiv.

Sources
LeanTauCeti.quotientWildInertiaSubgroupEquiv
Uses 5 · Used by 2
Statement usesThe wild inertia subgroup
Proof usesDedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · TauCeti.algebraicExtensionNormedField
Used byIwasawa's theorem · Tame inertia is ∏_{ℓ ≠ p} ℤ_ℓ

TheoremTame inertia is ∏_{ℓ ≠ p} ℤ_ℓ#

the tame inertia group I_K/P_K is isomorphic, as a topological group, to the product of the additive groups of ℓ-adic integers over the primes ℓ different from the residue characteristic p. Up to a choice of an isomorphism ℤ_ℓ(1) ≃ ℤ_ℓ for each ℓ (TauCeti.PadicTateTwist.nonempty_continuousAddEquiv), it is the tame character I_K/P_K ≃ ℤ̂^{(p')}(1) (TauCeti.quotientWildInertiaSubgroupEquiv) followed by the decomposition of ℤ̂^{(p')}(1) into its ℓ-adic components (TauCeti.PrimeToPTateModule.continuousMulEquivPiPadicTateTwist).

TauCeti.nonempty_continuousMulEquiv_piPadicInt.{u_1} (K : Type u_1) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
  Nonempty
    (↥(TauCeti.inertiaSubgroup K) ⧸
        (TauCeti.wildInertiaSubgroup K).subgroupOf (TauCeti.inertiaSubgroup K) ≃ₜ*
      Multiplicative
        ((ℓ :
            { ℓ // ↑ℓ ≠ ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) }) →
          ℤ_[↑↑ℓ]))
Lean

Formalized in Tau Ceti as TauCeti.nonempty_continuousMulEquiv_piPadicInt.

Sources
LeanTauCeti.nonempty_continuousMulEquiv_piPadicInt
Uses 3
Statement usesThe wild inertia subgroup
Proof usesThe prime-to-p Tate module is the product of its ℓ-adic components · Tame inertia is the prime-to-p Tate module

TheoremTame inertia is procyclic#

it is topologically generated by the class of an element of the inertia subgroup.

TauCeti.exists_topologicalClosure_zpowers_eq_tameInertia.{u} (K : Type u) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] :
  ∃ τ ∈ TauCeti.inertiaSubgroup K,
    (Subgroup.zpowers ((TauCeti.toTameQuotient K) τ)).topologicalClosure = TauCeti.tameInertia K
Lean

Formalized in Tau Ceti as TauCeti.exists_topologicalClosure_zpowers_eq_tameInertia.

Sources
LeanTauCeti.exists_topologicalClosure_zpowers_eq_tameInertia
Uses 5
Statement usesThe wild inertia subgroup
Proof usesDedekind's different theorem, the tame case · Euler's theorem on an n-th root of unity · The first half of Dedekind's different theorem · TauCeti.algebraicExtensionNormedField

DefinitionThe Galois group of the maximal unramified extension is the profinite integers#

This continuous multiplicative equivalence sends arithmetic Frobenius to zHat.gen.

TauCeti.maximalUnramifiedGaloisGroupEquivZHat.{u, v} (K : Type u) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type v) [Field Ω] [Algebra K Ω]
  [IsSepClosed Ω] :
  Gal(↥(TauCeti.maximalUnramifiedExtension K Ω)/K) ≃ₜ* ↑TauCeti.zHat.toProfinite.toTop
Lean

Formalized in Tau Ceti as TauCeti.maximalUnramifiedGaloisGroupEquivZHat.

Sources
LeanTauCeti.maximalUnramifiedGaloisGroupEquivZHat
Uses 3 · Used by 8
Statement usesTauCeti.algebraicExtensionNormedField
Proof usesDedekind's different theorem, the tame case · The first half of Dedekind's different theorem
Used byHilbert reciprocity · Local reciprocity for the Weil group · The global class formation · The global invariant · The global invariant is injective · Iwasawa's theorem · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · The Kronecker–Weber theorem

DefinitionTauCeti.algebraicExtensionNormedField#

The normed-field structure on an algebraic extension M of a nonarchimedean local field K given by the spectral norm of M/K with respect to the normalized absolute value of K.

TauCeti.algebraicExtensionNormedField.{u_1, u_2} (K : Type u_1) [Field K] [ValuativeRel K]
  [TopologicalSpace K] [IsNonarchimedeanLocalField K] (M : Type u_2) [Field M] [Algebra K M]
  [Algebra.IsAlgebraic K M] : NormedField M
Lean

Formalized in Tau Ceti as TauCeti.algebraicExtensionNormedField.

Sources
LeanTauCeti.algebraicExtensionNormedField
Used by 78
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) · Finite global reciprocity · 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 idelic consequence of Furtwängler's theorem · The Kummer case of global existence (Milne VII, Lemma 9.3) · The local class formation · The local invariant · The norm index theorem · Infinitely many totally ramified extensions in equal characteristic · IntermediateField.wildExponent · Local constancy of the root count · 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 · TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff · TauCeti.totallyRamifiedOfDegree · The orbit count ([Serre 1978, Remarque 3°]) · The root counts over σ_K(n) sum to n · The totally ramified quadratic extensions of ℚ_2 · The wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n · Hilbert sign prescription (O'Meara 71:19a) · Local equivalence by invariants · O'Meara 72:1 up to one global representation · The Hasse product formula · The kernel of the idele Hilbert character · The system of local invariants of a regular quadratic form Q over a number field · Herbrand's theorem in the upper numbering · Iwasawa's theorem · Serre's formula for the Artin conductor · Serre's lemma on the lower index of a quotient · Tame inertia is procyclic · Tame inertia is the prime-to-p Tate module · TauCeti.DyadicCyclotomicEight.map_restrictSqrtTwo_lowerRamificationGroup_three_ne · TauCeti.LocalFieldsRamification.upperJump_iff_exists_isCyclic_intermediateField · The Galois group of the maximal unramified extension is the profinite integers · Demushkin's theorem · Existence of the Tate module of a finite layer (NSW (5.6.5) and the proof of (7.4.1)) · Local reciprocity for A(L) · Shafarevich's theorem · The cyclotomic normalization of the local Artin map of a finite extension of ℚ_p · The generator rank of a local absolute Galois group (NSW (7.4.1)) · The marked presentation of G_{ℚ₂}(2) · The marked presentation of G_{ℚ₂(√-2)}(2) · Hilbert's formula for a number-field different exponent · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Hilbert's product formula · Local classification (O'Meara 63:20, Serre IV Thm 7) · The classification of regular forms over a local field, as an equivalence · The Hilbert symbol as a bilinear form over 𝔽₂ · The relative Stiefel–Whitney formula over a local field · Global existence (Milne VII, Theorem 9.5) · Local Tate duality in degree one · Modular-Artin reduction of the local Euler characteristic formula · Perfect local Tate duality in mixed characteristic · Shapiro's lemma for the normalized order · Tate's duality on an open subgroup acting trivially on μₙ · Tate's local Euler characteristic formula · The cyclic Hasse norm theorem · The Euler characteristic formula and G₀ · The Hasse principle for Brauer classes, from idele-class H¹ · The Kronecker–Weber theorem · The Kummer case of the second fundamental inequality · Dedekind's different theorem, the tame case · Hasse--Arf in prime degree · Hilbert's formula, truncated · Serre's quotient formula for the lower index · The finite level of the generator theorem (NSW, proof of (7.4.1)) · The first half of Dedekind's different theorem · The Gram formula for the Kummer cup over ℚ₂ · The upper bound of Dedekind's different theorem · Hermite's theorem: finitely many extensions of bounded degree are unramified outside a finite set

DefinitionThe wild inertia subgroup#

The wild inertia subgroup P_K of the absolute Galois group of a nonarchimedean local field K: the automorphisms of the algebraic closure fixing the maximal tamely ramified extension K^{t}. Through IntermediateField.fixingSubgroupEquiv it is Gal(K^{alg}/K^{t}).

TauCeti.wildInertiaSubgroup.{u_1} (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K] : Subgroup (Field.absoluteGaloisGroup K)
Lean

Formalized in Tau Ceti as TauCeti.wildInertiaSubgroup.

Sources
LeanTauCeti.wildInertiaSubgroup
Used by 6
Used byIwasawa's theorem · Tame inertia is ∏_{ℓ ≠ p} ℤ_ℓ · Tame inertia is procyclic · Tame inertia is the prime-to-p Tate module · The generator rank of a local absolute Galois group (NSW (7.4.1)) · The finite level of the generator theorem (NSW, proof of (7.4.1))

DefinitionThe prime-to-p Tate module is the product of its ℓ-adic components#

the ℓ-adic components toPadicTateTwist, over all primes ℓ prime to p, form an isomorphism of topological groups ℤ̂^{(p')}(1) ≃ₜ* ∏_{ℓ ∤ p} ℤ_ℓ(1). It holds for every commutative monoid E, by the Chinese remainder theorem at each level μ_m(E).

TauCeti.PrimeToPTateModule.continuousMulEquivPiPadicTateTwist.{u_1} (p : ℕ) (E : Type u_1)
  [CommMonoid E] :
  TauCeti.PrimeToPTateModule p E ≃ₜ*
    ((ℓ : { ℓ // Nat.Prime ℓ ∧ ℓ.Coprime p }) → Multiplicative (TauCeti.PadicTateTwist (↑ℓ) E))
Lean

Formalized in Tau Ceti as TauCeti.PrimeToPTateModule.continuousMulEquivPiPadicTateTwist.

Sources
LeanTauCeti.PrimeToPTateModule.continuousMulEquivPiPadicTateTwist
Used by 1
Used byTame inertia is ∏_{ℓ ≠ p} ℤ_ℓ

TheoremSerre's formula for the Artin conductor#

Serre's formula for the Artin conductor, truncated at any index n at which χ is trivial on G_n: for a finite abelian extension of local fields, f(χ) · #G_0 = ∑_{i < n, χ(G_i) ≠ 1} #G_i.

TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_eq_sum_range.{u_1, u_2, u_3}
  (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] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) {n : ℕ}
  (hn : TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑n ≤ χ.ker)
  [DecidablePred fun i => TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i ≤ χ.ker] :
  TauCeti.LocalFieldsRamification.artinConductorExponent K L χ *
      Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L 0) =
    ∑ i ∈ Finset.range n,
      if TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i ≤ χ.ker then 0
      else Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i)
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_eq_sum_range.

Other forms

Serre's formula for the Artin conductor. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_lowerRamificationGroup_zero.

TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_lowerRamificationGroup_zero.{u_1,
    u_2, u_3}
  (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] {M : Type u_3} [MulOneClass M] (χ : Gal(L/K) →* M) :
  TauCeti.LocalFieldsRamification.artinConductorExponent K L χ *
      Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L 0) =
    ∑ᶠ (i : ℕ) (_ : ¬TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i ≤ χ.ker),
      Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup K L ↑i)

Serre's formula for the Hilbert symbol over ℚ_2. Formalized in Tau Ceti as TauCeti.hilbertSymbol_padicTwo.

TauCeti.hilbertSymbol_padicTwo {a b : ℚ_[2]ˣ} {α β : ℤ} {u v : ℤ_[2]ˣ} (ha : ↑a = 2 ^ α * ↑↑u)
  (hb : ↑b = 2 ^ β * ↑↑v) :
  TauCeti.hilbertSymbol a b =
    (-1) ^
      (TauCeti.serreEps u * TauCeti.serreEps v + ↑α * TauCeti.serreOmega v +
        ↑β * TauCeti.serreOmega u)

Serre's formula for the Hilbert symbol over ℚ_p, for p odd. Formalized in Tau Ceti as TauCeti.Padic.hilbertSymbol_formula_of_ne_two.

TauCeti.Padic.hilbertSymbol_formula_of_ne_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2)
  {a b : ℚ_[p]ˣ} {α β : ℤ} {u v : ℤ_[p]ˣ} (ha : ↑a = ↑p ^ α * ↑↑u) (hb : ↑b = ↑p ^ β * ↑↑v) :
  TauCeti.hilbertSymbol a b =
    ((-1) ^ ((p - 1) / 2)) ^ (α * β) *
        (quadraticChar (ZMod p)).toUnitHom ((Units.map ↑PadicInt.toZMod) u) ^ β *
      (quadraticChar (ZMod p)).toUnitHom ((Units.map ↑PadicInt.toZMod) v) ^ α

Serre's formula over ℚ_p for integers, with Legendre symbols. Formalized in Tau Ceti as TauCeti.Padic.coe_hilbertSymbol_pow_mul_intCast_pow_mul_intCast.

TauCeti.Padic.coe_hilbertSymbol_pow_mul_intCast_pow_mul_intCast {p : ℕ} [Fact (Nat.Prime p)]
  (hp : p ≠ 2) (α β : ℕ) {m n : ℤ} (hm : ¬↑p ∣ m) (hn : ¬↑p ∣ n) :
  ↑(TauCeti.hilbertSymbol (Units.mk0 (↑p ^ α * ↑m) ⋯) (Units.mk0 (↑p ^ β * ↑n) ⋯)) =
    (-1) ^ (α * β * ((p - 1) / 2)) * legendreSym p m ^ β * legendreSym p n ^ α
Sources
LeanTauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_eq_sum_range · TauCeti.LocalFieldsRamification.artinConductorExponent_mul_card_lowerRamificationGroup_zero · TauCeti.hilbertSymbol_padicTwo · TauCeti.Padic.hilbertSymbol_formula_of_ne_two · TauCeti.Padic.coe_hilbertSymbol_pow_mul_intCast_pow_mul_intCast
Uses 4 · Used by 4
Proof usesHasse--Arf in prime degree · Hensel's lemma for the norm · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField
Used byQuadratic reciprocity is Hilbert reciprocity for two odd primes · Serre's mass formula for the quadratic extensions of ℚ_2 · The totally ramified quadratic extensions of ℚ_2 · The Gram formula for the Kummer cup over ℚ₂

TheoremSerre's lemma on the lower index of a quotient#

If σ has the largest lower index in its coset σ H, and i_G(σ) = j is finite, then φ_{M/L}(j - 1) = i_{G/H}(σ|_L) - 1.

TauCeti.LocalFieldsRamification.coe_herbrand_lowerIndex_sub_one.{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] [IsGalois L M]
  [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K))
  {j : ℕ} (hj : TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ = ↑j)
  (hσ :
    ∀ (τ : Gal(M/L)),
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer)
          (σ * AlgEquiv.restrictScalars K τ) ≤
        TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) :
  ↑(TauCeti.LocalFieldsRamification.herbrand L M ⟨↑j - 1, ⋯⟩) =
    ↑(TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer)
            (σ.restrictNormal L)).toNat -
      1
Lean

Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.coe_herbrand_lowerIndex_sub_one.

Other forms

Serre's lemma on the lower index of a quotient, in counting form. Formalized in Tau Ceti as TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum_card.

TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum_card.{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] [IsGalois L M]
  [Algebra K M] [ValuativeExtension K M] [Module.Finite K M] [IsScalarTower K L M] (σ : Gal(M/K))
  {j : ℕ} (hj : TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ = ↑j)
  (hσ :
    ∀ (τ : Gal(M/L)),
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer)
          (σ * AlgEquiv.restrictScalars K τ) ≤
        TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation M).integer) σ) :
  ↑(TauCeti.ramificationIndex L M) *
      TauCeti.IsLocalRing.lowerIndex (↥(ValuativeRel.valuation L).integer) (σ.restrictNormal L) =
    ∑ k ∈ Finset.range j,
      ↑(Nat.card ↥(TauCeti.LocalFieldsRamification.lowerRamificationGroup L M ↑k))
Sources
LeanTauCeti.LocalFieldsRamification.coe_herbrand_lowerIndex_sub_one · TauCeti.LocalFieldsRamification.ramificationIndex_mul_lowerIndex_restrictNormal_eq_sum_card
Uses 2 · Used by 1
Proof usesSerre's quotient formula for the lower index · TauCeti.algebraicExtensionNormedField
Used byHerbrand's theorem in the upper numbering

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.