From dcd60e25e4913e1b1d8da247e043d9c536073d86 Mon Sep 17 00:00:00 2001
From: Anne Baanen <vierkantor@vierkantor.com>
Date: Fri, 27 Aug 2021 14:36:55 +0000
Subject: [PATCH] feat(ring_theory/trace): the trace form is nondegenerate
 (#8777)

This PR shows the determinant of the trace form is nonzero over a finite separable field extension. This is an important ingredient in showing the integral closure of a Dedekind domain in a finite separable extension is again a Dedekind domain, i.e. that rings of integers are Dedekind domains. We extend the results of #8762 to write the trace form as a Vandermonde matrix to get a nice expression for the determinant, then use separability to show this value is nonzero.
---
 src/linear_algebra/matrix/basis.lean |  5 +++
 src/ring_theory/trace.lean           | 60 ++++++++++++++++++++++++++++
 2 files changed, 65 insertions(+)

diff --git a/src/linear_algebra/matrix/basis.lean b/src/linear_algebra/matrix/basis.lean
index 230871b6a86c0..04691d56bd656 100644
--- a/src/linear_algebra/matrix/basis.lean
+++ b/src/linear_algebra/matrix/basis.lean
@@ -167,6 +167,11 @@ begin
   simp only [matrix.mul_apply, basis.to_matrix_apply, basis.sum_repr_mul_repr],
 end
 
+/-- `b.to_matrix b'` and `b'.to_matrix b` are inverses. -/
+lemma basis.to_matrix_mul_to_matrix_flip [decidable_eq ι] [fintype ι'] :
+  b.to_matrix b' ⬝ b'.to_matrix b = 1 :=
+by rw [basis.to_matrix_mul_to_matrix, basis.to_matrix_self]
+
 @[simp]
 lemma basis.to_matrix_reindex
   (b : basis ι R M) (v : ι' → M) (e : ι ≃ ι') :
diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index 9be2b71913f6c..50d1d8a2c70dc 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -7,6 +7,7 @@ Authors: Anne Baanen
 import linear_algebra.bilinear_form
 import linear_algebra.char_poly.coeff
 import linear_algebra.determinant
+import linear_algebra.vandermonde
 import linear_algebra.trace
 import field_theory.algebraic_closure
 import field_theory.primitive_element
@@ -338,3 +339,62 @@ begin
 end
 
 end eq_sum_embeddings
+
+section det_ne_zero
+
+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 :=
+begin
+  suffices : algebra_map K (algebraic_closure L)
+    (det (bilin_form.to_matrix pb.basis (trace_form K L))) ≠ 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) (pb.is_integral_gen.pow _),
+        fintype.sum_equiv e],
+    intros σ,
+    rw [e.symm_apply_apply, σ.map_pow] },
+  { 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) },
+  { rw [alg_hom.card, pb.finrank] }
+end
+
+lemma det_trace_form_ne_zero  [is_separable K L] [decidable_eq ι] (b : basis ι K L) :
+  det (bilin_form.to_matrix b (trace_form K L)) ≠ 0 :=
+begin
+  haveI : finite_dimensional K L := finite_dimensional.of_fintype_basis b,
+  let pb : power_basis K L := field.power_basis_of_finite_of_separable _ _,
+  rw [← bilin_form.to_matrix_mul_basis_to_matrix pb.basis b,
+      ← det_comm' (pb.basis.to_matrix_mul_to_matrix_flip b) _,
+      ← matrix.mul_assoc, det_mul],
+  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]
+end
+
+end det_ne_zero