Discriminant of a family of vectors

Given an A-algebra B and b, an ι-indexed family of elements of B, we define the discriminant of b as the determinant of the matrix whose (i j)-th element is the trace of b i * b j.

Main definition

• Algebra.discr A b : the discriminant of b : ι → B.

Main results

• Algebra.discr_zero_of_not_linearIndependent : if b is not linear independent, then Algebra.discr A b = 0.
• Algebra.discr_of_matrix_vecMul and Algebra.discr_of_matrix_mulVec : formulas relating Algebra.discr A ι b with Algebra.discr A (b ᵥ* P.map (algebraMap A B)) and Algebra.discr A (P.map (algebraMap A B) *ᵥ b).
• Algebra.discr_not_zero_of_basis : over a field, if b is a basis, then Algebra.discr K b ≠ 0.
• Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two : 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).
• Algebra.discr_powerBasis_eq_prod : the discriminant of a power basis.
• Algebra.discr_isIntegral : if K and L are fields and IsScalarTower R K L, if b : ι → L satisfies ∀ i, IsIntegral R (b i), then IsIntegral R (discr K b).
• Algebra.discr_mul_isIntegral_mem_adjoin : let K be the fraction field of an integrally closed domain R and let L be a finite separable extension of K. Let B : PowerBasis K L be such that IsIntegral R B.gen. Then for all, z : L we have (discr K B.basis) • z ∈ adjoin R ({B.gen} : Set L).

Implementation details

Our definition works for any A-algebra B, but note that if B is not free as an A-module, then trace A B = 0 by definition, so discr A b = 0 for any b.

noncomputable def Algebra.discr {ι : Type w} [DecidableEq ι] (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) : A

Given an A-algebra B and b, an ι-indexed family of elements of B, we define discr A ι b as the determinant of traceMatrix A ι b.

Equations

• Algebra.discr A b = (Algebra.traceMatrix A b).det

theorem Algebra.discr_def (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) : Algebra.discr A b = (Algebra.traceMatrix A b).det

theorem Algebra.discr_eq_discr_of_algEquiv {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [CommRing C] [Algebra A C] [Fintype ι] (b : ι → B) (f : B ≃ₐ[A] C) : Algebra.discr A b = Algebra.discr A (⇑f ∘ b)

Mapping a family of vectors along an AlgEquiv preserves the discriminant.

@[simp]

theorem Algebra.discr_reindex (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] {ι' : Type u_1} [Fintype ι'] [Fintype ι] [DecidableEq ι'] (b : Basis ι A B) (f : ι ≃ ι') : Algebra.discr A (⇑b ∘ ⇑f.symm) = Algebra.discr A ⇑b

theorem Algebra.discr_zero_of_not_linearIndependent (A : Type u) {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] [IsDomain A] {b : ι → B} (hli : ¬LinearIndependent A b) : Algebra.discr A b = 0

If b is not linear independent, then Algebra.discr A b = 0.

theorem Algebra.discr_of_matrix_vecMul {A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) (P : Matrix ι ι A) : Algebra.discr A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.det ^ 2 * Algebra.discr A b

Relation between Algebra.discr A ι b and Algebra.discr A (b ᵥ* P.map (algebraMap A B)).

theorem Algebra.discr_of_matrix_mulVec {A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) (P : Matrix ι ι A) : Algebra.discr A ((P.map ⇑(algebraMap A B)).mulVec b) = P.det ^ 2 * Algebra.discr A b

Relation between Algebra.discr A ι b and Algebra.discr A ((P.map (algebraMap A B)) *ᵥ b).

theorem Algebra.discr_not_zero_of_basis {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsSeparable K L] (b : Basis ι K L) : Algebra.discr K ⇑b ≠ 0

If b is a basis of a finite separable field extension L/K, then Algebra.discr K b ≠ 0.

theorem Algebra.discr_isUnit_of_basis {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] [IsSeparable K L] (b : Basis ι K L) : IsUnit (Algebra.discr K ⇑b)

If b is a basis of a finite separable field extension L/K, then Algebra.discr K b is a unit.

theorem Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (b : ι → L) [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).

theorem Algebra.discr_powerBasis_eq_prod (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) (e : Fin pb.dim ≃ (L →ₐ[K] E)) [IsSeparable K L] : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = Finset.univ.prod fun (i : Fin pb.dim) => (Finset.Ioi i).prod fun (j : Fin pb.dim) => ((e j) pb.gen - (e i) pb.gen) ^ 2

The discriminant of a power basis.

theorem Algebra.discr_powerBasis_eq_prod' (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = Finset.univ.prod fun (i : Fin pb.dim) => (Finset.Ioi i).prod fun (j : Fin pb.dim) => -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

A variation of Algebra.discr_powerBasis_eq_prod.

theorem Algebra.discr_powerBasis_eq_prod'' (K : Type u) {L : Type v} (E : Type z) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Module.Finite K L] [IsAlgClosed E] (pb : PowerBasis K L) [IsSeparable K L] (e : Fin pb.dim ≃ (L →ₐ[K] E)) : (algebraMap K E) (Algebra.discr K ⇑pb.basis) = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * Finset.univ.prod fun (i : Fin pb.dim) => (Finset.Ioi i).prod fun (j : Fin pb.dim) => ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)

A variation of Algebra.discr_powerBasis_eq_prod.

theorem Algebra.discr_powerBasis_eq_norm (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] (pb : PowerBasis K L) [IsSeparable K L] : Algebra.discr K ⇑pb.basis = (-1) ^ (FiniteDimensional.finrank K L * (FiniteDimensional.finrank K L - 1) / 2) * (Algebra.norm K) ((Polynomial.aeval pb.gen) (Polynomial.derivative (minpoly K pb.gen)))

Formula for the discriminant of a power basis using the norm of the field extension.

theorem Algebra.discr_isIntegral {ι : Type w} [DecidableEq ι] [Fintype ι] (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] {R : Type z} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] {b : ι → L} (h : ∀ (i : ι), IsIntegral R (b i)) : IsIntegral R (Algebra.discr K b)

If K and L are fields and IsScalarTower R K L, and b : ι → L satisfies ∀ i, IsIntegral R (b i), then IsIntegral R (discr K b).

theorem Algebra.discr_mul_isIntegral_mem_adjoin (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [Module.Finite K L] {R : Type z} [CommRing R] [Algebra R K] [Algebra R L] [IsScalarTower R K L] [IsSeparable K L] [IsIntegrallyClosed R] [IsFractionRing R K] {B : PowerBasis K L} (hint : IsIntegral R B.gen) {z : L} (hz : IsIntegral R z) : Algebra.discr K ⇑B.basis • z ∈ Algebra.adjoin R {B.gen}

Let K be the fraction field of an integrally closed domain R and let L be a finite separable extension of K. Let B : PowerBasis K L be such that IsIntegral R B.gen. Then for all, z : L that are integral over R, we have (discr K B.basis) • z ∈ adjoin R ({B.gen} : Set L).

theorem Algebra.discr_eq_discr (A : Type u) {ι : Type w} [DecidableEq ι] [CommRing A] [Fintype ι] (b : Basis ι ℤ A) (b' : Basis ι ℤ A) : Algebra.discr ℤ ⇑b = Algebra.discr ℤ ⇑b'

Two (finite) ℤ-bases have the same discriminant.