The adele ring of a number field

This file contains the formalisation of the adele ring of a number field as the direct product of the infinite adele ring and the finite adele ring.

Main definitions

• NumberField.AdeleRing K is the adele ring of a number field K.
• NumberField.AdeleRing.principalSubgroup K is the subgroup of principal adeles (x)ᵥ.

References

• J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory

Tags

adele ring, number field

The adele ring

def NumberField.AdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_2 u_1)

AdeleRing (𝓞 K) K is the adele ring of a number field K.

More generally AdeleRing R K can be used if K is the field of fractions of the Dedekind domain R. This enables use of rings like AdeleRing ℤ ℚ, which in practice are easier to work with than AdeleRing (𝓞 ℚ) ℚ.

Note that this definition does not give the correct answer in the function field case.

Equations

• NumberField.AdeleRing R K = (NumberField.InfiniteAdeleRing K × IsDedekindDomain.FiniteAdeleRing R K)

@[instance_reducible]

noncomputable instance NumberField.instCommRingAdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : CommRing (AdeleRing R K)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance NumberField.instTopologicalSpaceAdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : TopologicalSpace (AdeleRing R K)

Equations

• NumberField.instTopologicalSpaceAdeleRing R K = NumberField.instTopologicalSpaceAdeleRing._aux_1 R K

instance NumberField.instIsTopologicalRingAdeleRing (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : IsTopologicalRing (AdeleRing R K)

@[instance_reducible]

noncomputable instance NumberField.instAlgebraAdeleRing (R : Type u_2) (K : Type u_1) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Algebra K (AdeleRing R K)

Equations

• NumberField.instAlgebraAdeleRing R K = { smul := NumberField.instAlgebraAdeleRing._aux_1 R K, algebraMap := NumberField.instAlgebraAdeleRing._aux_3 R K, commutes' := ⋯, smul_def' := ⋯ }

def NumberField.AdeleRing.«term𝔸ᶠ[_]» : Lean.ParserDescr

𝔸ᶠ[K] is notation for IsDedekindDomain.FiniteAdeleRing (𝓞 K) K.

Equations

• One or more equations did not get rendered due to their size.

def NumberField.AdeleRing.«term𝔸[_,_]» : Lean.ParserDescr

𝔸[R, K] is notation for NumberField.AdeleRing R K.

Equations

• One or more equations did not get rendered due to their size.

def NumberField.AdeleRing.«term𝔸[_]» : Lean.ParserDescr

𝔸[K] is notation for NumberField.AdeleRing (𝓞 K) K.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance NumberField.AdeleRing.instInhabited (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Inhabited (AdeleRing R K)

Equations

• NumberField.AdeleRing.instInhabited R K = { default := 0 }

@[simp]

theorem NumberField.AdeleRing.algebraMap_fst_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : K) (v : InfinitePlace K) : ((algebraMap K (AdeleRing R K)) x).1 v = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }

@[simp]

theorem NumberField.AdeleRing.algebraMap_snd_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (x : K) (v : IsDedekindDomain.HeightOneSpectrum R) : ((algebraMap K (AdeleRing R K)) x).2 v = { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) }

theorem NumberField.AdeleRing.algebraMap_injective (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [NumberField K] : Function.Injective ⇑(algebraMap K (AdeleRing R K))

noncomputable def NumberField.AdeleRing.ofCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) : v.Completion →* AdeleRing R K

The embedding of the completion Kᵥ at an infinite place v into the adele ring.

Equations

• NumberField.AdeleRing.ofCompletion R K v = (NumberField.InfiniteAdeleRing.ofCompletion v).prod 1

@[simp]

theorem NumberField.AdeleRing.ofCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) (i : v.Completion) : (ofCompletion R K v) i = ((InfiniteAdeleRing.ofCompletion v) i, 1)

noncomputable def NumberField.AdeleRing.ofAdicCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v →* AdeleRing R K

The embedding of the completion Kᵥ at a finite place v into the adele ring.

Equations

• NumberField.AdeleRing.ofAdicCompletion R K v = MonoidHom.prod 1 (IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion K v)

@[simp]

theorem NumberField.AdeleRing.ofAdicCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (i : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v) : (ofAdicCompletion R K v) i = (1, (IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion K v) i)

@[reducible, inline]

noncomputable abbrev NumberField.AdeleRing.principalSubgroup (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : AddSubgroup (AdeleRing R K)

The subgroup of principal adeles (x)ᵥ where x ∈ K.

Equations

• NumberField.AdeleRing.principalSubgroup R K = (algebraMap K (NumberField.AdeleRing R K)).range.toAddSubgroup

@[reducible, inline]

abbrev NumberField.IdeleGroup (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max u_2 u_1)

The idele group is the group of units of the adele ring.

Equations

• NumberField.IdeleGroup R K = (NumberField.AdeleRing R K)ˣ

noncomputable def NumberField.IdeleGroup.unitEmbedding (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Kˣ →* IdeleGroup R K

The map from Kˣ to the idele group of K. The image is the subgroup of principal ideles.

Equations

• NumberField.IdeleGroup.unitEmbedding R K = Units.map ↑(algebraMap K (NumberField.AdeleRing R K))

@[simp]

theorem NumberField.IdeleGroup.val_inv_unitEmbedding_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (u : Kˣ) : ↑((unitEmbedding R K) u)⁻¹ = (algebraMap K (AdeleRing R K)) (↑u)⁻¹

@[simp]

theorem NumberField.IdeleGroup.val_unitEmbedding_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (u : Kˣ) : ↑((unitEmbedding R K) u) = (algebraMap K (AdeleRing R K)) ↑u

noncomputable def NumberField.IdeleGroup.ofCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) : v.Completionˣ →* IdeleGroup R K

The map from the completion Kᵥ at an infinite place v to the idele group.

Equations

• NumberField.IdeleGroup.ofCompletion R K v = Units.map (NumberField.AdeleRing.ofCompletion R K v)

@[simp]

theorem NumberField.IdeleGroup.val_ofCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) (u : v.Completionˣ) : ↑((ofCompletion R K v) u) = ((InfiniteAdeleRing.ofCompletion v) ↑u, 1)

@[simp]

theorem NumberField.IdeleGroup.val_inv_ofCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) (u : v.Completionˣ) : ↑((ofCompletion R K v) u)⁻¹ = ((InfiniteAdeleRing.ofCompletion v) (↑u)⁻¹, 1)

noncomputable def NumberField.IdeleGroup.ofAdicCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ →* IdeleGroup R K

The map from the completion Kᵥ at a finite place v to the idele group.

Equations

• NumberField.IdeleGroup.ofAdicCompletion R K v = Units.map (NumberField.AdeleRing.ofAdicCompletion R K v)

@[simp]

theorem NumberField.IdeleGroup.val_inv_ofAdicCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : ↑((ofAdicCompletion R K v) u)⁻¹ = (1, (IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion K v) (↑u)⁻¹)

@[simp]

theorem NumberField.IdeleGroup.val_ofAdicCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : ↑((ofAdicCompletion R K v) u) = (1, (IsDedekindDomain.FiniteAdeleRing.ofAdicCompletion K v) ↑u)

@[reducible, inline]

noncomputable abbrev NumberField.IdeleGroup.principalSubgroup (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Subgroup (IdeleGroup R K)

The subgroup of principal ideles (x)ᵥ where x ∈ Kˣ.

Equations

• NumberField.IdeleGroup.principalSubgroup R K = (NumberField.IdeleGroup.unitEmbedding R K).range

@[reducible, inline]

abbrev NumberField.IdeleClassGroup (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] : Type (max (max u_2 u_1) u_1 u_2)

The idele class group is the quotient of the idele group by the subgroup of principal ideles.

Equations

• NumberField.IdeleClassGroup R K = (NumberField.IdeleGroup R K ⧸ NumberField.IdeleGroup.principalSubgroup R K)

noncomputable def NumberField.IdeleClassGroup.ofCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) : v.Completionˣ →* IdeleClassGroup R K

The map from the completion Kᵥ at an infinite place v to the idele class group.

Equations

• NumberField.IdeleClassGroup.ofCompletion R K v = (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup R K)).comp (NumberField.IdeleGroup.ofCompletion R K v)

@[simp]

theorem NumberField.IdeleClassGroup.ofCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : InfinitePlace K) (x : v.Completionˣ) : (ofCompletion R K v) x = ↑((IdeleGroup.ofCompletion R K v) x)

noncomputable def NumberField.IdeleClassGroup.ofAdicCompletion (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ →* IdeleClassGroup R K

The map from the completion Kᵥ at a finite place v to the idele class group.

Equations

• NumberField.IdeleClassGroup.ofAdicCompletion R K v = (QuotientGroup.mk' (NumberField.IdeleGroup.principalSubgroup R K)).comp (NumberField.IdeleGroup.ofAdicCompletion R K v)

@[simp]

theorem NumberField.IdeleClassGroup.ofAdicCompletion_apply (R : Type u_1) (K : Type u_2) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)ˣ) : (ofAdicCompletion R K v) x = ↑((IdeleGroup.ofAdicCompletion R K v) x)