Norm in number fields #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. 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.coe_norm_algebra_map
{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 K)) :
β(β(ring_of_integers.norm K) (β(algebra_map β₯(number_field.ring_of_integers K) β₯(number_field.ring_of_integers L)) x)) = β(algebra.norm K) (β(algebra_map K L) βx)
theorem
ring_of_integers.norm_algebra_map
{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 K)) :
theorem
ring_of_integers.is_unit_norm_of_is_galois
{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)) :
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).
theorem
ring_of_integers.norm_norm
{L : Type u_1}
(K : Type u_2)
[field K]
[field L]
[algebra K L]
[finite_dimensional K L]
(F : Type u_3)
[field F]
[algebra K F]
[is_separable K F]
[finite_dimensional K F]
[is_separable K L]
[algebra F L]
[is_separable F L]
[finite_dimensional F L]
[is_scalar_tower K F L]
(x : β₯(number_field.ring_of_integers L)) :
β(ring_of_integers.norm K) (β(ring_of_integers.norm F) x) = β(ring_of_integers.norm K) x
theorem
ring_of_integers.is_unit_norm
(K : Type u_2)
[field K]
{F : Type u_3}
[field F]
[algebra K F]
[is_separable K F]
[finite_dimensional K F]
[char_zero K]
{x : β₯(number_field.ring_of_integers F)} :
is_unit (β(ring_of_integers.norm K) x) β is_unit x