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. 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

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.

theorem NumberField.FiniteAdeleRing.hasFiniteMulSupport_norm {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Field K] [Algebra R K] [IsFractionRing R K] (x : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) : Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum R) => ‖↑x v‖

theorem NumberField.FiniteAdeleRing.hasProd_zero_of_not_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients 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

theorem NumberField.FiniteAdeleRing.tprod_norm_eq_finprod_of_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients 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‖

theorem NumberField.FiniteAdeleRing.tprod_norm_eq_finprod_of_unit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients 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‖

theorem NumberField.FiniteAdeleRing.tprod_eq_zero_of_not_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Field K] [Algebra R K] [IsFractionRing R K] {x : IsDedekindDomain.FiniteAdeleRing R K} (hx : ¬IsUnit x) : ∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖ = 0

@[instance_reducible]

noncomputable instance NumberField.FiniteAdeleRing.instNormFiniteAdeleRing {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients 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

• NumberField.FiniteAdeleRing.instNormFiniteAdeleRing = { norm := fun (x : IsDedekindDomain.FiniteAdeleRing R K) => ∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖ }

theorem NumberField.FiniteAdeleRing.norm_def {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Field K] [Algebra R K] [IsFractionRing R K] (x : IsDedekindDomain.FiniteAdeleRing R K) : ‖x‖ = ∏' (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖

theorem NumberField.FiniteAdeleRing.norm_eq_finprod_of_unit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Field K] [Algebra R K] [IsFractionRing R K] (x : (IsDedekindDomain.FiniteAdeleRing R K)ˣ) : ‖↑x‖ = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ‖↑x v‖

theorem NumberField.FiniteAdeleRing.norm_eq_finprod_of_isUnit {R : Type u_1} {K : Type u_2} [CommRing R] [IsDedekindDomain R] [Ring.HasFiniteQuotients R] [Field K] [Algebra R K] [IsFractionRing R K] {x : IsDedekindDomain.FiniteAdeleRing R K} (hx : IsUnit x) : ‖x‖ = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), ‖x v‖

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

theorem NumberField.FiniteAdeleRing.unitEmbedding_norm_apply {K : Type u_2} [Field K] [NumberField K] (x : Kˣ) : ‖↑((IsDedekindDomain.FiniteAdeleRing.unitEmbedding (RingOfIntegers K) K) x)‖ = ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)), (FinitePlace.mk v) ↑x

theorem NumberField.FiniteAdeleRing.unitEmbedding_norm_apply_eq_finprod_finitePlace {K : Type u_2} [Field K] [NumberField K] (x : Kˣ) : ‖↑((IsDedekindDomain.FiniteAdeleRing.unitEmbedding (RingOfIntegers K) K) x)‖ = ∏ᶠ (v : FinitePlace K), v ↑x

theorem NumberField.FiniteAdeleRing.unitEmbedding_norm_eq_inv_abs_norm {K : Type u_2} [Field K] [NumberField K] (x : Kˣ) : ‖↑((IsDedekindDomain.FiniteAdeleRing.unitEmbedding (RingOfIntegers K) K) x)‖ = ↑|(Algebra.norm ℚ) ↑x|⁻¹

theorem NumberField.FiniteAdeleRing.coe_norm_eq_inv_abs_norm {K : Type u_2} [Field K] [NumberField K] {x : K} (hx : x ≠ 0) : ‖(algebraMap K (IsDedekindDomain.FiniteAdeleRing (RingOfIntegers K) K)) x‖ = ↑|(Algebra.norm ℚ) x|⁻¹