# mathlibdocumentation

ring_theory.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_linear_independent : if b is not linear independent, then algebra.discr A b = 0.
• algebra.discr_of_matrix_vec_mul and discr_of_matrix_mul_vec : formulas relating algebra.discr A ι b with algebra.discr A ((P.map (algebra_map A B)).vec_mul b) and algebra.discr A ((P.map (algebra_map A B)).mul_vec 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_embeddings_matrix_reindex_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_of_power_basis_eq_prod : the discriminant of a power basis.
• discr_is_integral : if K and L are fields and is_scalar_tower R K L, is b : ι → L satisfies ∀ i, is_integral R (b i), then is_integral R (discr K b).
• discr_mul_is_integral_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 : power_basis K L be such that is_integral 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} [comm_ring A] [comm_ring B] [ 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 trace_matrix A ι b.

Equations
theorem algebra.discr_def (A : Type u) {B : Type v} {ι : Type w} [comm_ring A] [comm_ring B] [ B] [decidable_eq ι] [fintype ι] (b : ι → B) :
= b).det
@[simp]
theorem algebra.discr_reindex (A : Type u) {B : Type v} {ι : Type w} [comm_ring A] [comm_ring B] [ B] {ι' : Type u_1} [fintype ι'] [fintype ι] (b : A B) (f : ι ι') :
(b (f.symm)) =
theorem algebra.discr_zero_of_not_linear_independent (A : Type u) {B : Type v} {ι : Type w} [comm_ring A] [comm_ring B] [ B] [fintype ι] [is_domain A] {b : ι → B} (hli : ¬) :
= 0

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

theorem algebra.discr_of_matrix_vec_mul {A : Type u} {B : Type v} {ι : Type w} [comm_ring A] [comm_ring B] [ B] [fintype ι] [decidable_eq ι] (b : ι → B) (P : ι A) :
(P.map B))) = P.det ^ 2 *

Relation between algebra.discr A ι b and algebra.discr A ((P.map (algebra_map A B)).vec_mul b).

theorem algebra.discr_of_matrix_mul_vec {A : Type u} {B : Type v} {ι : Type w} [comm_ring A] [comm_ring B] [ B] [fintype ι] [decidable_eq ι] (b : ι → B) (P : ι A) :
((P.map B)).mul_vec b) = P.det ^ 2 *

Relation between algebra.discr A ι b and algebra.discr A ((P.map (algebra_map A B)).mul_vec b).

theorem algebra.discr_not_zero_of_basis {ι : Type w} [fintype ι] (K : Type u) {L : Type v} [field K] [field L] [ L] [ L] [ L] (b : K L) :
0

Over a field, if b is a basis, then algebra.discr K b ≠ 0.

theorem algebra.discr_is_unit_of_basis {ι : Type w} [fintype ι] (K : Type u) {L : Type v} [field K] [field L] [ L] [ L] [ L] (b : K L) :

Over a field, if b is a basis, then algebra.discr K b is a unit.

theorem algebra.discr_eq_det_embeddings_matrix_reindex_pow_two {ι : Type w} [fintype ι] (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E] [ L] [ E] [ L] (b : ι → L) [decidable_eq ι] [ L] (e : ι (L →ₐ[K] E)) :
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_power_basis_eq_prod (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E] [ L] [ E] [ L] (pb : L) (e : fin pb.dim (L →ₐ[K] E)) [ L] :
E) (pb.basis)) = finset.univ.prod (λ (i : fin pb.dim), (finset.Ioi i).prod (λ (j : fin pb.dim), ((e j) pb.gen - (e i) pb.gen) ^ 2))

The discriminant of a power basis.

theorem algebra.discr_power_basis_eq_prod' (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E] [ L] [ E] [ L] (pb : L) [ L] (e : fin pb.dim (L →ₐ[K] E)) :
E) (pb.basis)) = finset.univ.prod (λ (i : fin pb.dim), (finset.Ioi i).prod (λ (j : fin pb.dim), -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))))

A variation of of_power_basis_eq_prod.

theorem algebra.discr_power_basis_eq_prod'' (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E] [ L] [ E] [ L] (pb : L) [ L] (e : fin pb.dim (L →ₐ[K] E)) :
E) (pb.basis)) = (-1) ^ * - 1) / 2) * finset.univ.prod (λ (i : fin pb.dim), (finset.Ioi i).prod (λ (j : fin pb.dim), ((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen)))

A variation of of_power_basis_eq_prod.

theorem algebra.discr_power_basis_eq_norm (K : Type u) {L : Type v} [field K] [field L] [ L] [ L] (pb : L) [ L] :

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

theorem algebra.discr_is_integral {ι : Type w} [fintype ι] (K : Type u) {L : Type v} [field K] [field L] [ L] [ L] {R : Type z} [comm_ring R] [ K] [ L] [ L] {b : ι → L} (h : ∀ (i : ι), (b i)) :
b)

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

theorem algebra.discr_eq_discr_of_to_matrix_coeff_is_integral {ι : Type w} {ι' : Type u_1} [fintype ι'] [fintype ι] (K : Type u) [field K] [number_field K] {b : K} {b' : basis ι' K} (h : ∀ (i : ι) (j : ι'), (b.to_matrix b' i j)) (h' : ∀ (i : ι') (j : ι), (b'.to_matrix b i j)) :

If b and b' are ℚ-bases of a number field K such that ∀ i j, is_integral ℤ (b.to_matrix b' i j) and ∀ i j, is_integral ℤ (b'.to_matrix b i j) then discr ℚ b = discr ℚ b'.

theorem algebra.discr_mul_is_integral_mem_adjoin (K : Type u) {L : Type v} [field K] [field L] [ L] [ L] {R : Type z} [comm_ring R] [ K] [ L] [ L] [is_domain R] [ L] [ K] {B : L} (hint : B.gen) {z : L} (hz : z) :
(B.basis) z {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 : power_basis K L be such that is_integral 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).