mathlib documentation

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 #

Main results #

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] [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 trace_matrix A ι b.

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

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] [algebra A B] [fintype ι] [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :

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] [algebra A B] [fintype ι] [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :

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] [algebra K L] [module.finite K L] [is_separable K L] (b : basis ι K L) :

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] [algebra K L] [module.finite K L] [is_separable 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_embeddings_matrix_reindex_pow_two {ι : Type w} [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] [is_alg_closed E] (b : ι → L) [decidable_eq ι] [is_separable K L] (e : ι (L →ₐ[K] E)) :

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] [algebra K L] [algebra K E] [module.finite K L] [is_alg_closed E] (pb : power_basis K L) (e : fin pb.dim (L →ₐ[K] E)) [is_separable K L] :
(algebra_map K E) (algebra.discr K (pb.basis)) = finset.univ.prod (λ (i : fin pb.dim), (finset.filter (λ (j : fin pb.dim), i < j) finset.univ).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] [algebra K L] [algebra K E] [module.finite K L] [is_alg_closed E] (pb : power_basis K L) [is_separable K L] (e : fin pb.dim (L →ₐ[K] E)) :
(algebra_map K E) (algebra.discr K (pb.basis)) = finset.univ.prod (λ (i : fin pb.dim), (finset.filter (λ (j : fin pb.dim), i < j) finset.univ).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] [algebra K L] [algebra K E] [module.finite K L] [is_alg_closed E] (pb : power_basis K L) [is_separable K L] (e : fin pb.dim (L →ₐ[K] E)) :
(algebra_map K E) (algebra.discr K (pb.basis)) = (-1) ^ (finite_dimensional.finrank K L * (finite_dimensional.finrank K L - 1) / 2) * finset.univ.prod (λ (i : fin pb.dim), (finset.filter (λ (j : fin pb.dim), i < j) finset.univ).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.

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] [algebra K L] [module.finite K L] {R : Type z} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L] {b : ι → L} (h : ∀ (i : ι), is_integral R (b i)) :

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 : basis ι K} {b' : basis ι' K} (h : ∀ (i : ι) (j : ι'), is_integral (b.to_matrix b' i j)) (h' : ∀ (i : ι') (j : ι), is_integral (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] [algebra K L] [module.finite K L] {R : Type z} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L] [is_domain R] [is_separable K L] [is_integrally_closed R] [is_fraction_ring R K] {B : power_basis K L} (hint : is_integral R B.gen) {z : L} (hz : is_integral R z) :

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).