# 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} [] (A : Type u) {B : Type v} [] [] [Algebra A B] [] (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
• = ().det
Instances For
theorem Algebra.discr_def (A : Type u) {B : Type v} {ι : Type w} [] [] [] [Algebra A B] [] (b : ιB) :
= ().det
theorem Algebra.discr_eq_discr_of_algEquiv {A : Type u} {B : Type v} {C : Type z} {ι : Type w} [] [] [] [Algebra A B] [] [Algebra A C] [] (b : ιB) (f : B ≃ₐ[A] C) :
= 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} [] [] [] [Algebra A B] {ι' : Type u_1} [Fintype ι'] [] [] (b : Basis ι A B) (f : ι ι') :
Algebra.discr A (b f.symm) =
theorem Algebra.discr_zero_of_not_linearIndependent (A : Type u) {B : Type v} {ι : Type w} [] [] [] [Algebra A B] [] [] {b : ιB} (hli : ) :
= 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} [] [] [] [Algebra A B] [] (b : ιB) (P : Matrix ι ι A) :
Algebra.discr A (Matrix.vecMul b (P.map ())) = P.det ^ 2 *

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} [] [] [] [Algebra A B] [] (b : ιB) (P : Matrix ι ι A) :
Algebra.discr A ((P.map ()).mulVec b) = P.det ^ 2 *

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} [] [] (K : Type u) {L : Type v} [] [] [Algebra K L] [] [] (b : Basis ι K L) :
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} [] [] (K : Type u) {L : Type v} [] [] [Algebra K L] [] [] (b : Basis ι K L) :

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} [] [] (K : Type u) {L : Type v} (E : Type z) [] [] [] [Algebra K L] [Algebra K E] [] [] (b : ιL) [] (e : ι (L →ₐ[K] 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) [] [] [] [Algebra K L] [Algebra K E] [] [] (pb : ) (e : Fin pb.dim (L →ₐ[K] E)) [] :
() (Algebra.discr K pb.basis) = i : Fin pb.dim, j, ((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) [] [] [] [Algebra K L] [Algebra K E] [] [] (pb : ) [] (e : Fin pb.dim (L →ₐ[K] E)) :
() (Algebra.discr K pb.basis) = i : Fin pb.dim, j, -(((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) [] [] [] [Algebra K L] [Algebra K E] [] [] (pb : ) [] (e : Fin pb.dim (L →ₐ[K] E)) :
() (Algebra.discr K pb.basis) = (-1) ^ ( * () / 2) * i : Fin pb.dim, j, ((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} [] [] [Algebra K L] [] (pb : ) [] :
Algebra.discr K pb.basis = (-1) ^ ( * () / 2) * () ((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} [] [] (K : Type u) {L : Type v} [] [] [Algebra K L] [] {R : Type z} [] [Algebra R K] [Algebra R L] [] {b : ιL} (h : ∀ (i : ι), IsIntegral R (b i)) :

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} [] [] [Algebra K L] [] {R : Type z} [] [Algebra R K] [Algebra R L] [] [] [] {B : } (hint : IsIntegral R B.gen) {z : L} (hz : ) :
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} [] [] [] (b : Basis ι A) (b' : Basis ι A) :
=

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