English
For finite separable L/K and x ∈ L, the K-norm of x equals the product, over all K-embeddings σ: L→E, of σ(x) in an algebraic closure E of K.
Русский
Для конечного разделимого расширения L/K и элемента x∈L норма по K равна произведению всех изображений x под K-отображениями в неразложенном замыкании E.
LaTeX
$$$\\mathrm{algebraMap}_K^E(\\mathrm{norm}_K x) = \\prod_{\\sigma: L \\hookrightarrow_K E} \\sigma(x).$$$
Lean4
/-- For `L/K` a finite separable extension of fields and `E` an algebraically closed extension
of `K`, the norm (down to `K`) of an element `x` of `L` is equal to the product of the images
of `x` over all the `K`-embeddings `σ` of `L` into `E`. -/
theorem norm_eq_prod_embeddings [Algebra.IsSeparable K L] [IsAlgClosed E] (x : L) :
algebraMap K E (norm K x) = ∏ σ : L →ₐ[K] E, σ x :=
by
have hx := Algebra.IsSeparable.isIntegral K x
rw [norm_eq_norm_adjoin K x, RingHom.map_pow, ← adjoin.powerBasis_gen hx,
norm_eq_prod_embeddings_gen E (adjoin.powerBasis hx) (IsAlgClosed.splits_codomain _)]
· exact (prod_embeddings_eq_finrank_pow L (L := K⟮x⟯) E (adjoin.powerBasis hx)).symm
· haveI := Algebra.isSeparable_tower_bot_of_isSeparable K K⟮x⟯ L
exact Algebra.IsSeparable.isSeparable K _
