The semi-local component of an infinite adele

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

infiniteAdeleSemilocalHom L v : L_∞ → 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 infinite adeles along a tower L ⊆ M to id ⊗ (L → M), and the transport of infinite adeles along a K-isomorphism e to id ⊗ e. This is the archimedean counterpart of TauCeti.finiteAdeleSemilocalHom: it is how the components above v of adeles are mapped into extensions of K_v, for instance into a separable closure of K_v.

Taken over all infinite places v of K at once, these components identify the infinite adeles of L with ∏_v K_v ⊗[K] L (infiniteAdeleSemilocalEquiv), and the Galois action of σ ∈ Aut(L/K) on infinite adeles becomes id ⊗ σ on every factor. This is the decomposition of the infinite ideles L_∞ˣ into the semi-local units (K_v ⊗[K] L)ˣ.

Main definitions

• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom L v: the components above v of an infinite adele of L, as an element of K_v ⊗[K] L.
• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv K L: the ring isomorphism L_∞ ≃ ∏_v K_v ⊗[K] L given by the semi-local components above every infinite place of K.

Main results

• TauCeti.GlobalNumberFields.infiniteSemilocalEquiv_infiniteAdeleSemilocalHom: under the semi-local decomposition it is the family of components above v.
• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom_algebraMap: it sends x ∈ L to 1 ⊗ x.
• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom_infiniteAdeleExtension: naturality along a tower L ⊆ M.
• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom_infiniteAdeleEquiv: naturality under K-isomorphisms.
• TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_infiniteAdeleGaloisAction: under infiniteAdeleSemilocalEquiv, the Galois action is id ⊗ σ on each factor.

References

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

noncomputable def TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom {K : Type u_1} [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) : NumberField.InfiniteAdeleRing L →+* TensorProduct K v.Completion L

The semi-local component of an infinite adele. The components a_w of an infinite adele a of L at the places w of L above the infinite 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.GlobalNumberFields.infiniteAdeleSemilocalHom_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : NumberField.InfinitePlace K} (a : NumberField.InfiniteAdeleRing L) : (infiniteAdeleSemilocalHom L v) a = (infiniteSemilocalEquiv L v).symm fun (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) => a ↑w

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

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteSemilocalEquiv_infiniteAdeleSemilocalHom {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : NumberField.InfinitePlace K} (a : NumberField.InfiniteAdeleRing L) : (infiniteSemilocalEquiv L v) ((infiniteAdeleSemilocalHom L v) a) = fun (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) => a ↑w

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

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom_algebraMap {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] {v : NumberField.InfinitePlace K} (x : L) : (infiniteAdeleSemilocalHom L v) ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = 1 ⊗ₜ[K] x

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

The product over all infinite places

noncomputable def TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv (K : Type u_1) [Field K] [NumberField K] (L : Type u_2) [Field L] [NumberField L] [Algebra K L] : NumberField.InfiniteAdeleRing L ≃+* ((v : NumberField.InfinitePlace K) → TensorProduct K v.Completion L)

The infinite adeles are the product of the semi-local algebras. Grouping the infinite places of L by the infinite place of K below them (infiniteAdelePiLiesOverEquiv), the semi-local components identify the infinite adeles of L with ∏_v K_v ⊗[K] L, the product over the infinite places v of K.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (a : NumberField.InfiniteAdeleRing L) (v : NumberField.InfinitePlace K) : (infiniteAdeleSemilocalEquiv K L) a v = (infiniteAdeleSemilocalHom L v) a

The component at v of infiniteAdeleSemilocalEquiv is the semi-local component above v.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_symm_apply {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (y : (v : NumberField.InfinitePlace K) → TensorProduct K v.Completion L) (w : NumberField.InfinitePlace L) : (infiniteAdeleSemilocalEquiv K L).symm y w = (infiniteSemilocalEquiv L (w.comap (algebraMap K L))) (y (w.comap (algebraMap K L))) ⟨w, ⋯⟩

The inverse of infiniteAdeleSemilocalEquiv reads the component at a place w of L off the semi-local factor at the place below w.

Naturality

theorem TauCeti.GlobalNumberFields.infiniteAdeleSemilocalHom_infiniteAdeleEquiv {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) {M : Type u_3} [Field M] [NumberField M] [Algebra K M] (e : L ≃ₐ[K] M) (a : NumberField.InfiniteAdeleRing L) : (infiniteAdeleSemilocalHom M v) ((infiniteAdeleEquiv L M e.toRingEquiv) a) = (Algebra.TensorProduct.map (AlgHom.id v.Completion v.Completion) ↑e) ((infiniteAdeleSemilocalHom L v) a)

Naturality under isomorphisms: transporting an infinite 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.GlobalNumberFields.infiniteAdeleSemilocalHom_infiniteAdeleExtension {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (v : NumberField.InfinitePlace K) {M : Type u_3} [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (a : NumberField.InfiniteAdeleRing L) : (infiniteAdeleSemilocalHom M v) ((NumberField.infiniteAdeleExtension L M) a) = (Algebra.TensorProduct.map (AlgHom.id v.Completion v.Completion) (IsScalarTower.toAlgHom K L M)) ((infiniteAdeleSemilocalHom L v) a)

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

theorem TauCeti.GlobalNumberFields.infiniteAdeleSemilocalEquiv_infiniteAdeleGaloisAction {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L] (σ : Gal(L/K)) (a : NumberField.InfiniteAdeleRing L) (v : NumberField.InfinitePlace K) : (infiniteAdeleSemilocalEquiv K L) (((infiniteAdeleGaloisAction K L) σ) a) v = ((Algebra.TensorProduct.baseChangeAutHom v.Completion L) σ) ((infiniteAdeleSemilocalEquiv K L) a v)

The Galois action on the semi-local decomposition. Under infiniteAdeleSemilocalEquiv, the Galois action of σ ∈ Aut(L/K) on infinite adeles applies the base change id ⊗ σ to each semi-local factor K_v ⊗[K] L.