Products of normalized absolute values over finite completions #
For an extension of number fields L/K, the canonical map K_v → L_w raises normalized
absolute values to the local degree [L_w : K_v]. Taking the product over w ∣ v raises
the norm to the global degree [L : K]. This is the finite-place input to the idele norm
formula for extension of scalars.
Main results #
TauCeti.prod_norm_adicCompletionExtension_eq_norm_pow: the product of the normalized absolute values of the images in all completions above a finite place.
References #
- [J. Neukirch, Algebraic Number Theory][Neukirch1992], Chapter II, §8.
@[simp]
theorem
TauCeti.prod_norm_adicCompletionExtension_eq_norm_pow
{K : Type u_1}
[Field K]
[NumberField K]
(L : Type u_2)
[Field L]
[NumberField L]
[Algebra K L]
(v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))
(x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
:
∏ w : { w : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers L) // w.asIdeal.LiesOver v.asIdeal },
‖(IsDedekindDomain.HeightOneSpectrum.adicCompletionExtension K L v ↑w) x‖ = ‖x‖ ^ Module.finrank K L
The product of the normalized absolute values of the images of x ∈ K_v in all the
completions above v is ‖x‖ ^ [L : K]. This includes x = 0.