Norm in number fields #
Given a finite extension of number fields, we define the norm morphism as a function between the rings of integers.
Main definitions #
ring_of_integers.norm K:algebra.normas a morphism(𝓞 L) →* (𝓞 K).
Main results #
algebra.dvd_norm: ifL/Kis a finite Galois extension of fields, then, for all(x : 𝓞 L)we have thatx ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x).
@[simp]
theorem
ring_of_integers.norm_apply_coe
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_separable K L]
(n : ↥(number_field.ring_of_integers L)) :
↑(⇑(ring_of_integers.norm K) n) = ⇑(algebra.norm K) ↑n
noncomputable
def
ring_of_integers.norm
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_separable K L] :
algebra.norm as a morphism betwen the rings of integers.
Equations
theorem
ring_of_integers.coe_algebra_map_norm
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_separable K L]
(x : ↥(number_field.ring_of_integers L)) :
↑(⇑(algebra_map ↥(number_field.ring_of_integers K) ↥(number_field.ring_of_integers L)) (⇑(ring_of_integers.norm K) x)) = ⇑(algebra_map K L) (⇑(algebra.norm K) ↑x)
theorem
ring_of_integers.is_unit_norm
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_galois K L]
{x : ↥(number_field.ring_of_integers L)} :
is_unit (⇑(ring_of_integers.norm K) x) ↔ is_unit x
theorem
ring_of_integers.dvd_norm
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
[is_galois K L]
(x : ↥(number_field.ring_of_integers L)) :
x ∣ ⇑(algebra_map ↥(number_field.ring_of_integers K) ↥(number_field.ring_of_integers L)) (⇑(ring_of_integers.norm K) x)
If L/K is a finite Galois extension of fields, then, for all (x : 𝓞 L) we have that
x ∣ algebra_map (𝓞 K) (𝓞 L) (norm K x).