Counting totally ramified extensions of a local field, and Serre's mass formula
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.
TheoremThe orbit count ([Serre 1978, Remarque 3°])#
for L ∈ σ_K(n), the isomorphism class of L
inside σ_K(n) has n / #Aut_K(L) members, in multiplied form. The extension L / K is separable
of degree n, so it has n embeddings into SeparableClosure K; their images are the members of
the class, and the embeddings with a given image form a torsor under Aut_K(L).
TauCeti.ncard_isomorphic_mul_natCard_algEquiv.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ}
{L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n) :
{M | M ∈ TauCeti.totallyRamifiedOfDegree K n ∧ Nonempty (↥L ≃ₐ[K] ↥M)}.ncard *
Nat.card Gal(↥L/K) =
n
Uses 2 · Used by 1
TheoremTauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff#
For 0 < n, Serre's mass formula over a set of representatives,
∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = 1, is equivalent to the mass formula over σ_K(n),
∑_{L ∈ σ_K(n)} q ^ (-c(L)) = n.
TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff.{u_1}
{K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
{n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))}
(hR : TauCeti.IsRepresentativeSet n R) (hn : 0 < n) :
∑' (M : ↑R),
1 /
(↑(Nat.card Gal(↥↑M/K)) *
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑M).wildExponent) =
1 ↔
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree K n)),
1 /
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑L).wildExponent =
↑n
Lean
Formalized in Tau Ceti as TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff.
Sources
- Tau Ceti documentation:
TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff - Source of
TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iffin TauCeti/NumberTheory/LocalField/MassFormula/Representative.lean - Tau Ceti roadmap status: Counting totally ramified extensions of a local field, and Serre's mass formula
Uses 5 · Used by 1
TheoremThe totally ramified quadratic extensions of ℚ_2#
If x₁, …, x₆ are square roots of
-1, -5, 2, -2, 10, -10 in the separable closure of ℚ_2, then
σ_{ℚ_2}(2) = {ℚ_2(x₁), ℚ_2(x₂), ℚ_2(x₃), ℚ_2(x₄), ℚ_2(x₅), ℚ_2(x₆)}.
TauCeti.totallyRamifiedOfDegree_two_eq_padicTwo {x₁ x₂ x₃ x₄ x₅ x₆ : SeparableClosure ℚ_[2]}
(h₁ : x₁ ^ 2 = -1) (h₂ : x₂ ^ 2 = -5) (h₃ : x₃ ^ 2 = 2) (h₄ : x₄ ^ 2 = -2) (h₅ : x₅ ^ 2 = 10)
(h₆ : x₆ ^ 2 = -10) :
TauCeti.totallyRamifiedOfDegree ℚ_[2] 2 =
{ℚ_[2]⟮x₁⟯, ℚ_[2]⟮x₂⟯, ℚ_[2]⟮x₃⟯, ℚ_[2]⟮x₄⟯, ℚ_[2]⟮x₅⟯, ℚ_[2]⟮x₆⟯}
Lean
Formalized in Tau Ceti as TauCeti.totallyRamifiedOfDegree_two_eq_padicTwo.
Sources
- Tau Ceti documentation:
TauCeti.totallyRamifiedOfDegree_two_eq_padicTwo - Source of
TauCeti.totallyRamifiedOfDegree_two_eq_padicTwoin TauCeti/NumberTheory/LocalField/MassFormula/Quadratic/PadicTwo.lean - Tau Ceti roadmap status: Counting totally ramified extensions of a local field, and Serre's mass formula
Uses 9
n-th root of unity · The first half of Dedekind's different theorem · IntermediateField.wildExponent · Serre's formula for the Artin conductor · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscr
TheoremSerre's mass formula for the quadratic extensions of ℚ_2#
∑_{L ∈ σ_{ℚ_2}(2)} 2 ^ (-c(L)) = 2 · 2⁻¹ + 4 · 2⁻² = 2.
TauCeti.tsum_one_div_pow_wildExponent_two_padicTwo :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree ℚ_[2] 2)), 1 / 2 ^ (↑L).wildExponent = 2
Lean
Formalized in Tau Ceti as TauCeti.tsum_one_div_pow_wildExponent_two_padicTwo.
Other forms
Serre's mass formula for quadratic extensions of ℚ_p for an odd prime p. Formalized in Tau Ceti as TauCeti.Padic.tsum_one_div_pow_wildExponent_two.
TauCeti.Padic.tsum_one_div_pow_wildExponent_two {p : ℕ} [Fact (Nat.Prime p)] (hp : p ≠ 2) :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree ℚ_[p] 2)), 1 / ↑p ^ (↑L).wildExponent = 2
Sources
- Tau Ceti documentation:
TauCeti.tsum_one_div_pow_wildExponent_two_padicTwo - Source of
TauCeti.tsum_one_div_pow_wildExponent_two_padicTwoin TauCeti/NumberTheory/LocalField/MassFormula/Quadratic/PadicTwo.lean - Tau Ceti roadmap status: Counting totally ramified extensions of a local field, and Serre's mass formula
Uses 10
n-th root of unity · The first half of Dedekind's different theorem · Serre's formula for the Artin conductor · Serre's mass formula for quadratic extensions in odd residue characteristic · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscrTheoremSerre's mass formula for quadratic extensions in odd residue characteristic#
∑_{L ∈ σ_K(2)} q ^ (-c(L)) = 2, where q is the cardinality of the residue field of K. Both
members of σ_K(2) are tamely ramified, with weight 1.
TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_two.{u_1} {K : Type u_1} [Field K]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
(h2 : ¬ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ 2) :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree K 2)),
1 /
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑L).wildExponent =
2
Lean
Formalized in Tau Ceti as TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_two.
Other forms
Serre's mass formula over 𝔽_q((X)). Formalized in Tau Ceti as TauCeti.tsum_one_div_natCard_pow_wildExponent_laurentSeries.
TauCeti.tsum_one_div_natCard_pow_wildExponent_laurentSeries.{u_1} (F : Type u_1) [Field F]
[Finite F] {n : ℕ} :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree (LaurentSeries F) n)),
1 / ↑(Nat.card F) ^ (↑L).wildExponent =
↑n
Sources
- Tau Ceti documentation:
TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_two - Source of
TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent_twoin TauCeti/NumberTheory/LocalField/MassFormula/Quadratic/Basic.lean - Tau Ceti roadmap status: Counting totally ramified extensions of a local field, and Serre's mass formula
Uses 8 · Used by 1
TheoremHensel's lemma with an estimate over a Henselian discrete valuation ring#
If the order of
F at y₀ exceeds twice the order of its derivative there, then F has a root z whose
distance to y₀ has order exactly addVal (F(y₀)) - addVal (F'(y₀)). This is the existence
part of Mathlib's hensels_lemma in addVal spelling; the uniqueness of z in that ball is
Polynomial.existsUnique_isRoot_addVal_lt.
Polynomial.exists_isRoot_addVal_eval_eq.{u_1} {A : Type u_1} [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [HenselianLocalRing A] (F : Polynomial A) (y₀ : A)
(hlt :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) +
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) <
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ F)) :
∃ z,
F.IsRoot z ∧
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ F) =
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) +
(IsDiscreteValuationRing.addVal A) (z - y₀)
Lean
Formalized in Tau Ceti as Polynomial.exists_isRoot_addVal_eval_eq.
Other forms
Hensel's lemma with uniqueness over a Henselian discrete valuation ring. Formalized in Tau Ceti as Polynomial.existsUnique_isRoot_addVal_lt.
Polynomial.existsUnique_isRoot_addVal_lt.{u_1} {A : Type u_1} [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] [HenselianLocalRing A] (F : Polynomial A) (y₀ : A)
(hlt :
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) +
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) <
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ F)) :
∃! z,
F.IsRoot z ∧
(IsDiscreteValuationRing.addVal A) (Polynomial.eval y₀ (Polynomial.derivative F)) <
(IsDiscreteValuationRing.addVal A) (z - y₀)
Sources
Uses 1 · Used by 2
TheoremLocal constancy of the root count#
For a monic f over 𝒪[K] that is separable over
K, there is a threshold T > 0 such that every monic g over 𝒪[K] with
g.coeff i - f.coeff i ∈ 𝓂[K] ^ T for all i has as many roots as f, counted with
multiplicity, in every finite intermediate field of Ω / K. The threshold depends only on f.
TauCeti.exists_card_aroots_eq.{u_1, u_2} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] (Ω : Type u_2) [Field Ω] [Algebra K Ω]
{f : Polynomial ↥(ValuativeRel.valuation K).integer} (hf : f.Monic)
(hfsep : (Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f).Separable) :
∃ T,
0 < T ∧
∀ (M : IntermediateField K Ω) [Module.Finite K ↥M]
(g : Polynomial ↥(ValuativeRel.valuation K).integer),
g.Monic →
(∀ (i : ℕ),
g.coeff i - f.coeff i ∈
IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ T) →
((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) g).aroots
↥M).card =
((Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f).aroots
↥M).card
Uses 2 · Used by 1
TheoremThe scaling law for Haar measure#
If the determinant of a square matrix A over 𝒪[K]
is associated to ϖ ^ k for a uniformizer ϖ, then for every regular additive Haar measure μ
on ι → K and every set s, μ (A '' s) = q ^ (-k) * μ s, where q = Nat.card 𝓀[K]. This is
the nonarchimedean analogue of MeasureTheory.Measure.addHaar_image_linearMap.
MeasureTheory.Measure.addHaar_image_mulVec.{u_1, u_2} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {ι : Type u_2} [Fintype ι] [DecidableEq ι]
[MeasurableSpace (ι → K)] [BorelSpace (ι → K)] (μ : MeasureTheory.Measure (ι → K))
[μ.IsAddHaarMeasure] [μ.Regular] {A : Matrix ι ι ↥(ValuativeRel.valuation K).integer}
{ϖ : ↥(ValuativeRel.valuation K).integer} (hϖ : Irreducible ϖ) {k : ℕ}
(hk : Associated A.det (ϖ ^ k)) (s : Set (ι → K)) :
μ ((A.map ⇑(algebraMap (↥(ValuativeRel.valuation K).integer) K)).mulVec '' s) =
1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ k * μ s
TheoremInfinitely many totally ramified extensions in equal characteristic#
If 0 < n and
(n : K) = 0, that is, K has characteristic p > 0 with p ∣ n, then σ_K(n) is infinite:
its discriminant exponents are unbounded.
TauCeti.infinite_totallyRamifiedOfDegree.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) (hnK : ↑n = 0) :
(TauCeti.totallyRamifiedOfDegree K n).Infinite
Uses 3 · Used by 1
DefinitionTauCeti.totallyRamifiedOfDegree#
Serre's σ_K(n): the subextensions of SeparableClosure K that are totally ramified of
degree n over K.
TauCeti.totallyRamifiedOfDegree.{u_1} (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K] (n : ℕ) : Set (IntermediateField K (SeparableClosure K))
Uses 1 · Used by 11
ℚ_2 · Serre's second mass formula · TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff · 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 ∣ nDefinitionIntermediateField.wildExponent#
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.
IntermediateField.wildExponent.{u_1} {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K] (L : IntermediateField K (SeparableClosure K)) : ℕ
Uses 2 · Used by 8
ℚ_2 · Serre's second mass formula · TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff · The totally ramified quadratic extensions of ℚ_2 · The wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n
TheoremThe wild exponent is bounded on σ_K(n) away from equal characteristic p ∣ n#
if n
is nonzero in K, every L ∈ σ_K(n) has c(L) ≤ n · v_K(n). In equal characteristic, where
v_K(n) = 0, this recovers c(L) = 0 for p ∤ n.
IntermediateField.wildExponent_le_mul_natCastValuation.{u_1} {K : Type u_1} [Field K]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ}
{L : IntermediateField K (SeparableClosure K)} (hL : L ∈ TauCeti.totallyRamifiedOfDegree K n)
(hnK : ↑n ≠ 0) : L.wildExponent ≤ n * TauCeti.natCastValuation K n hnK
Lean
Formalized in Tau Ceti as IntermediateField.wildExponent_le_mul_natCastValuation.
Sources
- Tau Ceti documentation:
IntermediateField.wildExponent_le_mul_natCastValuation - Source of
IntermediateField.wildExponent_le_mul_natCastValuationin TauCeti/NumberTheory/LocalField/MassFormula/Finite.lean - Tau Ceti roadmap status: Counting totally ramified extensions of a local field, and Serre's mass formula
Uses 5 · Used by 1
DefinitionTauCeti.eisensteinSet#
The Eisenstein region in the space Fin n → K of coefficient vectors of monic polynomials of
degree n: every coefficient has valuation below 1, and the constant term of monicOfCoeff a
has valuation at least that of every element of valuation below 1. For 0 < n the constant term
is a 0, which then has the valuation of a uniformizer; for n = 0 it is 1, and the region is
the whole one-point space. When 𝒪[K] is a discrete valuation ring,
TauCeti.mem_eisensteinSet_iff_exists_isEisensteinAt identifies these with the coefficient vectors
of the polynomials over 𝒪[K] that are Eisenstein at 𝓂[K].
TauCeti.eisensteinSet.{u_1} (K : Type u_1) [Field K] [ValuativeRel K] (n : ℕ) : Set (Fin n → K)
TheoremThe volume of the Eisenstein region#
for a left-invariant measure on Fin n → K
normalized on the integer box, the Eisenstein region has volume q ^ (-n) (1 - q⁻¹) for
0 < n, where q = Nat.card 𝓀[K].
TauCeti.measure_eisensteinSet.{u_1} {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) [MeasurableSpace (Fin n → K)]
[BorelSpace (Fin n → K)] (μ : MeasureTheory.Measure (Fin n → K)) [μ.IsAddLeftInvariant]
(hμ : μ (TauCeti.integerBox K (Fin n)) = 1) :
μ (TauCeti.eisensteinSet K n) =
1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ n *
(1 - 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)))
Uses 1 · Used by 1
DefinitionIntermediateField.rootCount#
The root count of a coefficient vector a : Fin n → K in a subextension L: the number of
roots of the monic polynomial monicOfCoeff a lying in L, counted with multiplicity.
IntermediateField.rootCount.{u_1, u_2} {K : Type u_1} {E : Type u_2} [Field K] [Field E]
[Algebra K E] (L : IntermediateField K E) {n : ℕ} (a : Fin n → K) : ℕ
Used by 2
TheoremThe root counts over σ_K(n) sum to n#
Let f be an Eisenstein polynomial over 𝒪[K]
with image monicOfCoeff a over K, for a : Fin n → K, and assume that monicOfCoeff a is
separable. Then ∑_{L ∈ σ_K(n)} L.rootCount a = n: each of the n roots of monicOfCoeff a in
the separable closure lies in exactly one member of σ_K(n), the one it generates.
TauCeti.tsum_rootCount_eq_of_separable.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {a : Fin n → K}
{f : Polynomial ↥(ValuativeRel.valuation K).integer}
(he : f.IsEisensteinAt (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer))
(hf :
Polynomial.map (algebraMap (↥(ValuativeRel.valuation K).integer) K) f =
TauCeti.Polynomial.monicOfCoeff a)
(hsep : (TauCeti.Polynomial.monicOfCoeff a).Separable) :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree K n)), ↑((↑L).rootCount a) = ↑n
Uses 4 · Used by 1
TheoremPolynomial.card_roots_eq_sum_ite_of_addVal_lt#
Count roots by a finite disjoint family of balls covering them. If the derivative order at each root is smaller than the ball order, each occupied ball contributes exactly one root. The derivative bound also excludes repeated rational roots, so no separability hypothesis is needed.
Polynomial.card_roots_eq_sum_ite_of_addVal_lt.{u_1} {A : Type u_1} [CommRing A] [IsDomain A]
[IsDiscreteValuationRing A] (F : Polynomial A) (C : Finset A) {r : ℕ}
(hcover : ∀ x ∈ F.roots, ∃ c ∈ C, ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c))
(hdisj : (↑C).PairwiseDisjoint fun c => {x | ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c)})
(hder :
∀ x ∈ F.roots,
(IsDiscreteValuationRing.addVal A) (Polynomial.eval x (Polynomial.derivative F)) < ↑r) :
F.roots.card =
∑ c ∈ C, if ∃ x ∈ F.roots, ↑r ≤ (IsDiscreteValuationRing.addVal A) (x - c) then 1 else 0
Used by 1
TheoremSerre's finiteness dichotomy#
for 0 < n, there are infinitely many totally ramified
degree-n subextensions of a separable closure of K exactly when K has equal
characteristic p, the residue characteristic, and p ∣ n.
TauCeti.infinite_totallyRamifiedOfDegree_iff.{u_1} {K : Type u_1} [Field K] [ValuativeRel K]
[TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) :
(TauCeti.totallyRamifiedOfDegree K n).Infinite ↔
ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∧
ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n
Lean
Formalized in Tau Ceti as TauCeti.infinite_totallyRamifiedOfDegree_iff.
Other forms
Serre's finiteness dichotomy, relative to the weighted count. Formalized in Tau Ceti as TauCeti.infinite_totallyRamifiedOfDegree_iff_or_tsum_eq_top.
TauCeti.infinite_totallyRamifiedOfDegree_iff_or_tsum_eq_top.{u_1} {K : Type u_1} [Field K]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} (hn : 0 < n) :
(TauCeti.totallyRamifiedOfDegree K n).Infinite ↔
ringChar K = ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∧
ringChar (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer) ∣ n ∨
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree K n)),
1 /
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑L).wildExponent =
⊤
Sources
TheoremSerre's first mass formula#
the totally ramified degree-n subextensions L of a
separable closure of K satisfy ∑_L q ^ (-c(L)) = n, where q is the residue cardinality of
K and c(L) is the wild exponent.
TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent.{u_1} {K : Type u_1} [Field K]
[ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} :
∑' (L : ↑(TauCeti.totallyRamifiedOfDegree K n)),
1 /
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑L).wildExponent =
↑n
Lean
Formalized in Tau Ceti as TauCeti.tsum_one_div_natCard_residueField_pow_wildExponent.
Sources
Uses 13 · Used by 3
σ_K(n) sum to n · TauCeti.algebraicExtensionNormedField · TauCeti.eisensteinSet · TauCeti.relDiscr · The volume of the Eisenstein regionTheoremSerre's second mass formula#
for 0 < n and every set R of representatives of the
K-isomorphism classes in σ_K(n), ∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = 1.
TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent.{u_1}
{K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K]
{n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))}
(hR : TauCeti.IsRepresentativeSet n R) (hn : 0 < n) :
∑' (M : ↑R),
1 /
(↑(Nat.card Gal(↥↑M/K)) *
↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^
(↑M).wildExponent) =
1
Lean
Formalized in Tau Ceti as TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.