The semi-local component of a finite adele

Let L/K be an extension of number fields and v a finite place of K. A finite adele a of L has a component a_w ∈ L_w at each of the finitely many places w of L above v. Read through the semi-local decomposition K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w (TauCeti.semilocalEquiv), this family is an element of the scalar extension K_v ⊗[K] L, and

finiteAdeleSemilocalHom L v : 𝔸_L^f → K_v ⊗[K] L

is a ring homomorphism. It sends a diagonal field element x ∈ L to 1 ⊗ x, and it is natural: it carries the extension map of finite adeles along a tower L ⊆ M to id ⊗ (L → M), and the transport of finite adeles along a K-automorphism σ of L to id ⊗ σ. The ring K_v ⊗[K] L receives K-algebra maps out of L more easily than the product of completions does, so this is how the components above v of adeles are mapped into extensions of K_v, for instance into a separable closure of K_v.

On units, the components above v of a finite idele form a unit of K_v ⊗[K] L (finiteIdeleSemilocalHom), and a finite idele is determined by these semi-local components. Conversely, a family of semi-local units which are integral at all but finitely many places is the family of semi-local components of a finite idele (finiteIdeleOfSemilocalUnits).

Main definitions

• TauCeti.finiteAdeleSemilocalHom L v: the components above v of a finite adele of L, as an element of K_v ⊗[K] L.
• TauCeti.finiteIdeleSemilocalHom L v: the components above v of a finite idele of L, as a unit of K_v ⊗[K] L.
• TauCeti.finiteIdeleOfSemilocalUnits: the finite idele with prescribed semi-local components.

Main results

• TauCeti.semilocalEquiv_finiteAdeleSemilocalHom: under the semi-local decomposition it is the family of components above v.
• TauCeti.finiteAdeleSemilocalHom_algebraMap: it sends x ∈ L to 1 ⊗ x.
• TauCeti.finiteAdeleSemilocalHom_finiteAdeleExtension: naturality along a tower L ⊆ M.
• TauCeti.finiteAdeleSemilocalHom_finiteAdeleEquiv: naturality under K-automorphisms of L.
• TauCeti.eq_of_forall_finiteIdeleSemilocalHom_eq: a finite idele is determined by its semi-local components.
• TauCeti.finiteIdeleSemilocalHom_map_finiteAdeleGaloisAction: taking semi-local components of finite ideles is Galois equivariant.

References

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

noncomputable def TauCeti.finiteAdeleSemilocalHom {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)) : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L →+* TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L

The semi-local component of a finite adele. The components a_w of a finite adele a of L at the places w of L above the finite place v of K, read in K_v ⊗[K] L through the semi-local decomposition K_v ⊗[K] L ≃ ∏_{w ∣ v} L_w.

theorem TauCeti.finiteAdeleSemilocalHom_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)} (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : (finiteAdeleSemilocalHom L v) a = (semilocalEquiv L v).symm fun (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) => a ↑w

The semi-local component of a finite adele is the inverse semi-local decomposition of its family of components at the places above v.

@[simp]

theorem TauCeti.semilocalEquiv_finiteAdeleSemilocalHom {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.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : (semilocalEquiv L v) ((finiteAdeleSemilocalHom L v) a) = fun (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) => a ↑w

Under the semi-local decomposition, the semi-local component of a finite adele is its family of components at the places above v.

@[simp]

theorem TauCeti.finiteAdeleSemilocalHom_algebraMap {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)} (x : L) : (finiteAdeleSemilocalHom L v) ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = 1 ⊗ₜ[K] x

The semi-local component of a diagonal field element x is 1 ⊗ x.

Naturality

theorem TauCeti.finiteAdeleSemilocalHom_finiteAdeleEquiv {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)) {M : Type u_3} [Field M] [NumberField M] [Algebra K M] (e : L ≃ₐ[K] M) (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : (finiteAdeleSemilocalHom M v) ((GlobalNumberFields.finiteAdeleEquiv L M e.toRingEquiv) a) = (Algebra.TensorProduct.map (AlgHom.id (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) ↑e) ((finiteAdeleSemilocalHom L v) a)

Naturality under isomorphisms: transporting a finite adele of L along a K-algebra isomorphism e : L ≃ M, for instance a K-automorphism of L, applies id ⊗ e to its semi-local component.

theorem TauCeti.finiteAdeleSemilocalHom_finiteAdeleExtension {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)) {M : Type u_3} [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) : (finiteAdeleSemilocalHom M v) ((IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers L) L (NumberField.RingOfIntegers M) M) a) = (Algebra.TensorProduct.map (AlgHom.id (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) (IsScalarTower.toAlgHom K L M)) ((finiteAdeleSemilocalHom L v) a)

Naturality along a tower L ⊆ M: the semi-local component of the extension to M of a finite adele of L is the image of its semi-local component under id ⊗ (L → M).

The semi-local components of a finite idele

noncomputable def TauCeti.finiteIdeleSemilocalHom {K : Type u} [Field K] [NumberField K] (L : Type u) [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ →* (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ

The semi-local component of a finite idele. The components of a finite idele of L at the places of L above the finite place v of K, as a unit of K_v ⊗[K] L.

@[simp]

theorem TauCeti.coe_finiteIdeleSemilocalHom {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ) : ↑((finiteIdeleSemilocalHom L v) a) = (finiteAdeleSemilocalHom L v) ↑a

The semi-local component of a finite idele, as a unit of K_v ⊗[K] L, has the semi-local component of the underlying finite adele as its value.

theorem TauCeti.semilocalEquiv_finiteIdeleSemilocalHom {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) : (semilocalEquiv L v) (↑((finiteIdeleSemilocalHom L v) a)) w = ↑a ↑w

Under the semi-local decomposition, the semi-local component of a finite idele is its family of components at the places above v.

theorem TauCeti.eq_of_forall_finiteIdeleSemilocalHom_eq {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {a b : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ} (h : ∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), (finiteIdeleSemilocalHom L v) a = (finiteIdeleSemilocalHom L v) b) : a = b

A finite idele is determined by its semi-local components.

theorem TauCeti.finiteIdeleSemilocalHom_map_finiteAdeleGaloisAction {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (σ : Gal(L/K)) (a : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ) : (finiteIdeleSemilocalHom L v) ((Units.map ↑((GlobalNumberFields.finiteAdeleGaloisAction K L) σ)) a) = (Units.map ↑((Algebra.TensorProduct.baseChangeAutHom (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L) σ)) ((finiteIdeleSemilocalHom L v) a)

Taking semi-local components is Galois equivariant. The semi-local component of the transport of a finite idele along σ ∈ Aut(L/K) is the image of its semi-local component under id ⊗ σ.

noncomputable def TauCeti.finiteIdeleOfSemilocalUnits {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (y : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ) (hy : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, y v ∈ semilocalIntegralUnits L v) : (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)ˣ

The finite idele with prescribed semi-local components. A family of units y v ∈ (K_v ⊗[K] L)ˣ, integral in every component for all but finitely many v, assembles to a finite idele of L whose component at a place w above v is the component of y v at w.

@[simp]

theorem TauCeti.coe_finiteIdeleOfSemilocalUnits_apply {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] (y : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ) (hy : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, y v ∈ semilocalIntegralUnits L v) (w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L)) : ↑(finiteIdeleOfSemilocalUnits y hy) w = (semilocalEquiv L (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w)) ↑(y (IsDedekindDomain.HeightOneSpectrum.under (NumberField.RingOfIntegers K) w)) ⟨w, ⋯⟩

The component of finiteIdeleOfSemilocalUnits y hy at a place w of L is the component at w of the prescribed unit y v, for v the place of K below w.

@[simp]

theorem TauCeti.finiteIdeleSemilocalHom_finiteIdeleOfSemilocalUnits {K : Type u} [Field K] [NumberField K] {L : Type u} [Field L] [NumberField L] [Algebra K L] {v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)} (y : (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → (TensorProduct K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) L)ˣ) (hy : ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) in Filter.cofinite, y v ∈ semilocalIntegralUnits L v) : (finiteIdeleSemilocalHom L v) (finiteIdeleOfSemilocalUnits y hy) = y v

The semi-local components of finiteIdeleOfSemilocalUnits y hy are the prescribed units y v.