[Merged by Bors] - feat(ring_theory/discriminant): add the discriminant of a family of vectors

src/data/matrix/basic.lean

@@ -1443,6 +1443,12 @@ lemma conj_transpose_reindex [has_star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M
   (reindex eₘ eₙ M)ᴴ = (reindex eₙ eₘ Mᴴ) :=
 rfl
 
+@[simp]
+lemma minor_mul_transpose_minor [fintype n] [fintype m] [semiring α]
+  (e : n ≃ m) (M : matrix n m α) :
+  (M.minor id e) ⬝ (Mᵀ).minor e id = M ⬝ Mᵀ :=
+by rw [minor_mul_equiv, minor_id_id]
+
 /-- The left `n × l` part of a `n × (l+r)` matrix. -/
 @[reducible]
 def sub_left {m l r : nat} (A : matrix (fin m) (fin (l + r)) α) : matrix (fin m) (fin l) α :=

src/linear_algebra/alternating.lean

@@ -466,7 +466,7 @@ lemma map_linear_dependent
   (h : ¬linear_independent K v) :
   f v = 0 :=
 begin
-  obtain ⟨s, g, h, i, hi, hz⟩ := linear_dependent_iff.mp h,
+  obtain ⟨s, g, h, i, hi, hz⟩ := not_linear_independent_iff.mp h,
   suffices : f (update v i (g i • v i)) = 0,
   { rw [f.map_smul, function.update_eq_self, smul_eq_zero] at this,
     exact or.resolve_left this hz, },

src/linear_algebra/finite_dimensional.lean

@@ -465,7 +465,7 @@ lemma exists_nontrivial_relation_of_dim_lt_card
   ∃ f : V → K, ∑ e in t, f e • e = 0 ∧ ∃ x ∈ t, f x ≠ 0 :=
 begin
   have := mt finset_card_le_finrank_of_linear_independent (by { simpa using h }),
-  rw linear_dependent_iff at this,
+  rw not_linear_independent_iff at this,
   obtain ⟨s, g, sum, z, zm, nonzero⟩ := this,
   -- Now we have to extend `g` to all of `t`, then to all of `V`.
   let f : V → K :=

src/linear_algebra/linear_independent.lean

@@ -122,7 +122,7 @@ linear_independent_iff'.trans ⟨λ H s g hg hv i, if his : i ∈ s then H s g h
     (by simp_rw [ite_smul, zero_smul, finset.sum_extend_by_zero, hg]) i,
   exact (if_pos hi).symm }⟩
 
-theorem linear_dependent_iff : ¬ linear_independent R v ↔
+theorem not_linear_independent_iff : ¬ linear_independent R v ↔
   ∃ s : finset ι, ∃ g : ι → R, (∑ i in s, g i • v i) = 0 ∧ (∃ i ∈ s, g i ≠ 0) :=
 begin
   rw linear_independent_iff',
@@ -146,6 +146,10 @@ theorem fintype.linear_independent_iff' [fintype ι] :
     (linear_map.lsum R (λ i : ι, R) ℕ (λ i, linear_map.id.smul_right (v i))).ker = ⊥ :=
 by simp [fintype.linear_independent_iff, linear_map.ker_eq_bot', funext_iff]
 
+lemma fintype.not_linear_independent_iff [fintype ι] :
+  ¬linear_independent R v ↔ ∃ g : ι → R, (∑ i, g i • v i) = 0 ∧ (∃ i, g i ≠ 0) :=
+by simpa using (not_iff_not.2 fintype.linear_independent_iff)
+
 lemma linear_independent_empty_type [is_empty ι] : linear_independent R v :=
 linear_independent_iff.mpr $ λ v hv, subsingleton.elim v 0
 

src/ring_theory/discriminant.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2021 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import ring_theory.trace
+
+/-!
+# 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_linear_independent` : over a field, if `b` is linear independent, 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.
+
+## 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`.
+-/
+
+universes u v w z
+
+open_locale matrix big_operators
+
+open matrix finite_dimensional fintype polynomial finset
+
+namespace algebra
+
+variables (A : Type u) {B : Type v} (C : Type z) {ι : Type w}
+variables [comm_ring A] [comm_ring B] [algebra A B] [comm_ring C] [algebra A C]
+
+section discr
+
+/-- 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`. -/
+noncomputable
+def discr (A : Type u) {B : Type v} [comm_ring A] [comm_ring B] [algebra A B] [fintype ι]
+  (b : ι → B) := by { classical, exact (trace_matrix A b).det }
+
+lemma discr_def [decidable_eq ι] [fintype ι] (b : ι → B) :
+  discr A b = (trace_matrix A b).det := by convert rfl
+
+variable [fintype ι]
+
+section basic
+
+lemma discr_zero_of_not_linear_independent [is_domain A] {b : ι → B}
+  (hli : ¬linear_independent A b) : discr A b = 0 :=
+begin
+  classical,
+  obtain ⟨g, hg, i, hi⟩ := fintype.not_linear_independent_iff.1 hli,
+  have : (trace_matrix A b).mul_vec g = 0,
+  { ext i,
+    have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (((g j) • (b j)) * b i),
+    { intro j, simp [mul_comm], },
+    simp only [mul_vec, dot_product, trace_matrix, pi.zero_apply, trace_form_apply,
+      λ j, this j, ← linear_map.map_sum, ← sum_mul, hg, zero_mul, linear_map.map_zero] },
+  by_contra h,
+  rw discr_def at h,
+  simpa [matrix.eq_zero_of_mul_vec_eq_zero h this] using hi,
+end
+
+variable {A}
+
+lemma discr_of_matrix_vec_mul [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :
+  discr A ((P.map (algebra_map A B)).vec_mul b) = P.det ^ 2 * discr A b :=
+by rw [discr_def, trace_matrix_of_matrix_vec_mul, det_mul, det_mul, det_transpose, mul_comm,
+    ← mul_assoc, discr_def, pow_two]
+
+
+lemma discr_of_matrix_mul_vec [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :
+  discr A ((P.map (algebra_map A B)).mul_vec b) = P.det ^ 2 * discr A b :=
+by rw [discr_def, trace_matrix_of_matrix_mul_vec, det_mul, det_mul, det_transpose,
+  mul_comm, ← mul_assoc, discr_def, pow_two]
+
+end basic
+
+section field
+
+variables (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E]
+variables [algebra K L] [algebra K E]
+variables [module.finite K L] [is_separable K L] [is_alg_closed E]
+variables (b : ι → L) (pb : power_basis K L)
+
+lemma discr_not_zero_of_linear_independent [nonempty ι]
+  (hcard : fintype.card ι = finrank K L) (hli : linear_independent K b) : discr K b ≠ 0 :=
+begin
+  classical,
+  have := span_eq_top_of_linear_independent_of_card_eq_finrank hli hcard,
+  rw [discr_def, trace_matrix_def],
+  simp_rw [← basis.mk_apply hli this],
+  rw [← trace_matrix_def, trace_matrix_of_basis, ← bilin_form.nondegenerate_iff_det_ne_zero],
+  exact trace_form_nondegenerate _ _
+end
+
+lemma discr_eq_det_embeddings_matrix_reindex_pow_two [decidable_eq ι]
+  (e : ι ≃ (L →ₐ[K] E)) : algebra_map K E (discr K b) =
+  (embeddings_matrix_reindex K E b e).det ^ 2 :=
+by rw [discr_def, ring_hom.map_det, ring_hom.map_matrix_apply,
+    trace_matrix_eq_embeddings_matrix_reindex_mul_trans, det_mul, det_transpose, pow_two]
+
+lemma discr_power_basis_eq_prod (e : fin pb.dim ≃ (L →ₐ[K] E)) :
+  algebra_map K E (discr K pb.basis) =
+  ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j), (e j pb.gen- (e i pb.gen)) ^ 2 :=
+begin
+  rw [discr_eq_det_embeddings_matrix_reindex_pow_two K E pb.basis e,
+    embeddings_matrix_reindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow],
+  congr, ext i,
+  rw [← prod_pow]
+end
+
+end field
+
+end discr
+
+end algebra

src/ring_theory/trace.lean

@@ -20,6 +20,27 @@ Suppose we have an `R`-algebra `S` with a finite basis. For each `s : S`,
 the trace of the linear map given by multiplying by `s` gives information about
 the roots of the minimal polynomial of `s` over `R`.
 
+## Main definitions
+
+ * `algebra.trace R S x`: the trace of an element `s` of an `R`-algebra `S`
+ * `algebra.trace_form R S`: bilinear form sending `x`, `y` to the trace of `x * y`
+ * `algebra.trace_matrix R b`: the matrix whose `(i j)`-th element is the trace of `b i * b j`.
+ * `algebra.embeddings_matrix A C b : matrix κ (B →ₐ[A] C) C` is the matrix whose
+   `(i, σ)` coefficient is `σ (b i)`.
+ * `algebra.embeddings_matrix_reindex A C b e : matrix κ κ C` is the matrix whose `(i, j)`
+   coefficient is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ`
+   given by a bijection `e : κ ≃ (B →ₐ[A] C)`.
+
+## Main results
+
+ * `trace_algebra_map_of_basis`, `trace_algebra_map`: if `x : K`, then `Tr_{L/K} x = [L : K] x`
+ * `trace_trace_of_basis`, `trace_trace`: `Tr_{L/K} (Tr_{F/L} x) = Tr_{F/K} x`
+ * `trace_eq_sum_roots`: the trace of `x : K(x)` is the sum of all conjugate roots of `x`
+ * `trace_eq_sum_embeddings`: the trace of `x : K(x)` is the sum of all embeddings of `x` into an
+   algebraically closed field
+ * `trace_form_nondegenerate`: the trace form over a separable extension is a nondegenerate
+   bilinear form
+
 ## Implementation notes
 
 Typically, the trace is defined specifically for finite field extensions.
@@ -36,12 +57,12 @@ For now, the definitions assume `S` is commutative, so the choice doesn't matter
 
 -/
 
-universes u v w
+universes u v w z
 
 variables {R S T : Type*} [comm_ring R] [comm_ring S] [comm_ring T]
 variables [algebra R S] [algebra R T]
 variables {K L : Type*} [field K] [field L] [algebra K L]
-variables {ι : Type w} [fintype ι]
+variables {ι κ : Type w} [fintype ι]
 
 open finite_dimensional
 open linear_map
@@ -341,36 +362,120 @@ end eq_sum_embeddings
 
 section det_ne_zero
 
+namespace algebra
+
+variables (A : Type u) {B : Type v} (C : Type z)
+variables [comm_ring A] [comm_ring B] [algebra A B] [comm_ring C] [algebra A C]
+
+open finset
+
+/-- Given an `A`-algebra `B` and `b`, an `κ`-indexed family of elements of `B`, we define
+`trace_matrix A b` as the matrix whose `(i j)`-th element is the trace of `b i * b j`. -/
+@[simp] noncomputable
+def trace_matrix (b : κ → B) : matrix κ κ A
+| i j := trace_form A B (b i) (b j)
+
+lemma trace_matrix_def (b : κ → B) : trace_matrix A b = λ i j, trace_form A B (b i) (b j) := rfl
+
+variables {A}
+
+lemma trace_matrix_of_matrix_vec_mul [fintype κ] (b : κ → B) (P : matrix κ κ A) :
+  trace_matrix A ((P.map (algebra_map A B)).vec_mul b) = Pᵀ ⬝ (trace_matrix A b) ⬝ P :=
+begin
+  ext α β,
+  rw [trace_matrix, vec_mul, dot_product, vec_mul, dot_product, matrix.mul_apply,
+    bilin_form.sum_left, fintype.sum_congr _ _ (λ (i : κ), @bilin_form.sum_right _ _ _ _ _ _ _ _
+    (b i * P.map (algebra_map A B) i α) (λ (y : κ), b y * P.map (algebra_map A B) y β)), sum_comm],
+  congr, ext x,
+  rw [matrix.mul_apply, sum_mul],
+  congr, ext y,
+  rw [map_apply, trace_form_apply, mul_comm (b y), ← smul_def],
+  simp only [id.smul_eq_mul, ring_hom.id_apply, map_apply, transpose_apply, linear_map.map_smulₛₗ,
+    trace_form_apply, algebra.smul_mul_assoc],
+  rw [mul_comm (b x), ← smul_def],
+  ring_nf,
+  simp,
+end
+
+lemma trace_matrix_of_matrix_mul_vec [fintype κ] (b : κ → B) (P : matrix κ κ A) :
+  trace_matrix A ((P.map (algebra_map A B)).mul_vec b) = P ⬝ (trace_matrix A b) ⬝ Pᵀ :=
+begin
+  refine add_equiv.injective transpose_add_equiv _,
+  rw [transpose_add_equiv_apply, transpose_add_equiv_apply, ← vec_mul_transpose,
+    ← transpose_map, trace_matrix_of_matrix_vec_mul, transpose_transpose, transpose_mul,
+    transpose_transpose, transpose_mul]
+end
+
+lemma trace_matrix_of_basis [fintype κ] [decidable_eq κ] (b : basis κ A B) :
+  trace_matrix A b = bilin_form.to_matrix b (trace_form A B) :=
+begin
+  ext i j,
+  rw [trace_matrix, trace_form_apply, trace_form_to_matrix]
+end
+
+variable (A)
+/-- `embeddings_matrix A C b : matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is
+  `σ (b i)`. It is mostly useful for fields when `fintype.card κ = finrank A B` and `C` is
+  algebraically closed. -/
+@[simp] def embeddings_matrix (b : κ → B) : matrix κ (B →ₐ[A] C) C
+| i σ := σ (b i)
+
+/-- `embeddings_matrix_reindex A C b e : matrix κ κ C` is the matrix whose `(i, j)` coefficient
+  is `σⱼ (b i)`, where `σⱼ : B →ₐ[A] C` is the embedding corresponding to `j : κ` given by a
+  bijection `e : κ ≃ (B →ₐ[A] C)`. It is mostly useful for fields and `C` is algebraically closed.
+  In this case, in presence of `h : fintype.card κ = finrank A B`, one can take
+  `e := equiv_of_card_eq ((alg_hom.card A B C).trans h.symm)`. -/
+def embeddings_matrix_reindex (b : κ → B) (e : κ ≃ (B →ₐ[A] C)) :=
+reindex (equiv.refl κ) e.symm (embeddings_matrix A C b)
+
+variable {A}
+
+lemma embeddings_matrix_reindex_eq_vandermonde (pb : power_basis A B)
+  (e : fin pb.dim ≃ (B →ₐ[A] C)) :
+  embeddings_matrix_reindex A C pb.basis e = (vandermonde (λ i, e i pb.gen))ᵀ :=
+by { ext i j, simp [embeddings_matrix_reindex, embeddings_matrix] }
+
+section field
+
+variables (K) {L} (E : Type z) [field E]
+variables [algebra K E]
+variables [module.finite K L] [is_separable K L] [is_alg_closed E]
+variables (b : κ → L) (pb : power_basis K L)
+
+lemma trace_matrix_eq_embeddings_matrix_mul_trans :
+  (trace_matrix K b).map (algebra_map K E) =
+  (embeddings_matrix K E b) ⬝ (embeddings_matrix K E b)ᵀ :=
+by { ext i j, simp [trace_eq_sum_embeddings, embeddings_matrix, matrix.mul_apply] }
+
+lemma trace_matrix_eq_embeddings_matrix_reindex_mul_trans [fintype κ]
+  (e : κ ≃ (L →ₐ[K] E)) : (trace_matrix K b).map (algebra_map K E) =
+  (embeddings_matrix_reindex K E b e) ⬝ (embeddings_matrix_reindex K E b e)ᵀ :=
+by rw [trace_matrix_eq_embeddings_matrix_mul_trans, embeddings_matrix_reindex, reindex_apply,
+  transpose_minor, ← minor_mul_transpose_minor, ← equiv.coe_refl, equiv.refl_symm]
+
+end field
+
+end algebra
+
 open algebra
 
 variables (pb : power_basis K L)
 
-lemma det_trace_form_ne_zero' [is_separable K L] :
-  det (bilin_form.to_matrix pb.basis (trace_form K L)) ≠ 0 :=
+lemma det_trace_matrix_ne_zero' [is_separable K L] :
+  det (trace_matrix K pb.basis) ≠ 0 :=
 begin
-  suffices : algebra_map K (algebraic_closure L)
-    (det (bilin_form.to_matrix pb.basis (trace_form K L))) ≠ 0,
+  suffices : algebra_map K (algebraic_closure L) (det (trace_matrix K pb.basis)) ≠ 0,
   { refine mt (λ ht, _) this,
     rw [ht, ring_hom.map_zero] },
   haveI : finite_dimensional K L := pb.finite_dimensional,
-  let e : (L →ₐ[K] algebraic_closure L) ≃ fin pb.dim := fintype.equiv_fin_of_card_eq _,
-  let M : matrix (fin pb.dim) (fin pb.dim) (algebraic_closure L) :=
-    vandermonde (λ i, e.symm i pb.gen),
-  calc algebra_map K (algebraic_closure _) (bilin_form.to_matrix pb.basis (trace_form K L)).det
-      = det ((algebra_map K _).map_matrix $
-              bilin_form.to_matrix pb.basis (trace_form K L)) : ring_hom.map_det _ _
-  ... = det (Mᵀ ⬝ M) : _
-  ... = det M * det M : by rw [det_mul, det_transpose]
-  ... ≠ 0 : mt mul_self_eq_zero.mp _,
-  { refine congr_arg det _, ext i j,
-    rw [vandermonde_transpose_mul_vandermonde, ring_hom.map_matrix_apply, matrix.map_apply,
-        bilin_form.to_matrix_apply, pb.basis_eq_pow, pb.basis_eq_pow, trace_form_apply,
-        ← pow_add, trace_eq_sum_embeddings (algebraic_closure L), fintype.sum_equiv e],
-    intros σ,
-    rw [e.symm_apply_apply, σ.map_pow] },
+  let e : fin pb.dim ≃ (L →ₐ[K] algebraic_closure L) := (fintype.equiv_fin_of_card_eq _).symm,
+  rw [ring_hom.map_det, ring_hom.map_matrix_apply,
+      trace_matrix_eq_embeddings_matrix_reindex_mul_trans K _ _ e,
+      embeddings_matrix_reindex_eq_vandermonde, det_mul, det_transpose],
+  refine mt mul_self_eq_zero.mp _,
   { simp only [det_vandermonde, finset.prod_eq_zero_iff, not_exists, sub_eq_zero],
     intros i _ j hij h,
-    exact (finset.mem_filter.mp hij).2.ne' (e.symm.injective $ pb.alg_hom_ext h) },
+    exact (finset.mem_filter.mp hij).2.ne' (e.injective $ pb.alg_hom_ext h) },
   { rw [alg_hom.card, pb.finrank] }
 end
 
@@ -385,14 +490,15 @@ begin
   swap, { apply basis.to_matrix_mul_to_matrix_flip },
   refine mul_ne_zero
     (is_unit_of_mul_eq_one _ ((b.to_matrix pb.basis)ᵀ ⬝ b.to_matrix pb.basis).det _).ne_zero
-    (det_trace_form_ne_zero' pb),
-  calc (pb.basis.to_matrix b ⬝ (pb.basis.to_matrix b)ᵀ).det *
-      ((b.to_matrix pb.basis)ᵀ ⬝ b.to_matrix pb.basis).det
-      = (pb.basis.to_matrix b ⬝ (b.to_matrix pb.basis ⬝ pb.basis.to_matrix b)ᵀ ⬝
-        b.to_matrix pb.basis).det
-      : by simp only [← det_mul, matrix.mul_assoc, matrix.transpose_mul]
-  ... = 1 : by simp only [basis.to_matrix_mul_to_matrix_flip, matrix.transpose_one,
-                          matrix.mul_one, matrix.det_one]
+    _,
+  { calc (pb.basis.to_matrix b ⬝ (pb.basis.to_matrix b)ᵀ).det *
+        ((b.to_matrix pb.basis)ᵀ ⬝ b.to_matrix pb.basis).det
+        = (pb.basis.to_matrix b ⬝ (b.to_matrix pb.basis ⬝ pb.basis.to_matrix b)ᵀ ⬝
+          b.to_matrix pb.basis).det
+        : by simp only [← det_mul, matrix.mul_assoc, matrix.transpose_mul]
+    ... = 1 : by simp only [basis.to_matrix_mul_to_matrix_flip, matrix.transpose_one,
+                            matrix.mul_one, matrix.det_one] },
+  simpa only [trace_matrix_of_basis] using det_trace_matrix_ne_zero' pb
 end
 
 variables (K L)