Base change of infinite adeles

For a finite extension of number fields L/K, scalar extension identifies K∞ ⊗[K] L with L∞. The comparison is an algebra equivalence over K∞ and a homeomorphism when the tensor product carries the module topology over K∞. Its component at a place of L is the semilocal comparison at the place below it.

The construction assembles infiniteSemilocalEquiv through Mathlib's TensorProduct.piLeft. This includes the real-to-complex factors of local degree two. In a tower K ⊆ L ⊆ M, the comparison for M/K factors through the one for L/K (infiniteAdeleBaseChangeEquiv_tower).

References

• J. Neukirch, Algebraic Number Theory, Chapter II, Proposition (8.3).

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

The scalar-extension map of infinite adeles, using the completion maps at the places above each base place.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeHom_tmul (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (a : NumberField.InfiniteAdeleRing K) (x : L) : (infiniteAdeleBaseChangeHom K L) (a ⊗ₜ[K] x) = (NumberField.infiniteAdeleExtension K L) a * (algebraMap L (NumberField.InfiniteAdeleRing L)) x

On pure tensors, the base-change map multiplies the extended adele by the diagonal field element.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeHom_tmul_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (a : NumberField.InfiniteAdeleRing K) (x : L) (w : NumberField.InfinitePlace L) : (infiniteAdeleBaseChangeHom K L) (a ⊗ₜ[K] x) w = (NumberField.LiesOver.completionMap (w.comap (algebraMap K L)) w) (a (w.comap (algebraMap K L))) * (algebraMap L w.Completion) x

At a place of L, a pure tensor is evaluated using the completion map from the place below it and the local embedding of the field element.

def TauCeti.GlobalNumberFields.infiniteAdelePiLiesOverEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : NumberField.InfiniteAdeleRing L ≃+* ((v : NumberField.InfinitePlace K) → (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completion)

Infinite adeles grouped by places of the base field. The infinite adeles of L are the product over the infinite places v of K of the families of components at the places of L above v.

@[simp]

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

The family at v of a grouped infinite adele consists of its components above v.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdelePiLiesOverEquiv_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (a : (v : NumberField.InfinitePlace K) → (w : { w : NumberField.InfinitePlace L // w.LiesOver v }) → (↑w).Completion) (w : NumberField.InfinitePlace L) : (infiniteAdelePiLiesOverEquiv K L).symm a w = a (w.comap (algebraMap K L)) ⟨w, ⋯⟩

Ungrouping reads the component at a place w of L off the family at the place below w.

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

The archimedean semilocal decompositions assemble to a bijective base-change map.

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

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

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeAlgEquiv_toAlgHom (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] : ↑(infiniteAdeleBaseChangeAlgEquiv K L) = infiniteAdeleBaseChangeHom K L

Forgetting invertibility recovers the canonical base-change homomorphism.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeAlgEquiv_symm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] (x : L) : (infiniteAdeleBaseChangeAlgEquiv K L).symm ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = 1 ⊗ₜ[K] x

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

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

Base change of infinite adeles is a continuous algebra equivalence over the infinite adele ring of the base field. The source carries its module topology over that ring.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeEquiv_toAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] [IsModuleTopology (NumberField.InfiniteAdeleRing K) (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] : (infiniteAdeleBaseChangeEquiv K L).toAlgEquiv = infiniteAdeleBaseChangeAlgEquiv K L

Forgetting continuity recovers the algebraic base-change equivalence.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeEquiv_tmul (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] [IsModuleTopology (NumberField.InfiniteAdeleRing K) (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] (a : NumberField.InfiniteAdeleRing K) (x : L) : (infiniteAdeleBaseChangeEquiv K L) (a ⊗ₜ[K] x) = (NumberField.infiniteAdeleExtension K L) a * (algebraMap L (NumberField.InfiniteAdeleRing L)) x

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

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeEquiv_tmul_apply (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] [IsModuleTopology (NumberField.InfiniteAdeleRing K) (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] (a : NumberField.InfiniteAdeleRing K) (x : L) (w : NumberField.InfinitePlace L) : (infiniteAdeleBaseChangeEquiv K L) (a ⊗ₜ[K] x) w = (NumberField.LiesOver.completionMap (w.comap (algebraMap K L)) w) (a (w.comap (algebraMap K L))) * (algebraMap L w.Completion) x

At a place of L, the continuous comparison evaluates a pure tensor using the completion map from the place below it and the local embedding of the field element.

@[simp]

theorem TauCeti.GlobalNumberFields.infiniteAdeleBaseChangeEquiv_symm_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [TopologicalSpace (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] [IsModuleTopology (NumberField.InfiniteAdeleRing K) (TensorProduct K (NumberField.InfiniteAdeleRing K) L)] (x : L) : (infiniteAdeleBaseChangeEquiv K L).symm ((algebraMap L (NumberField.InfiniteAdeleRing L)) x) = 1 ⊗ₜ[K] x

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

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

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