The finite adele ring of a number field #

This file concerns the finite adele ring of a Dedekind domain R and its field of fractions under the assumption that Ring.HasFiniteQuotients R and Infinite R. Later, these results are applied to the case where K is a number field and R is 𝓞 K.

Main definitions #

NumberField.FiniteAdeleRing.instNormFiniteAdeleRing : the norm on the finite adele ring.

Tags #

adele ring, number field

source

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.

Instances For

source

theorem NumberField.FiniteAdeleRing.hasFiniteMulSupport_norm {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] (x : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) :

Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ‖↑x v‖

source

theorem NumberField.FiniteAdeleRing.hasProd_zero_of_not_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] {x : IsDedekindDomain.FiniteAdeleRing R K} (hx : ¬IsUnit x) :

HasProd (fun (v : IsDedekindDomain.HeightOneSpectrum R) => ‖x v‖) 0

source

theorem NumberField.FiniteAdeleRing.tprod_norm_eq_finprod_of_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] {x : IsDedekindDomain.FiniteAdeleRing R K} (hx : IsUnit x) :

∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖ = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖

source

theorem NumberField.FiniteAdeleRing.tprod_norm_eq_finprod_of_unit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] (x : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) :

∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖↑x v‖ = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ‖↑x v‖

source

theorem NumberField.FiniteAdeleRing.tprod_eq_zero_of_not_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] {x : IsDedekindDomain.FiniteAdeleRing R K} (hx : ¬IsUnit x) :

∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖ = 0

source

@[instance_reducible]

noncomputable instance NumberField.FiniteAdeleRing.instNormFiniteAdeleRing {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Infinite R] [Field K] [Algebra R K] [IsFractionRing R K] :

Norm (IsDedekindDomain.FiniteAdeleRing R K)

The norm on the finite adele ring is the product of all the local norms. If a finite adele is a unit, then this is a finite product in disguise. Otherwise, it is zero (and not the junk tprod value of 1).

Equations