Sums over representatives of the isomorphism classes

Serre's mass formula has two forms: the sum of q ^ (-c(L)) over the totally ramified extensions L ∈ σ_K(n) of a local field K inside a fixed separable closure, which equals n, and the sum of 1 / (#Aut_K(M) · q ^ c(M)) over a set of representatives M of their K-isomorphism classes, which equals 1. This file passes from the first to the second.

Following Serre, a set of representatives is a predicate rather than a quotient: IsRepresentativeSet n R says that R ⊆ σ_K(n) and that every member of σ_K(n) is K-isomorphic to exactly one member of R. Such sets exist. A sum over σ_K(n) of a function that is constant on K-isomorphism classes splits along the classes. By the orbit count TauCeti.ncard_isomorphic_mul_natCard_algEquiv, the class of M has n / #Aut_K(M) members, so the sum equals the sum over R of n / #Aut_K(M) times the value at M. The wild exponent is such a function, so the two forms of the mass formula are equivalent.

Main definitions

• TauCeti.IsRepresentativeSet n R: R is a set of representatives of the K-isomorphism classes of σ_K(n).

Main results

• TauCeti.exists_isRepresentativeSet: sets of representatives exist.

In the namespace TauCeti.IsRepresentativeSet:

• tsum_eq_tsum_div_natCard_algEquiv_mul: a sum over σ_K(n) of an isomorphism-invariant function, regrouped along isomorphism classes.
• mul_tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent: n · ∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = ∑_{L ∈ σ_K(n)} q ^ (-c(L)).
• tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff: for 0 < n, the second form of the mass formula holds for R exactly when the first does.

References

• J.-P. Serre, Une « formule de masse » pour les extensions totalement ramifiées de degré donné d'un corps local, C. R. Acad. Sci. Paris Sér. A 286 (1978), 1031–1036, Théorème 2 and Remarque 3°.

def TauCeti.IsRepresentativeSet {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) (R : Set (IntermediateField K (SeparableClosure K))) : Prop

A set R of subextensions of SeparableClosure K is a set of representatives of the K-isomorphism classes of σ_K(n) when R ⊆ σ_K(n) and every member of σ_K(n) is K-isomorphic to exactly one member of R.

theorem TauCeti.isRepresentativeSet_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} : IsRepresentativeSet n R ↔ R ⊆ totallyRamifiedOfDegree K n ∧ ∀ L ∈ totallyRamifiedOfDegree K n, ∃! M : IntermediateField K (SeparableClosure K), M ∈ R ∧ Nonempty (↥L ≃ₐ[K] ↥M)

theorem TauCeti.exists_isRepresentativeSet (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : ∃ (R : Set (IntermediateField K (SeparableClosure K))), IsRepresentativeSet n R

Every σ_K(n) has a set of representatives of its K-isomorphism classes.

theorem TauCeti.IsRepresentativeSet.subset {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} (hR : IsRepresentativeSet n R) : R ⊆ totallyRamifiedOfDegree K n

theorem TauCeti.IsRepresentativeSet.existsUnique {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} {L : IntermediateField K (SeparableClosure K)} (hR : IsRepresentativeSet n R) (hL : L ∈ totallyRamifiedOfDegree K n) : ∃! M : IntermediateField K (SeparableClosure K), M ∈ R ∧ Nonempty (↥L ≃ₐ[K] ↥M)

theorem TauCeti.IsRepresentativeSet.tsum_eq_tsum_div_natCard_algEquiv_mul {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} (hR : IsRepresentativeSet n R) (f : IntermediateField K (SeparableClosure K) → ENNReal) (hf : ∀ {L M : IntermediateField K (SeparableClosure K)} (a : ↥L ≃ₐ[K] ↥M), f L = f M) : ∑' (L : ↑(totallyRamifiedOfDegree K n)), f ↑L = ∑' (M : ↑R), ↑n / ↑(Nat.card Gal(↥↑M/K)) * f ↑M

A sum over σ_K(n) of a function that is constant on K-isomorphism classes, regrouped along the classes: the class of a representative M has n / #Aut_K(M) members.

theorem TauCeti.IsRepresentativeSet.mul_tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} (hR : IsRepresentativeSet n R) : ↑n * ∑' (M : ↑R), 1 / (↑(Nat.card Gal(↥↑M/K)) * ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑M).wildExponent) = ∑' (L : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent

The two sums of Serre's mass formula, related along isomorphism classes: n · ∑_{M ∈ R} 1 / (#Aut_K(M) · q ^ c(M)) = ∑_{L ∈ σ_K(n)} q ^ (-c(L)).

theorem TauCeti.IsRepresentativeSet.tsum_one_div_natCard_algEquiv_mul_natCard_residueField_pow_wildExponent_eq_one_iff {K : Type u_1} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {n : ℕ} {R : Set (IntermediateField K (SeparableClosure K))} (hR : 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 : ↑(totallyRamifiedOfDegree K n)), 1 / ↑(Nat.card (IsLocalRing.ResidueField ↥(ValuativeRel.valuation K).integer)) ^ (↑L).wildExponent = ↑n

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.