Base change of adeles

The canonical map 𝔸_K ⊗[K] L → 𝔸_L for number fields L/K is an algebra equivalence over 𝔸_K. Its finite and infinite components are the corresponding local scalar-extension maps, after distributing the tensor product over the product defining 𝔸_K. When the source has its module topology over 𝔸_K, the map is a homeomorphism.

Bijectivity combines the finite-adele comparison finiteAdeleBaseChangeAlgEquiv with the archimedean comparison infiniteAdeleBaseChangeAlgEquiv. The inverse is continuous by the open mapping theorem for σ-compact groups.

Main definitions

• TauCeti.GlobalNumberFields.adeleBaseChangeHom: the canonical map 𝔸_K ⊗[K] L →ₐ[𝔸_K] 𝔸_L.
• TauCeti.GlobalNumberFields.adeleBaseChangeAlgEquiv: that map as an algebra equivalence.
• TauCeti.GlobalNumberFields.adeleBaseChangeEquiv: that map as a continuous algebra equivalence, for the module topology on the source.

Main results

• TauCeti.GlobalNumberFields.adeleBaseChangeHom_fst, TauCeti.GlobalNumberFields.adeleBaseChangeHom_snd: the infinite and finite components are the infinite- and finite-adele comparisons.
• TauCeti.GlobalNumberFields.adeleBaseChangeHom_bijective: the map is bijective.
• TauCeti.GlobalNumberFields.isOpenMap_adeleBaseChangeEquiv: the comparison sends open sets to open sets for the module topology.
• TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tmul_one, TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_apply_prod: the continuous comparison extends 𝔸_K → 𝔸_L and is the product of the infinite- and finite-adele comparisons.
• TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tower: in a tower K ⊆ L ⊆ M, base change from K to M factors through base change from K to L.

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (8.3).
• J. W. S. Cassels and A. Fröhlich, eds., Algebraic Number Theory, Chapter II, §14.

noncomputable def TauCeti.GlobalNumberFields.adeleBaseChangeHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L →ₐ[NumberField.AdeleRing (NumberField.RingOfIntegers K) K] NumberField.AdeleRing (NumberField.RingOfIntegers L) L

The canonical scalar-extension map of full adeles over the adele ring of the base field.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_tmul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (x : L) : (adeleBaseChangeHom K L) (a ⊗ₜ[K] x) = (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a * (algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x

A pure tensor maps to the extended adele times the diagonal field element.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_fst (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (t : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L) : ((adeleBaseChangeHom K L) t).1 = (infiniteAdeleBaseChangeHom K L) ((TensorProduct.prodLeft K K (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L) t).1

The infinite component of the full comparison is the infinite-adele comparison after splitting the source tensor product into its two components.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_snd (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (t : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L) : ((adeleBaseChangeHom K L) t).2 = (finiteAdeleBaseChangeHom K L) ((TensorProduct.prodLeft K K (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L) t).2

The finite component of the full comparison is the finite-adele comparison after splitting the source tensor product into its two components.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_injective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Function.Injective ⇑(adeleBaseChangeHom K L)

The canonical scalar-extension map of full adeles is injective.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_surjective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Function.Surjective ⇑(adeleBaseChangeHom K L)

The canonical scalar-extension map of full adeles is surjective.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeHom_bijective (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : Function.Bijective ⇑(adeleBaseChangeHom K L)

The canonical scalar-extension map of full adeles is bijective.

noncomputable def TauCeti.GlobalNumberFields.adeleBaseChangeAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L ≃ₐ[NumberField.AdeleRing (NumberField.RingOfIntegers K) K] NumberField.AdeleRing (NumberField.RingOfIntegers L) L

Base change of adeles is an algebra equivalence over the adele ring of the base field, independently of a topology on the tensor product.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeAlgEquiv_toAlgHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ↑(adeleBaseChangeAlgEquiv K L) = adeleBaseChangeHom K L

Forgetting invertibility recovers the canonical base-change homomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeAlgEquiv_symm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : L) : (adeleBaseChangeAlgEquiv K L).symm ((algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x) = 1 ⊗ₜ[K] x

The algebraic inverse comparison sends a diagonal field element to 1 ⊗ x.

theorem TauCeti.GlobalNumberFields.continuous_adeleBaseChangeHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] : Continuous ⇑(adeleBaseChangeHom K L)

The canonical full-adele comparison is continuous for the module topology over the base adele ring.

noncomputable def TauCeti.GlobalNumberFields.adeleBaseChangeEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L ≃A[NumberField.AdeleRing (NumberField.RingOfIntegers K) K] NumberField.AdeleRing (NumberField.RingOfIntegers L) L

Base change of adeles is a continuous algebra equivalence 𝔸_K ⊗[K] L ≃A[𝔸_K] 𝔸_L over the adele ring of the base field, for the module topology on the source.

theorem TauCeti.GlobalNumberFields.isOpenMap_adeleBaseChangeEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] : IsOpenMap ⇑(adeleBaseChangeEquiv K L)

The adelic base-change comparison maps open sets to open sets for the module topology on the tensor product.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_toAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] : (adeleBaseChangeEquiv K L).toAlgEquiv = adeleBaseChangeAlgEquiv K L

Forgetting continuity recovers the algebraic base-change equivalence.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tmul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (x : L) : (adeleBaseChangeEquiv K L) (a ⊗ₜ[K] x) = (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a * (algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x

The continuous comparison sends a pure tensor to the extended adele times the diagonal field element.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tmul_one (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) : (adeleBaseChangeEquiv K L) (a ⊗ₜ[K] 1) = (NumberField.adeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a

The continuous comparison restricts on 𝔸_K ⊗ 1 to the extension map 𝔸_K → 𝔸_L.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_apply_prod (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] (t : TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L) : (adeleBaseChangeEquiv K L) t = ((infiniteAdeleBaseChangeAlgEquiv K L) ((TensorProduct.prodLeft K K (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L) t).1, (finiteAdeleBaseChangeAlgEquiv K L) ((TensorProduct.prodLeft K K (NumberField.InfiniteAdeleRing K) (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L) t).2)

The continuous comparison is the pair of the infinite- and finite-adele comparisons, after splitting the source tensor product into its two components.

@[simp]

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_symm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] (x : L) : (adeleBaseChangeEquiv K L).symm ((algebraMap L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L)) x) = 1 ⊗ₜ[K] x

The inverse comparison sends a diagonal field element to 1 ⊗ x.

theorem TauCeti.GlobalNumberFields.adeleBaseChangeEquiv_tower (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) L)] (M : Type u_3) [Field M] [NumberField M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [TopologicalSpace (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) M)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (NumberField.AdeleRing (NumberField.RingOfIntegers K) K) M)] [TopologicalSpace (TensorProduct L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) M)] [IsModuleTopology (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) (TensorProduct L (NumberField.AdeleRing (NumberField.RingOfIntegers L) L) M)] (a : NumberField.AdeleRing (NumberField.RingOfIntegers K) K) (z : M) : (adeleBaseChangeEquiv K M) (a ⊗ₜ[K] z) = (adeleBaseChangeEquiv L M) ((adeleBaseChangeEquiv K L) (a ⊗ₜ[K] 1) ⊗ₜ[L] z)

Base change of adeles in a tower K ⊆ L ⊆ M: the comparison for M/K factors through the comparison for L/K, followed by the comparison for M/L.