English
Let L/K be a finite separable field extension and b = (b_i) a finite set in L. For an algebraically closed field E with embeddings σ_j : L → E corresponding to j ∈ ι via a bijection e : ι ≃ (L →ₐ[K] E), the discriminant of b over K equals the square of the determinant of the embeddings matrix: algebraMap_K_E(discr_K(b)) = det(embeddingsMatrixReindex_K_E(b,e))^2.
Русский
Пусть L/K — конечное разделимое расширение полей, и пусть b = (b_i) — конечный набор элементов L. Для алгебраически замкнутого поля E с вложениями σ_j: L → E, соответствующими j ∈ ι посредством биекции e: ι ≃ (L →ₐ[K] E), дискриминант b над K равен квадрату детерминанта матрицы вложений: algebraMap_K_E(discr_K(b)) = det(embeddingsMatrixReindex_K_E(b,e))^2.
LaTeX
$$$$ \\ algebraMap_K_E(\\mathrm{discr}\\,K\\,b) = \\big( \\det(\\mathrm{embeddingsMatrixReindex}\\,K\\,E\\,b\\,e) \\big)^2 $$$$
Lean4
/-- If `L/K` is a field extension and `b : ι → L`, then `discr K b` is the square of the
determinant of the matrix whose `(i, j)` coefficient is `σⱼ (b i)`, where `σⱼ : L →ₐ[K] E` is the
embedding in an algebraically closed field `E` corresponding to `j : ι` via a bijection
`e : ι ≃ (L →ₐ[K] E)`. -/
theorem discr_eq_det_embeddingsMatrixReindex_pow_two [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)) :
algebraMap K E (discr K b) = (embeddingsMatrixReindex K E b e).det ^ 2 := by
rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply, traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul,
det_transpose, pow_two]
