Theorems · Theorem · commutative algebra

Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two

∀ {ι : Type w} [inst : DecidableEq ι] [inst_1 : Fintype ι] (K : Type u) {L : Type v} (E : Type z) [inst_2 : Field K]
  [inst_3 : Field L] [inst_4 : Field E] [inst_5 : Algebra K L] [inst_6 : Algebra K E] [Module.Finite K L]
  [IsAlgClosed E] (b : ι → L) [Algebra.IsSeparable K L] (e : ι ≃ (L →ₐ[K] E)),
  (algebraMap K E) (Algebra.discr K b) = (Algebra.embeddingsMatrixReindex K E b e).det ^ 2

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).

Defined in

Mathlib.RingTheory.Discriminant

Cited by

4 results in Mathlib

Foundations

Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeFieldFieldFieldAlgebraAlgebraModule.FiniteIsAlgClosedAlgebra.IsSeparable