# Documentation

Mathlib.RingTheory.Discriminant

# 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 ((P.map (algebraMap A B)).vecMul b) and Algebra.discr A ((P.map (algebraMap A B)).mulVec 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.

Instances For
theorem Algebra.discr_def (A : Type u) {B : Type v} {ι : Type w} [] [] [] [Algebra A B] [] (b : ιB) :
=
@[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) :

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

theorem Algebra.discr_of_matrix_mulVec {A : Type u} {B : Type v} {ι : Type w} [] [] [] [Algebra A B] [] (b : ιB) (P : Matrix ι ι A) :

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

theorem Algebra.discr_not_zero_of_basis {ι : Type w} [] [] (K : Type u) {L : Type v} [] [] [Algebra K L] [] [] (b : Basis ι K L) :
0

Over a field, if b is a basis, 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) :

Over a field, if b is a basis, 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)) :
↑() () = ^ 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) = Finset.prod Finset.univ fun i => Finset.prod () fun 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) = Finset.prod Finset.univ fun i => Finset.prod () fun 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) * Finset.prod Finset.univ fun i => Finset.prod () fun 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_eq_discr_of_toMatrix_coeff_isIntegral {ι : Type w} [] {ι' : Type u_1} [Fintype ι'] [] [] (K : Type u) [] [] {b : Basis ι K} {b' : Basis ι' K} (h : ∀ (i : ι) (j : ι'), IsIntegral (Basis.toMatrix b (b') i j)) (h' : ∀ (i : ι') (j : ι), IsIntegral (Basis.toMatrix b' (b) i j)) :
=

If b and b' are ℚ-bases of a number field K such that ∀ i j, IsIntegral ℤ (b.toMatrix b' i j) and ∀ i j, IsIntegral ℤ (b'.toMatrix b i j) then discr ℚ b = discr ℚ 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.