refactor(RingTheory/Trace): Define TraceForm with LinearMap.BilinForm

Mathlib/FieldTheory/Finite/Trace.lean

@@ -26,7 +26,7 @@ theorem trace_to_zmod_nondegenerate (F : Type*) [Field F] [Finite F]
     [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) :
     ∃ b : F, Algebra.trace (ZMod (ringChar F)) F (a * b) ≠ 0 := by
   haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
-  have htr := traceForm_nondegenerate (ZMod (ringChar F)) F a
+  have htr := traceForm_separatingLeft (ZMod (ringChar F)) F a
   simp_rw [Algebra.traceForm_apply] at htr
   by_contra! hf
   exact ha (htr hf)

Mathlib/NumberTheory/ClassNumber/Finite.lean

@@ -380,7 +380,7 @@ noncomputable def fintypeOfAdmissibleOfFinite : Fintype (ClassGroup S) := by
   choose s b hb_int using FiniteDimensional.exists_is_basis_integral R K L
 -- Porting note: `this` and `f` below where solved at the end rather than being defined at first.
   have : LinearIndependent R ((Algebra.traceForm K L).dualBasis
-      (traceForm_nondegenerate K L) b) := by
+      (traceForm_separatingLeft K L) b) := by
     refine' (Basis.linearIndependent _).restrict_scalars _
     simp only [Algebra.smul_def, mul_one]
     apply IsFractionRing.injective

Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

@@ -5,10 +5,10 @@ Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
 -/
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
-import Mathlib.LinearAlgebra.BilinearForm.DualLattice
 import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.Localization.Module
 import Mathlib.RingTheory.Trace
+import Mathlib.LinearAlgebra.BilinearForm.DualLattice
 
 #align_import ring_theory.dedekind_domain.integral_closure from "leanprover-community/mathlib"@"4cf7ca0e69e048b006674cf4499e5c7d296a89e0"
 
@@ -94,20 +94,19 @@ variable {A K L}
 theorem IsIntegralClosure.range_le_span_dualBasis [IsSeparable K L] {ι : Type*} [Fintype ι]
     [DecidableEq ι] (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
     LinearMap.range ((Algebra.linearMap C L).restrictScalars A) ≤
-    Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
+    Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_separatingLeft K L) b) := by
   rw [← LinearMap.BilinForm.dualSubmodule_span_of_basis,
     ← LinearMap.BilinForm.le_flip_dualSubmodule, Submodule.span_le]
   rintro _ ⟨i, rfl⟩ _ ⟨y, rfl⟩
-  simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.BilinForm.flip_apply,
-    traceForm_apply]
+  simp only [LinearMap.coe_restrictScalars, linearMap_apply, LinearMap.flip_apply, traceForm_apply]
   refine IsIntegrallyClosed.isIntegral_iff.mp ?_
   exact isIntegral_trace ((IsIntegralClosure.isIntegral A L y).algebraMap.mul (hb_int i))
 #align is_integral_closure.range_le_span_dual_basis IsIntegralClosure.range_le_span_dualBasis
 
 theorem integralClosure_le_span_dualBasis [IsSeparable K L] {ι : Type*} [Fintype ι] [DecidableEq ι]
     (b : Basis ι K L) (hb_int : ∀ i, IsIntegral A (b i)) [IsIntegrallyClosed A] :
     Subalgebra.toSubmodule (integralClosure A L) ≤
-    Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_nondegenerate K L) b) := by
+    Submodule.span A (Set.range <| (traceForm K L).dualBasis (traceForm_separatingLeft K L) b) := by
   refine' le_trans _ (IsIntegralClosure.range_le_span_dualBasis (integralClosure A L) b hb_int)
   intro x hx
   exact ⟨⟨x, hx⟩, rfl⟩
@@ -177,7 +176,7 @@ theorem IsIntegralClosure.isNoetherian [IsIntegrallyClosed A] [IsNoetherianRing
     IsNoetherian A C := by
   haveI := Classical.decEq L
   obtain ⟨s, b, hb_int⟩ := FiniteDimensional.exists_is_basis_integral A K L
-  let b' := (traceForm K L).dualBasis (traceForm_nondegenerate K L) b
+  let b' := (traceForm K L).dualBasis (traceForm_separatingLeft K L) b
   letI := isNoetherian_span_of_finite A (Set.finite_range b')
   let f : C →ₗ[A] Submodule.span A (Set.range b') :=
     (Submodule.inclusion (IsIntegralClosure.range_le_span_dualBasis C b hb_int)).comp

Mathlib/RingTheory/Discriminant.lean

@@ -135,8 +135,8 @@ variable [Module.Finite K L] [IsAlgClosed E]
 /-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`. -/
 theorem discr_not_zero_of_basis [IsSeparable K L] (b : Basis ι K L) :
     discr K b ≠ 0 := by
-  rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]
-  exact traceForm_nondegenerate _ _
+  rw [discr_def, traceMatrix_of_basis, ← LinearMap.separatingLeft_iff_det_ne_zero]
+  exact traceForm_separatingLeft _ _
 #align algebra.discr_not_zero_of_basis Algebra.discr_not_zero_of_basis
 
 /-- If `b` is a basis of a finite separable field extension `L/K`,

Mathlib/RingTheory/Trace.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.LinearAlgebra.Matrix.BilinearForm
+import Mathlib.LinearAlgebra.Matrix.SesquilinearForm
 import Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
 import Mathlib.LinearAlgebra.Determinant
 import Mathlib.LinearAlgebra.FiniteDimensional
@@ -14,6 +14,7 @@ import Mathlib.FieldTheory.PrimitiveElement
 import Mathlib.FieldTheory.Galois
 import Mathlib.RingTheory.PowerBasis
 import Mathlib.FieldTheory.Minpoly.MinpolyDiv
+import Mathlib.LinearAlgebra.BilinearForm.Properties
 
 #align_import ring_theory.trace from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
 
@@ -82,6 +83,8 @@ open scoped BigOperators
 
 open scoped Matrix
 
+open LinearMap (BilinForm)
+
 namespace Algebra
 
 variable (b : Basis ι R S)
@@ -206,12 +209,13 @@ theorem traceForm_isSymm : (traceForm R S).IsSymm := fun _ _ => congr_arg (trace
 #align algebra.trace_form_is_symm Algebra.traceForm_isSymm
 
 theorem traceForm_toMatrix [DecidableEq ι] (i j) :
-    BilinForm.toMatrix b (traceForm R S) i j = trace R S (b i * b j) := by
-  rw [BilinForm.toMatrix_apply, traceForm_apply]
+    LinearMap.toMatrix₂ b b (traceForm R S) i j = trace R S (b i * b j) := by
+  rw [LinearMap.toMatrix₂_apply, traceForm_apply]
 #align algebra.trace_form_to_matrix Algebra.traceForm_toMatrix
 
 theorem traceForm_toMatrix_powerBasis (h : PowerBasis R S) :
-    BilinForm.toMatrix h.basis (traceForm R S) = of fun i j => trace R S (h.gen ^ (i.1 + j.1)) :=
+    LinearMap.toMatrix₂ h.basis h.basis (traceForm R S) = of fun i j =>
+    trace R S (h.gen ^ (i.1 + j.1)) :=
   by ext; rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]
 #align algebra.trace_form_to_matrix_power_basis Algebra.traceForm_toMatrix_powerBasis
 
@@ -471,12 +475,8 @@ variable {A}
 theorem traceMatrix_of_matrix_vecMul [Fintype κ] (b : κ → B) (P : Matrix κ κ A) :
     traceMatrix A (b ᵥ* P.map (algebraMap A B)) = Pᵀ * traceMatrix A b * P := by
   ext (α β)
-  rw [traceMatrix_apply, vecMul, dotProduct, vecMul, dotProduct, Matrix.mul_apply,
-    BilinForm.sum_left,
-    Fintype.sum_congr _ _ fun i : κ =>
-      BilinForm.sum_right _ _ (b i * P.map (algebraMap A B) i α) fun y : κ =>
-        b y * P.map (algebraMap A B) y β,
-    sum_comm]
+  rw [traceMatrix_apply, vecMul, dotProduct, vecMul, dotProduct, Matrix.mul_apply, map_sum₂,
+    Fintype.sum_congr _ _ fun i : κ => map_sum _ _ _, sum_comm]
   congr; ext x
   rw [Matrix.mul_apply, sum_mul]
   congr; ext y
@@ -497,7 +497,7 @@ theorem traceMatrix_of_matrix_mulVec [Fintype κ] (b : κ → B) (P : Matrix κ
 #align algebra.trace_matrix_of_matrix_mul_vec Algebra.traceMatrix_of_matrix_mulVec
 
 theorem traceMatrix_of_basis [Fintype κ] [DecidableEq κ] (b : Basis κ A B) :
-    traceMatrix A b = BilinForm.toMatrix b (traceForm A B) := by
+    traceMatrix A b = LinearMap.toMatrix₂ b b (traceForm A B) := by
   ext (i j)
   rw [traceMatrix_apply, traceForm_apply, traceForm_toMatrix]
 #align algebra.trace_matrix_of_basis Algebra.traceMatrix_of_basis
@@ -602,12 +602,13 @@ theorem det_traceMatrix_ne_zero' [IsSeparable K L] : det (traceMatrix K pb.basis
   · rw [AlgHom.card, pb.finrank]
 #align det_trace_matrix_ne_zero' det_traceMatrix_ne_zero'
 
+
 theorem det_traceForm_ne_zero [IsSeparable K L] [DecidableEq ι] (b : Basis ι K L) :
-    det (BilinForm.toMatrix b (traceForm K L)) ≠ 0 := by
+    det (LinearMap.toMatrix₂ b b (traceForm K L)) ≠ 0 := by
   haveI : FiniteDimensional K L := FiniteDimensional.of_fintype_basis b
   let pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable _ _
-  rw [← BilinForm.toMatrix_mul_basis_toMatrix pb.basis b, ←
-    det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _, ← Matrix.mul_assoc, det_mul]
+  rw [← LinearMap.toMatrix₂_mul_basis_toMatrix pb.basis pb.basis, ← det_comm', ← Matrix.mul_assoc,
+    det_mul]
   swap; · apply Basis.toMatrix_mul_toMatrix_flip
   refine'
     mul_ne_zero
@@ -622,15 +623,15 @@ theorem det_traceForm_ne_zero [IsSeparable K L] [DecidableEq ι] (b : Basis ι K
         simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
           Matrix.det_one]
   simpa only [traceMatrix_of_basis] using det_traceMatrix_ne_zero' pb
+  rw [Basis.toMatrix_mul_toMatrix_flip]
 #align det_trace_form_ne_zero det_traceForm_ne_zero
 
 variable (K L)
 
-theorem traceForm_nondegenerate [FiniteDimensional K L] [IsSeparable K L] :
-    (traceForm K L).Nondegenerate :=
-  BilinForm.nondegenerate_of_det_ne_zero (traceForm K L) _
-    (det_traceForm_ne_zero (FiniteDimensional.finBasis K L))
-#align trace_form_nondegenerate traceForm_nondegenerate
+theorem traceForm_separatingLeft [FiniteDimensional K L] [IsSeparable K L] :
+    (traceForm K L).SeparatingLeft :=
+  separatingLeft_of_det_ne_zero _ (det_traceForm_ne_zero (FiniteDimensional.finBasis K L))
+#align trace_form_nondegenerate traceForm_separatingLeft
 
 theorem Algebra.trace_ne_zero [FiniteDimensional K L] [IsSeparable K L] :
     Algebra.trace K L ≠ 0 := by
@@ -656,10 +657,10 @@ with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
 -/
 lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [IsSeparable K L]
     (pb : PowerBasis K L) (i) :
-    (Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i =
+    (Algebra.traceForm K L).dualBasis (traceForm_separatingLeft K L) pb.basis i =
       (minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen) := by
   classical
-  apply ((Algebra.traceForm K L).toDual (traceForm_nondegenerate K L)).injective
+  apply ((Algebra.traceForm K L).toDual (traceForm_separatingLeft K L)).injective
   apply pb.basis.ext
   intro j
   simp only [BilinForm.toDual_def, BilinForm.apply_dualBasis_left]