The semi-local map K_v ⊗[K] L → ∏_{w ∣ v} L_w #
Let L/K be an extension of number fields and v a finite place of K. Every finite place w
of L above v gives a completion L_w, which is a K_v-algebra through the canonical
completion map completionAlgHom v w. Together these give the semi-local map
semilocalHom v : K_v ⊗[K] L →ₐ[K_v] ∏_{w ∣ v} L_w, a ⊗ x ↦ (a · x)_w .
This map is an isomorphism of K_v-algebras, semilocalEquiv v: the semi-local decomposition of
Neukirch II (8.3). It identifies the scalar extension of L to K_v with the product of the
completions of L at the places above v, so a question about L over K at v becomes the
same question for the finitely many local extensions L_w/K_v. Comparing the degrees of its two
sides gives the local–global degree identity ∑_{w ∣ v} [L_w : K_v] = [L : K], whose counterpart
at the infinite places is Mathlib's NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank.
The places above v are indexed by the subtype
{w : HeightOneSpectrum (𝓞 L) // w.asIdeal.LiesOver v.asIdeal}, which is finite
(IsDedekindDomain.HeightOneSpectrum.finite_liesOver) and which
IsDedekindDomain.HeightOneSpectrum.liesOverEquivPrimesOver identifies with
Ideal.primesOver v.asIdeal (𝓞 L).
Main definitions #
TauCeti.semilocalHom: the semi-local mapK_v ⊗[K] L →ₐ[K_v] ∏_{w ∣ v} L_w.TauCeti.semilocalEquiv: that map, as an isomorphism ofK_v-algebras.
Main results #
TauCeti.semilocalHom_tmulandTauCeti.semilocalEquiv_tmul: the value on pure tensors,semilocalEquiv v (a ⊗ₜ x) w = algebraMap K_v L_w a * algebraMap L L_w x, which determines the map.TauCeti.denseRange_algebraMap_pi_liesOver:Lis dense in∏_{w ∣ v} L_w.TauCeti.semilocalHom_surjectiveandTauCeti.semilocalHom_injective: the semi-local map is surjective and injective.TauCeti.sum_finrank_adicCompletion_eq_finrank:∑_{w ∣ v} [L_w : K_v] = [L : K].TauCeti.semilocalContinuousEquiv: the semi-local decomposition as a continuous algebra equivalence when the tensor product carries its module topology overK_v.
Topology #
Both sides of the semi-local decomposition are finite-dimensional K_v-vector spaces. Each
carries its canonical K_v-module topology, which on ∏_{w ∣ v} L_w is the product topology,
and K_v-linear maps between such spaces are continuous. So when K_v ⊗[K] L carries its module
topology, semilocalEquiv v is a homeomorphism. This placewise identification of topological
rings is the finite-place input for identifying the finite adeles of L with the scalar
extension of the finite adeles of K to L.
Provenance #
The continuous equivalence and its companion formulas follow the archimedean analogue
TauCeti.GlobalNumberFields.infiniteSemilocalContinuousEquiv in
TauCeti.NumberTheory.NumberField.Global.Places.Semilocal.
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, Proposition (8.3).
The semi-local map K_v ⊗[K] L → ∏_{w ∣ v} L_w of a finite place v of K, sending
a ⊗ x to the family (a · x)_w over the places w of L above v. Each L_w is a
K_v-algebra through the canonical completion map completionAlgHom v w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The semi-local map on a pure tensor.
Weak approximation above v. The diagonal image of L is dense in the product of the
completions of L at the places above v.
The semi-local map is surjective: every family (y_w)_{w ∣ v} of elements of the
completions L_w is the image of an element of K_v ⊗[K] L.
The local degrees above v add up to the global degree:
∑_{w ∣ v} [L_w : K_v] = [L : K]. Each local degree is e(w ∣ v) · f(w ∣ v), and the sum of
those products over the primes above v is the global degree.
The semi-local map is injective: an element of K_v ⊗[K] L is determined by its images
in the completions L_w at the places w of L above v.
The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w: completing L at the
finitely many places above a finite place v of K decomposes the scalar extension of L to
K_v into the product of those completions.
Equations
Instances For
The semi-local decomposition is the semi-local map.
The semi-local decomposition on a pure tensor, the formula that determines it.
The inverse semi-local comparison sends a diagonal field element to 1 ⊗ x.
The semi-local decomposition is topological when the tensor product carries the module
topology over K_v. Both the comparison and its inverse are continuous.
Equations
- TauCeti.semilocalContinuousEquiv L v = { toAlgEquiv := TauCeti.semilocalEquiv L v, continuous_toFun := ⋯, continuous_invFun := ⋯ }
Instances For
Forgetting continuity recovers the algebraic semi-local decomposition.
The continuous semi-local comparison has the prescribed formula on pure tensors.
The inverse continuous comparison sends a diagonal field element to 1 ⊗ x.