The integral semi-local decomposition of a number field

Let L/K be an extension of number fields and let v be a finite place of K. The scalar extension of the ring of integers of L to the completed integer ring at v decomposes as the product of the completed integer rings at the places above v:

𝒪_v ⊗[𝓞 K] 𝓞 L ≃ₐ[𝒪_v] ∏_{w ∣ v} 𝒪_w.

The map sends a pure tensor a ⊗ x to (a * x)_w. Its scalar extension to the fraction field is the semi-local decomposition semilocalEquiv. Surjectivity follows from simultaneous approximation in the finitely many completed integer rings: the image is both dense and closed, the latter because it is a finitely generated submodule over the compact ring 𝒪_v.

Main definitions

• TauCeti.integralSemilocalHom: the canonical homomorphism to the product of completed integer rings.
• TauCeti.integralSemilocalToField: the canonical map from the integral tensor product to the field tensor product.
• TauCeti.integralSemilocalEquiv: the integral semi-local decomposition.

Main results

• TauCeti.integralSemilocalEquiv_tmul: the value of the equivalence on pure tensors.
• TauCeti.integralSemilocalEquiv_fieldCompatibility: after inclusion into the completions, the integral equivalence agrees with semilocalEquiv.

References

• [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, Proposition (8.3).

noncomputable def TauCeti.integralSemilocalHom {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L) →ₐ[↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)

The canonical map from the integral scalar extension at v to the product of the completed integer rings at the places above v.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.integralSemilocalHom_tmul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (x : NumberField.RingOfIntegers L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) : (integralSemilocalHom L v) (a ⊗ₜ[NumberField.RingOfIntegers K] x) w = (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) a * (algebraMap (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) x

The integral semi-local map on a pure tensor.

theorem TauCeti.denseRange_algebraMap_integers_pi_liesOver {K : Type u_1} [Field K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : DenseRange fun (x : NumberField.RingOfIntegers L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) => (algebraMap (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) x

The diagonal image of the global integers is dense in the product of the completed integer rings at the places above v.

theorem TauCeti.integralSemilocalHom_surjective {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Surjective ⇑(integralSemilocalHom L v)

The integral semi-local map is surjective.

noncomputable def TauCeti.integralSemilocalToField {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L) →ₐ[NumberField.RingOfIntegers K] TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L

The canonical inclusion of the integral tensor product in the field tensor product.

Equations

• TauCeti.integralSemilocalToField L v = (TauCeti.integralFieldBaseChangeAlgHom✝ L v).comp (TauCeti.integralTensorToBaseChange✝ L v)

@[simp]

theorem TauCeti.integralSemilocalToField_tmul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (x : NumberField.RingOfIntegers L) : (integralSemilocalToField L v) (a ⊗ₜ[NumberField.RingOfIntegers K] x) = ↑a ⊗ₜ[K] ↑x

The inclusion in the field tensor product on a pure tensor.

theorem TauCeti.integralSemilocalHom_fieldCompatibility {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (z : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L)) : (semilocalEquiv L v) ((integralSemilocalToField L v) z) = fun (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) => ↑((integralSemilocalHom L v) z w)

The integral and field semi-local maps agree after inclusion in the completions.

theorem TauCeti.integralSemilocalToField_injective {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Injective ⇑(integralSemilocalToField L v)

The canonical inclusion of the integral tensor product in the field tensor product is injective.

theorem TauCeti.integralSemilocalHom_injective {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Function.Injective ⇑(integralSemilocalHom L v)

The integral semi-local map is injective.

noncomputable def TauCeti.integralSemilocalEquiv {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L) ≃ₐ[↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)] (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) → ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)

The integral semi-local decomposition: scalar extension of the global integers to the completed integer ring at v is the product of the completed integer rings above v.

Equations

• TauCeti.integralSemilocalEquiv L v = AlgEquiv.ofBijective (TauCeti.integralSemilocalHom L v) ⋯

@[simp]

theorem TauCeti.integralSemilocalEquiv_tmul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (x : NumberField.RingOfIntegers L) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) : (integralSemilocalEquiv L v) (a ⊗ₜ[NumberField.RingOfIntegers K] x) w = (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) a * (algebraMap (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) x

The integral semi-local decomposition on a pure tensor.

theorem TauCeti.integralSemilocalEquiv_fieldCompatibility {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (z : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L)) : (semilocalEquiv L v) ((integralSemilocalToField L v) z) = fun (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) => ↑((integralSemilocalEquiv L v) z w)

After inclusion into the completions, the integral semi-local decomposition agrees with the field semi-local decomposition.

noncomputable def TauCeti.integralSemilocalComponent {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L) →ₐ[↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)

Projection of the integral semi-local decomposition to the completed integer ring at w.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.integralSemilocalComponent_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) (z : TensorProduct (NumberField.RingOfIntegers K) (↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (NumberField.RingOfIntegers L)) : (integralSemilocalComponent w) z = (integralSemilocalEquiv L v) z w

A component projection is evaluation of the integral semi-local decomposition.

theorem TauCeti.integralSemilocalComponent_tmul {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) (a : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)) (x : NumberField.RingOfIntegers L) : (integralSemilocalComponent w) (a ⊗ₜ[NumberField.RingOfIntegers K] x) = (algebraMap ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) a * (algebraMap (NumberField.RingOfIntegers L) ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers L ↑w)) x

A component projection of the integral semi-local decomposition on a pure tensor.