The global different exponent

The coefficient of the different ideal of a number-field extension at a prime w equals the coefficient of the different ideal of the completed integer-ring extension at its maximal ideal. The global different extends to the completed different, and completion preserves the multiplicity of an ideal at the selected prime. This is the coefficient comparison needed to transport local different-exponent theorems to number fields.

For a Galois extension, Hilbert's local different formula and the comparison between global and local ramification groups then express this coefficient as \sum_{i \ge 0} (\# G_i - 1).

References

• J. Neukirch, Algebraic Number Theory, Chapter III, Proposition 2.2 and Theorem 2.6.
• J.-P. Serre, Corps Locaux, Chapter IV, §1, Proposition 4.

theorem IsDedekindDomain.HeightOneSpectrum.adjoin_integerEquivAdicCompletionIntegers_eq_top {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (x : ↥(ValuativeRel.valuation (adicCompletion L w)).integer) (hx : (↥(ValuativeRel.valuation (adicCompletion K v)).integer)[x] = ⊤) : (↥(adicCompletionIntegers K v))[w.integerEquivAdicCompletionIntegers x] = ⊤

A generator of the abstract valuation integer ring remains a generator after identifying it with the concrete adic-completion integer ring.

theorem IsDedekindDomain.HeightOneSpectrum.map_minpoly_integerEquivAdicCompletionIntegers {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] (x : ↥(ValuativeRel.valuation (adicCompletion L w)).integer) : Polynomial.map v.integerEquivAdicCompletionIntegers.toRingHom (minpoly (↥(ValuativeRel.valuation (adicCompletion K v)).integer) x) = minpoly (↥(adicCompletionIntegers K v)) (w.integerEquivAdicCompletionIntegers x)

Minimal polynomials are carried across the canonical identifications between abstract valuation integer rings and concrete adic-completion integer rings.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.map_differentIdeal_integerEquivAdicCompletionIntegers {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Ideal.map w.integerEquivAdicCompletionIntegers (differentIdeal ↥(ValuativeRel.valuation (adicCompletion K v)).integer ↥(ValuativeRel.valuation (adicCompletion L w)).integer) = differentIdeal ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)

The identification of the abstract valuation rings of K_v ⊆ L_w with the concrete completed integer rings carries the local different ideal to the completed different ideal.

theorem IsDedekindDomain.HeightOneSpectrum.differentExponent_adicCompletion_eq_multiplicity_differentIdeal {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : TauCeti.differentExponent (adicCompletion K v) (adicCompletion L w) = multiplicity (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers L w)) (differentIdeal ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w))

The local different exponent of L_w/K_v is the multiplicity of the completed different ideal in the maximal ideal of the concrete completed integer ring.

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_adicCompletionIntegers_eq_multiplicity_asIdeal {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : multiplicity (IsLocalRing.maximalIdeal ↥(adicCompletionIntegers L w)) (differentIdeal ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)) = multiplicity w.asIdeal (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L))

The exponent of the completed different at the maximal ideal is the exponent of the global different at w.

theorem IsDedekindDomain.HeightOneSpectrum.multiplicity_differentIdeal_eq_finsum_card_ramificationGroup_sub_one {K : Type u_1} {L : Type u_2} [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [IsGalois K L] : multiplicity w.asIdeal (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = ∑ᶠ (i : ℕ), (Nat.card ↥(Ideal.ramificationGroup Gal(L/K) w.asIdeal i) - 1)

Hilbert's formula for a number-field different exponent. For a finite Galois extension L/K, the multiplicity of a prime w in the global different is the sum of the orders of the nonnegative-index lower ramification groups, minus one in each degree.