The different ideal localizes at a completion

Let L/K be an extension of number fields, v a finite place of K and w a finite place of L above v, with completed integer rings 𝒪_v ⊆ 𝒪_w. Then the different of 𝒪 L / 𝒪 K generates the different of the local extension 𝒪_w / 𝒪_v:

𝔇(𝒪 L / 𝒪 K) · 𝒪_w = 𝔇(𝒪_w / 𝒪_v).

The trace dual of the global extension spans the trace dual of the completed extension. This comparison gives the equality of different ideals, and lets results about the global different be used at each completed place. The semilocal decomposition relates the global trace pairing to the local pairings.

This is the completion counterpart of TauCeti.span_traceDual_one_eq_traceDual_one, TauCeti.extended_dual_one_eq_dual_one, and TauCeti.map_differentIdeal_eq_differentIdeal in TauCeti/RingTheory/DedekindDomain/Different/Localization.lean; the trace-dual comparison and the names follow that formal localization result.

The completion comparison equations are used with both places explicit: their left-hand sides determine w but not the base place v, so they are not simplification rules.

Main results

All in the namespace IsDedekindDomain.HeightOneSpectrum, as they take the place v first:

• sum_trace_mul_smul_algebraMap_eq: a trace-dual expansion of L over K remains one of L_w over K_v.
• span_traceDual_one_eq_traceDual_one_adicCompletionIntegers: the local trace dual is spanned by the global one.
• extended_dual_one_eq_dual_one_adicCompletionIntegers: the same statement for fractional ideals, as the extension of the global trace dual along 𝒪 L → 𝒪_w.
• map_differentIdeal_eq_differentIdeal_adicCompletionIntegers: the different ideal commutes with completion.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter III, Proposition (2.2).
• J.-P. Serre, Corps locaux, Chapter III, §4, Proposition 10.

theorem IsDedekindDomain.HeightOneSpectrum.sum_trace_mul_smul_algebraMap_eq {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] {ι : Type u_3} [Fintype ι] (b y : ι → L) (h : ∀ (x : L), ∑ i : ι, (Algebra.trace K L) (x * b i) • y i = x) (z : adicCompletion L w) : ∑ i : ι, (Algebra.trace (adicCompletion K v) (adicCompletion L w)) (z * (algebraMap L (adicCompletion L w)) (b i)) • (algebraMap L (adicCompletion L w)) (y i) = z

Trace-dual expansions pass to completions. If x = ∑ᵢ Tr_{L/K}(x bᵢ) yᵢ for every x ∈ L, then z = ∑ᵢ Tr_{L_w/K_v}(z bᵢ) yᵢ for every z ∈ L_w.

theorem IsDedekindDomain.HeightOneSpectrum.span_traceDual_one_eq_traceDual_one_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Submodule.span (↥(adicCompletionIntegers L w)) (⇑(algebraMap L (adicCompletion L w)) '' ↑(Submodule.traceDual (NumberField.RingOfIntegers K) K 1)) = Submodule.traceDual (↥(adicCompletionIntegers K v)) (adicCompletion K v) 1

The local trace dual is spanned by the global one. The trace dual of 𝒪_w over 𝒪_v is the 𝒪_w-span of the image in L_w of the trace dual of 𝒪 L over 𝒪 K.

theorem IsDedekindDomain.HeightOneSpectrum.extended_dual_one_eq_dual_one_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : FractionalIdeal.extended (adicCompletion L w) ⋯ (FractionalIdeal.dual (NumberField.RingOfIntegers K) K 1) = FractionalIdeal.dual (↥(adicCompletionIntegers K v)) (adicCompletion K v) 1

Trace duals commute with completion, as fractional ideals: extending the trace dual of 𝒪 L over 𝒪 K to 𝒪_w gives the trace dual of 𝒪_w over 𝒪_v.

theorem IsDedekindDomain.HeightOneSpectrum.map_differentIdeal_eq_differentIdeal_adicCompletionIntegers {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : HeightOneSpectrum (NumberField.RingOfIntegers L)) [w.asIdeal.LiesOver v.asIdeal] : Ideal.map (algebraMap (NumberField.RingOfIntegers L) ↥(adicCompletionIntegers L w)) (differentIdeal (NumberField.RingOfIntegers K) (NumberField.RingOfIntegers L)) = differentIdeal ↥(adicCompletionIntegers K v) ↥(adicCompletionIntegers L w)

The different commutes with completion. The different ideal of 𝒪 L over 𝒪 K generates in 𝒪_w the different ideal of 𝒪_w over 𝒪_v.