Base change of finite adeles

For number fields L/K, the canonical map from 𝔸ᶠ_K ⊗[K] L to 𝔸ᶠ_L multiplies an extended adele by a diagonal field element. It is an algebra equivalence over 𝔸ᶠ_K, and a homeomorphism when the source carries its module topology over 𝔸ᶠ_K.

Injectivity holds because the semilocal decomposition at every finite place detects the coordinates of a tensor in any scalar-extended field basis. For surjectivity, write the components of a finite adele of L above each finite place v of K in an integral basis b of L, as ∑ i, c_i ⊗ b_i with c_i ∈ K_v. At the cofinitely many places where those components are integral, the integral semilocal decomposition 𝒪_v ⊗[𝓞 K] 𝓞 L ≃ ∏_{w ∣ v} 𝒪_w lets the c_i be chosen in 𝒪_v, so they assemble to finite adeles of K. The inverse is continuous by the open mapping theorem for σ-compact groups, as for the infinite-adele comparison in TauCeti.NumberTheory.NumberField.Global.Adeles.InfiniteBaseChange.

Main definitions

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

Main results

• TauCeti.GlobalNumberFields.finiteAdeleBaseChangeHom_apply: the components above v are the semilocal map after evaluation at v.
• TauCeti.GlobalNumberFields.finiteAdeleBaseChangeHom_injective, TauCeti.GlobalNumberFields.finiteAdeleBaseChangeHom_surjective: the map is bijective.
• TauCeti.GlobalNumberFields.finiteAdeleBaseChangeEquiv_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.finiteAdeleBaseChangeHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L →ₐ[IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K] IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L

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

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeHom_tmul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (x : L) : (finiteAdeleBaseChangeHom K L) (a ⊗ₜ[K] x) = (IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a * (algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x

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

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeHom_apply (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (s : TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal }) : ((finiteAdeleBaseChangeHom K L) s) ↑w = (semilocalHom L v) ((TensorProduct.map (↑(IsDedekindDomain.FiniteAdeleRing.proj K v)).toLinearMap LinearMap.id) s) w

The component above v of the finite-adele comparison is the semilocal map after scalar extension of evaluation at v.

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

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

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

The canonical scalar-extension map of finite adeles is surjective: every finite adele of L is a sum of finite adeles of K times elements of L.

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

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

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

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

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeAlgEquiv_toAlgHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] : ↑(finiteAdeleBaseChangeAlgEquiv K L) = finiteAdeleBaseChangeHom K L

Forgetting invertibility recovers the canonical base-change homomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeAlgEquiv_symm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] (x : L) : (finiteAdeleBaseChangeAlgEquiv K L).symm ((algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x) = 1 ⊗ₜ[K] x

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

theorem TauCeti.GlobalNumberFields.continuous_finiteAdeleBaseChangeHom (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] : Continuous ⇑(finiteAdeleBaseChangeHom K L)

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

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

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

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeEquiv_toAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] : (finiteAdeleBaseChangeEquiv K L).toAlgEquiv = finiteAdeleBaseChangeAlgEquiv K L

Forgetting continuity recovers the algebraic base-change equivalence.

@[simp]

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeEquiv_tmul (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (x : L) : (finiteAdeleBaseChangeEquiv K L) (a ⊗ₜ[K] x) = (IsDedekindDomain.finiteAdeleExtension (NumberField.RingOfIntegers K) K (NumberField.RingOfIntegers L) L) a * (algebraMap L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L)) x

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

@[simp]

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

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

theorem TauCeti.GlobalNumberFields.finiteAdeleBaseChangeEquiv_tower (K : Type u_1) (L : Type u_2) [Field K] [NumberField K] [Field L] [NumberField L] [Algebra K L] [TopologicalSpace (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) L)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (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 (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) M)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (TensorProduct K (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) M)] [TopologicalSpace (TensorProduct L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) M)] [IsModuleTopology (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) (TensorProduct L (IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers L) L) M)] (a : IsDedekindDomain.FiniteAdeleRing (NumberField.RingOfIntegers K) K) (z : M) : (finiteAdeleBaseChangeEquiv K M) (a ⊗ₜ[K] z) = (finiteAdeleBaseChangeEquiv L M) ((finiteAdeleBaseChangeEquiv K L) (a ⊗ₜ[K] 1) ⊗ₜ[L] z)

Base change of finite 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.