This file constructs the homomorphism 𝓝 : I_K → ℝ₊ˣ. At a finite place a uniformizer contributes the norm of its prime ideal; at infinity we divide by the normalized archimedean norm. This is the convention for which principal ideles have norm one.
The norm of a unit in a normed field, as a positive real unit.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]def nnnormUnitHom (F : Type*) [NormedField F] :
Fˣ →* ℝ≥0ˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]theorem nnnormUnitHom_val (F : Type*) [NormedField F] (x : Fˣ) :
((nnnormUnitHom F x : ℝ≥0ˣ) : ℝ≥0) = ‖(x : F)‖₊The product of the normalized norms of all archimedean components.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGroupdef archimedeanNorm :
InfiniteIdeleGroup K →* ℝ≥0ˣ where
toFun a := ∏ w : InfinitePlace K,
nnnormUnitHom w.Completion (component w a) ^ w.mult
map_one' := by
apply Finset.prod_eq_one
intro w _
rw [map_one, map_one, one_pow]
map_mul' a b := by
simp only [map_mul, Finset.prod_mul_distrib, mul_pow]Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace InfiniteIdeleGrouptheorem archimedeanNorm_apply (a : InfiniteIdeleGroup K) :
archimedeanNorm a =
∏ w : InfinitePlace K,
nnnormUnitHom w.Completion (component w a) ^ w.multThe positive real unit given by the absolute norm of a finite prime.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroupdef primeNorm (v : HeightOneSpectrum (𝓞 K)) : ℝ≥0ˣThe homomorphism sending an integer exponent to the corresponding power of the absolute norm of a finite prime.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroupdef primeNormPowerHom (v : HeightOneSpectrum (𝓞 K)) :
Multiplicative ℤ →* ℝ≥0ˣThe norm of a finitely supported divisor.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroupdef divisorNorm :
Multiplicative (HeightOneSpectrum (𝓞 K) →₀ ℤ) →* ℝ≥0ˣThe finite part of the absolute idele norm.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGroupdef absoluteNorm :
FiniteIdeleGroup K →* ℝ≥0ˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace FiniteIdeleGrouptheorem absoluteNorm_apply (a : FiniteIdeleGroup K) :
absoluteNorm a =
(valuationVector a).toAdd.prod fun v n =>
primeNorm v ^ n := by
rflThe absolute norm on the idele group.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroupdef absoluteNorm :
IdeleGroup K →* ℝ≥0ˣSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGrouptheorem absoluteNorm_apply (a : IdeleGroup K) :
absoluteNorm a =
FiniteIdeleGroup.absoluteNorm a.2 *
(InfiniteIdeleGroup.archimedeanNorm a.1)⁻¹The norm-one ideles.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField RestrictedProduct NNReal
open NumberField IsDedekindDomain
noncomputable section
variable {K : Type*} [Field K] [NumberField K]
namespace IdeleGroupdef normOneSubgroup : Subgroup (IdeleGroup K)