English
Let K be a field of characteristic zero and F a finite-dimensional K-algebra. For every x in the ring of integers of F, the norm from F to K is a unit in the ring of integers of K if and only if x is a unit in the ring of integers of F.
Русский
Пусть K — поле характеристика ноль, F — конечномерное расширение над K. Пусть x принадлежит кольцу целых чисел F. Тогда нормa_{F/K}(x) является единицей в кольце целых чисел K тогда и только тогда, когда x является единицей в кольце целых чисел F.
LaTeX
$$$\text{IsUnit}\big(\mathrm{N}_{F/K}(x)\big) \iff \text{IsUnit}(x), \quad x \in \mathcal{O}_F,$$$
Lean4
theorem isUnit_norm [CharZero K] {x : 𝓞 F} : IsUnit (norm K x) ↔ IsUnit x :=
by
letI : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
let L := normalClosure K F (AlgebraicClosure F)
haveI : FiniteDimensional F L := FiniteDimensional.right K F L
haveI : IsAlgClosure K (AlgebraicClosure F) := IsAlgClosure.ofAlgebraic K F (AlgebraicClosure F)
haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L
calc
IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) := (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
_ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
_ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := (isUnit_norm_of_isGalois K)
_ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
_ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
_ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)
