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.