The adele ring along a field extension

For an extension L / K, every infinite place w of L lies over its restriction w.comap (algebraMap K L) to K, and Mathlib's NumberField.LiesOver.completionMap is the continuous extension K_{w.comap (algebraMap K L)} → L_w of K → L. Placewise, these maps assemble into a ring homomorphism K_∞ → L_∞ of infinite adele rings. Together with the finite part IsDedekindDomain.finiteAdeleExtension, they give the extension map 𝔸_K → 𝔸_L of adele rings, which sends an adele (a_v)_v to (a_{v(w)})_w, where v(w) is the place of K below w.

These are the maps along which the adeles and ideles of K and L are compared, for instance under base change and norm.

Main results

• NumberField.infiniteAdeleExtension, NumberField.adeleExtension: the extension maps of infinite adele rings and of adele rings.
• NumberField.continuous_infiniteAdeleExtension, NumberField.continuous_adeleExtension: they are continuous.
• NumberField.infiniteAdeleExtension_algebraMap, NumberField.adeleExtension_algebraMap: they extend K → L along the diagonal embeddings.
• NumberField.eq_infiniteAdeleExtension_of_continuous: for a number field K, the infinite extension map is the only continuous ring homomorphism with that property, because K is dense in K_∞.
• NumberField.infiniteAdeleExtension_comp, NumberField.adeleExtension_comp, NumberField.infiniteAdeleExtension_self, NumberField.adeleExtension_self: the tower composition and identity laws.
• NumberField.infiniteAdeleExtensionAlgebra, NumberField.adeleExtensionAlgebra: the induced algebra structures, available in the corresponding scopes.

Provenance

These maps follow the FLT project's adele base-change construction (github.com/ImperialCollegeLondon/FLT, FLT/NumberField/InfiniteAdeleRing.lean and FLT/NumberField/AdeleRing.lean; Kevin Buzzard et al., Apache-2.0). The finite component is described more specifically in FiniteAdeleRing/Extension.lean.

noncomputable def NumberField.infiniteAdeleExtension (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : InfiniteAdeleRing K →+* InfiniteAdeleRing L

The extension map of infinite adele rings along L / K: the component at an infinite place w of L is the image of the component at w.comap (algebraMap K L) under the completion map K_{w.comap (algebraMap K L)} → L_w.

@[simp]

theorem NumberField.infiniteAdeleExtension_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (x : InfiniteAdeleRing K) (w : InfinitePlace L) : (infiniteAdeleExtension K L) x w = (LiesOver.completionMap (w.comap (algebraMap K L)) w) (x (w.comap (algebraMap K L)))

The component of infiniteAdeleExtension K L x at w is the image of the component of x at w.comap (algebraMap K L).

theorem NumberField.continuous_infiniteAdeleExtension (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Continuous ⇑(infiniteAdeleExtension K L)

The extension map of infinite adele rings is continuous.

@[simp]

theorem NumberField.infiniteAdeleExtension_algebraMap (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (x : K) : (infiniteAdeleExtension K L) ((algebraMap K (InfiniteAdeleRing K)) x) = (algebraMap L (InfiniteAdeleRing L)) ((algebraMap K L) x)

The extension map of infinite adele rings extends K → L along the diagonal embeddings.

theorem NumberField.eq_infiniteAdeleExtension_of_continuous (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] {f : InfiniteAdeleRing K →+* InfiniteAdeleRing L} (hf : Continuous ⇑f) (hfK : ∀ (x : K), f ((algebraMap K (InfiniteAdeleRing K)) x) = (algebraMap L (InfiniteAdeleRing L)) ((algebraMap K L) x)) : f = infiniteAdeleExtension K L

For a number field K, infiniteAdeleExtension is the only continuous ring homomorphism of infinite adele rings extending K → L along the diagonal embeddings: K is dense in K_∞, and L_∞ is Hausdorff.

@[simp]

theorem NumberField.infiniteAdeleExtension_comp (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (M : Type u_3) [Field M] [Algebra L M] [Algebra K M] [IsScalarTower K L M] : (infiniteAdeleExtension L M).comp (infiniteAdeleExtension K L) = infiniteAdeleExtension K M

The extension maps of infinite adele rings compose in a tower K ⊆ L ⊆ M.

@[simp]

theorem NumberField.infiniteAdeleExtension_self (K : Type u_1) [Field K] : infiniteAdeleExtension K K = RingHom.id (InfiniteAdeleRing K)

Extension of infinite adeles along the identity extension is the identity map.

@[reducible]

noncomputable def NumberField.infiniteAdeleExtensionAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Algebra (InfiniteAdeleRing K) (InfiniteAdeleRing L)

The algebra structure on infinite adeles induced by infiniteAdeleExtension, available in the InfiniteAdeleExtension scope.

@[simp]

theorem NumberField.algebraMap_infiniteAdeleExtensionAlgebra (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : algebraMap (InfiniteAdeleRing K) (InfiniteAdeleRing L) = infiniteAdeleExtension K L

The algebra map of infiniteAdeleExtensionAlgebra is the infinite extension map.

noncomputable def NumberField.adeleExtension (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] : AdeleRing R K →+* AdeleRing B L

The extension map of adele rings along an integral extension B / R of Dedekind domains with fraction fields L / K: infiniteAdeleExtension on the infinite component and finiteAdeleExtension on the finite component.

@[simp]

theorem NumberField.adeleExtension_fst {R : Type u_1} {K : Type u_2} {B : Type u_3} {L : Type u_4} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (a : AdeleRing R K) : ((adeleExtension R K B L) a).1 = (infiniteAdeleExtension K L) a.1

The infinite component of adeleExtension R K B L a is the infinite extension of the infinite component of a.

@[simp]

theorem NumberField.adeleExtension_snd {R : Type u_1} {K : Type u_2} {B : Type u_3} {L : Type u_4} [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (a : AdeleRing R K) : ((adeleExtension R K B L) a).2 = (IsDedekindDomain.finiteAdeleExtension R K B L) a.2

The finite component of adeleExtension R K B L a is the finite extension of the finite component of a.

theorem NumberField.continuous_adeleExtension (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] : Continuous ⇑(adeleExtension R K B L)

The extension map of adele rings is continuous.

@[simp]

theorem NumberField.adeleExtension_algebraMap (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (x : K) : (adeleExtension R K B L) ((algebraMap K (AdeleRing R K)) x) = (algebraMap L (AdeleRing B L)) ((algebraMap K L) x)

The extension map of adele rings extends K → L along the diagonal embeddings.

@[simp]

theorem NumberField.adeleExtension_comp (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] (C : Type u_5) (M : Type u_6) [CommRing C] [IsDedekindDomain C] [Algebra B C] [Algebra.IsIntegral B C] [Field M] [Algebra L M] [Algebra B M] [IsScalarTower B L M] [Algebra C M] [IsFractionRing C M] [IsScalarTower B C M] [Algebra R C] [Algebra.IsIntegral R C] [Algebra K M] [Algebra R M] [IsScalarTower R K M] [IsScalarTower R C M] [IsScalarTower K L M] : (adeleExtension B L C M).comp (adeleExtension R K B L) = adeleExtension R K C M

The extension maps of adele rings compose in a tower K ⊆ L ⊆ M.

@[simp]

theorem NumberField.adeleExtension_self (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : adeleExtension R K R K = RingHom.id (AdeleRing R K)

Extension of adeles along the identity extension is the identity map.

@[reducible]

noncomputable def NumberField.adeleExtensionAlgebra (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] : Algebra (AdeleRing R K) (AdeleRing B L)

The algebra structure on adeles induced by adeleExtension, available in the AdeleExtension scope.

@[simp]

theorem NumberField.algebraMap_adeleExtensionAlgebra (R : Type u_1) (K : Type u_2) (B : Type u_3) (L : Type u_4) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [CommRing B] [IsDedekindDomain B] [Algebra R B] [Algebra.IsIntegral R B] [Field L] [Algebra K L] [Algebra R L] [IsScalarTower R K L] [Algebra B L] [IsFractionRing B L] [IsScalarTower R B L] : algebraMap (AdeleRing R K) (AdeleRing B L) = adeleExtension R K B L

The algebra map of adeleExtensionAlgebra is the adele extension map.