mathlib3 documentation

ring_theory.discriminant

Discriminant of a family of vectors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [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

algebra.discr A b = (algebra.trace_matrix A b).det

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

algebra.discr A b = (algebra.trace_matrix A b).det

@[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 : ι ≃ ι') :

algebra.discr A (⇑b ∘ ⇑(f.symm)) = algebra.discr A ⇑b

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

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

algebra.discr A (matrix.vec_mul b (P.map ⇑(algebra_map A B))) = P.det ^ 2 * algebra.discr A b

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

algebra.discr A ((P.map ⇑(algebra_map A B)).mul_vec b) = P.det ^ 2 * algebra.discr A b

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

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

is_unit (algebra.discr K ⇑b)

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

⇑(algebra_map K E) (algebra.discr K b) = (algebra.embeddings_matrix_reindex K 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] [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.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] [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.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] [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.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] [algebra K L] [module.finite K L] (pb : power_basis K L) [is_separable K L] :

algebra.discr K ⇑(pb.basis) = (-1) ^ (finite_dimensional.finrank K L * (finite_dimensional.finrank K L - 1) / 2) * ⇑(algebra.norm K) (⇑(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_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)) :

is_integral R (algebra.discr K 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 : 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)) :

algebra.discr ℚ ⇑b = algebra.discr ℚ ⇑b'

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

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