The finite adele ring along an integral extension of Dedekind domains

Let B / R be an integral extension of Dedekind domains with fraction fields L / K. Every height-one prime w of B lies over the height-one prime w.under R of R, and the completion maps K_{w.under R} → L_w (HeightOneSpectrum.adicCompletionExtension) carry integers to integers. Placewise, they assemble into a ring homomorphism of finite adele rings 𝔸_K^∞ → 𝔸_L^∞, sending (a_v)_v to (a_{w.under R})_w. The restricted-product condition is preserved because only finitely many primes of B lie over each prime of R.

This is the map along which the finite adeles and finite ideles of K and L are compared, for instance under base change and norm.

Main results

• IsDedekindDomain.finiteAdeleExtension: the extension map 𝔸_K^∞ →+* 𝔸_L^∞.
• IsDedekindDomain.continuous_finiteAdeleExtension: it is continuous.
• IsDedekindDomain.finiteAdeleExtension_algebraMap: it extends K → L along the diagonal embeddings.
• IsDedekindDomain.eq_finiteAdeleExtension_of_continuous: it is the only continuous ring homomorphism with that property, because K is dense in its finite adeles.
• IsDedekindDomain.finiteAdeleExtension_comp, IsDedekindDomain.finiteAdeleExtension_self: the tower composition and identity laws.
• IsDedekindDomain.finiteAdeleExtensionAlgebra: the induced algebra structure, available in the FiniteAdeleExtension scope.

Provenance

The placewise construction follows the FLT project's finite-adele base change (FLT/DedekindDomain/FiniteAdeleRing/BaseChange.lean, FiniteAdeleRing.mapRingHom and its continuity lemma; Kevin Buzzard et al., Apache-2.0).

noncomputable def IsDedekindDomain.finiteAdeleExtension (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] : FiniteAdeleRing R K →+* FiniteAdeleRing B L

The extension map of finite adele rings along an integral extension B / R of Dedekind domains: the component at a height-one prime w of B is the image of the component at w.under R under the completion map K_{w.under R} → L_w.

@[simp]

theorem IsDedekindDomain.finiteAdeleExtension_apply {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 : FiniteAdeleRing R K) (w : HeightOneSpectrum B) : ((finiteAdeleExtension R K B L) a) w = (HeightOneSpectrum.adicCompletionExtension K L (HeightOneSpectrum.under R w) w) (a (HeightOneSpectrum.under R w))

The component of finiteAdeleExtension R K B L a at w is the image of the component of a at w.under R.

theorem IsDedekindDomain.continuous_finiteAdeleExtension (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 ⇑(finiteAdeleExtension R K B L)

The extension map of finite adele rings is continuous.

@[simp]

theorem IsDedekindDomain.finiteAdeleExtension_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) : (finiteAdeleExtension R K B L) ((algebraMap K (FiniteAdeleRing R K)) x) = (algebraMap L (FiniteAdeleRing B L)) ((algebraMap K L) x)

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

theorem IsDedekindDomain.eq_finiteAdeleExtension_of_continuous (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] {f : FiniteAdeleRing R K →+* FiniteAdeleRing B L} (hf : Continuous ⇑f) (hfK : ∀ (x : K), f ((algebraMap K (FiniteAdeleRing R K)) x) = (algebraMap L (FiniteAdeleRing B L)) ((algebraMap K L) x)) : f = finiteAdeleExtension R K B L

finiteAdeleExtension is the only continuous ring homomorphism of finite adele rings extending K → L along the diagonal embeddings: by strong approximation K is dense in its finite adeles, and the finite adeles of L are Hausdorff.

@[simp]

theorem IsDedekindDomain.finiteAdeleExtension_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] : (finiteAdeleExtension B L C M).comp (finiteAdeleExtension R K B L) = finiteAdeleExtension R K C M

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

@[simp]

theorem IsDedekindDomain.finiteAdeleExtension_self (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : finiteAdeleExtension R K R K = RingHom.id (FiniteAdeleRing R K)

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

@[reducible]

noncomputable def IsDedekindDomain.finiteAdeleExtensionAlgebra (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 (FiniteAdeleRing R K) (FiniteAdeleRing B L)

The algebra structure on finite adeles induced by finiteAdeleExtension, available in the FiniteAdeleExtension scope.

@[simp]

theorem IsDedekindDomain.algebraMap_finiteAdeleExtensionAlgebra (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 (FiniteAdeleRing R K) (FiniteAdeleRing B L) = finiteAdeleExtension R K B L

The algebra map of finiteAdeleExtensionAlgebra is the finite extension map.