English
If x ∈ L is integral over R, then its norm to K is integral over R, assuming towers with IsScalarTower and freeness conditions.
Русский
Если x ∈ L интеграл над R, то его норма по направлению K является интегралом над R, при условии существования заданной структуры тензорной башни и свободности модулей.
LaTeX
$$$\\text{IsIntegral}_R(x) \\implies \\text{IsIntegral}_R(\\mathrm{norm}_K(x)).$$$
Lean4
theorem isIntegral_norm [Algebra R L] [Algebra R K] [IsScalarTower R K L] {x : L} (hx : IsIntegral R x) :
IsIntegral R (norm K x) := by
by_cases h : FiniteDimensional K L
swap
· simpa [norm_eq_one_of_not_module_finite h] using isIntegral_one
let F := K⟮x⟯
rw [← norm_norm (S := F), ← coe_gen K x, ← IntermediateField.algebraMap_apply,
norm_algebraMap_of_basis (Module.Free.chooseBasis F L) (gen K x), map_pow]
apply IsIntegral.pow
rw [← isIntegral_algebraMap_iff (algebraMap K (AlgebraicClosure F)).injective,
norm_gen_eq_prod_roots _ (IsAlgClosed.splits_codomain _)]
refine IsIntegral.multiset_prod (fun y hy ↦ ⟨minpoly R x, minpoly.monic hx, ?_⟩)
suffices (aeval y) ((minpoly R x).map (algebraMap R K)) = 0 by simpa
obtain ⟨P, hP⟩ := minpoly.dvd K x (show aeval x ((minpoly R x).map (algebraMap R K)) = 0 by simp)
simp [hP, aeval_mul, (mem_aroots'.mp hy).2]
