refactor(LinearAlgebra/QuadraticForm/Basic): Use bilinear maps for th…

…e companion (#10097)

This PR replaces the companion `(B : BilinForm R M)` of a quadratic form with a bilinear map `(B : M →ₗ[R] M →ₗ[R] R)`.

This is intended as a baby step towards generalising quadratic forms to quadratic maps. In the future we could allow for companion bilinear or even sesquilinear maps into an `R`-module.



Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>
Co-authored-by: Christopher Hoskin <christopher.hoskin@overleaf.com>

Mathlib/LinearAlgebra/BilinearMap.lean

@@ -402,6 +402,13 @@ abbrev _root_.Submodule.restrictBilinear (p : Submodule R M) (f : M →ₗ[R] M
     p →ₗ[R] p →ₗ[R] R :=
   f.compl₁₂ p.subtype p.subtype
 
+/-- `linMulLin f g` is the bilinear form mapping `x` and `y` to `f x * g y` -/
+def linMulLin (f g : M →ₗ[R] R) : M →ₗ[R] M →ₗ[R] R :=
+  LinearMap.mk₂ R (fun x y => f x * g y) (fun x y z => by simp only [map_add, add_mul])
+  (fun _ _ => by simp only [SMulHomClass.map_smul, smul_eq_mul, mul_assoc, forall_const])
+  (fun _ _ _ => by simp only [map_add, mul_add])
+  (fun _ _ => by simp only [SMulHomClass.map_smul, smul_eq_mul, mul_left_comm, forall_const])
+
 end CommSemiring
 
 section CommRing

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -142,7 +142,7 @@ structure QuadraticForm (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoi
     where
   toFun : M → R
   toFun_smul : ∀ (a : R) (x : M), toFun (a • x) = a * a * toFun x
-  exists_companion' : ∃ B : BilinForm R M, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y
+  exists_companion' : ∃ B : M →ₗ[R] M →ₗ[R] R, ∀ x y, toFun (x + y) = toFun x + toFun y + B x y
 #align quadratic_form QuadraticForm
 
 namespace QuadraticForm
@@ -218,15 +218,15 @@ theorem map_smul (a : R) (x : M) : Q (a • x) = a * a * Q x :=
   Q.toFun_smul a x
 #align quadratic_form.map_smul QuadraticForm.map_smul
 
-theorem exists_companion : ∃ B : BilinForm R M, ∀ x y, Q (x + y) = Q x + Q y + B x y :=
+theorem exists_companion : ∃ B : M →ₗ[R] M →ₗ[R] R, ∀ x y, Q (x + y) = Q x + Q y + B x y :=
   Q.exists_companion'
 #align quadratic_form.exists_companion QuadraticForm.exists_companion
 
 theorem map_add_add_add_map (x y z : M) :
     Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x) := by
   obtain ⟨B, h⟩ := Q.exists_companion
   rw [add_comm z x]
-  simp only [h, BilinForm.add_left]
+  simp only [h, map_add, LinearMap.add_apply]
   abel
 #align quadratic_form.map_add_add_add_map QuadraticForm.map_add_add_add_map
 
@@ -278,7 +278,7 @@ theorem polar_add_left (x x' y : M) : polar Q (x + x') y = polar Q x y + polar Q
 @[simp]
 theorem polar_smul_left (a : R) (x y : M) : polar Q (a • x) y = a * polar Q x y := by
   obtain ⟨B, h⟩ := Q.exists_companion
-  simp_rw [polar, h, Q.map_smul, BilinForm.smul_left, sub_sub, add_sub_cancel']
+  simp_rw [polar, h, Q.map_smul, LinearMap.map_smul₂, sub_sub, add_sub_cancel', smul_eq_mul]
 #align quadratic_form.polar_smul_left QuadraticForm.polar_smul_left
 
 @[simp]
@@ -332,6 +332,12 @@ def polarBilin : BilinForm R M where
   bilin_smul_right r x y := by simp_rw [polar_comm _ x, polar_smul_left Q]
 #align quadratic_form.polar_bilin QuadraticForm.polarBilin
 
+/-- `QuadraticForm.polar` as a bilinear map -/
+@[simps!]
+def polarLinearMap₂ : M →ₗ[R] M →ₗ[R] R :=
+  LinearMap.mk₂ R (polar Q) (polar_add_left Q) (polar_smul_left Q) (polar_add_right Q)
+  (polar_smul_right Q)
+
 variable [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M]
 
 @[simp]
@@ -352,20 +358,19 @@ def ofPolar (toFun : M → R) (toFun_smul : ∀ (a : R) (x : M), toFun (a • x)
     QuadraticForm R M :=
   { toFun
     toFun_smul
-    exists_companion' :=
-      ⟨{  bilin := polar toFun
-          bilin_add_left := polar_add_left
-          bilin_smul_left := polar_smul_left
-          bilin_add_right := fun x y z => by simp_rw [polar_comm _ x, polar_add_left]
-          bilin_smul_right := fun r x y => by
-            simp_rw [polar_comm _ x, polar_smul_left, smul_eq_mul] },
-        fun x y => by rw [BilinForm.coeFn_mk, polar, sub_sub, add_sub_cancel'_right]⟩ }
+    exists_companion' := ⟨LinearMap.mk₂ R (polar toFun) (polar_add_left) (polar_smul_left)
+      (fun x _ _ => by simp_rw [polar_comm _ x, polar_add_left])
+      (fun _ _ _ => by rw [polar_comm, polar_smul_left, polar_comm]),
+      fun _ _ =>  by
+        simp only [LinearMap.mk₂_apply]
+        rw [polar, sub_sub, add_sub_cancel'_right]⟩ }
 #align quadratic_form.of_polar QuadraticForm.ofPolar
 
 /-- In a ring the companion bilinear form is unique and equal to `QuadraticForm.polar`. -/
-theorem choose_exists_companion : Q.exists_companion.choose = polarBilin Q :=
-  BilinForm.ext fun x y => by
-    rw [polarBilin_apply, polar, Q.exists_companion.choose_spec, sub_sub, add_sub_cancel']
+theorem choose_exists_companion : Q.exists_companion.choose = polarLinearMap₂ Q :=
+  LinearMap.ext₂ fun x y => by
+    rw [polarLinearMap₂_apply_apply, polar, Q.exists_companion.choose_spec, sub_sub,
+      add_sub_cancel']
 #align quadratic_form.some_exists_companion QuadraticForm.choose_exists_companion
 
 end CommRing
@@ -377,7 +382,7 @@ variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 section SMul
 
 variable [Monoid S] [Monoid T] [DistribMulAction S R] [DistribMulAction T R]
-variable [SMulCommClass S R R] [SMulCommClass T R R]
+variable [SMulCommClass R S R] [SMulCommClass S R R] [SMulCommClass T R R] [SMulCommClass R T R]
 
 /-- `QuadraticForm R M` inherits the scalar action from any algebra over `R`.
 
@@ -411,7 +416,7 @@ end SMul
 instance : Zero (QuadraticForm R M) :=
   ⟨{  toFun := fun _ => 0
       toFun_smul := fun a _ => by simp only [mul_zero]
-      exists_companion' := ⟨0, fun _ _ => by simp only [add_zero, BilinForm.zero_apply]⟩ }⟩
+      exists_companion' := ⟨0, fun _ _ => by simp only [add_zero, LinearMap.zero_apply]⟩ }⟩
 
 @[simp]
 theorem coeFn_zero : ⇑(0 : QuadraticForm R M) = 0 :=
@@ -434,7 +439,7 @@ instance : Add (QuadraticForm R M) :=
         let ⟨B, h⟩ := Q.exists_companion
         let ⟨B', h'⟩ := Q'.exists_companion
         ⟨B + B', fun x y => by
-          simp_rw [Pi.add_apply, h, h', BilinForm.add_apply, add_add_add_comm]⟩ }⟩
+          simp_rw [Pi.add_apply, h, h', LinearMap.add_apply, add_add_add_comm]⟩ }⟩
 
 @[simp]
 theorem coeFn_add (Q Q' : QuadraticForm R M) : ⇑(Q + Q') = Q + Q' :=
@@ -481,7 +486,7 @@ theorem sum_apply {ι : Type*} (Q : ι → QuadraticForm R M) (s : Finset ι) (x
 
 end Sum
 
-instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] :
+instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] [SMulCommClass R S R] :
     DistribMulAction S (QuadraticForm R M) where
   mul_smul a b Q := ext fun x => by simp only [smul_apply, mul_smul]
   one_smul Q := ext fun x => by simp only [QuadraticForm.smul_apply, one_smul]
@@ -492,7 +497,8 @@ instance [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] :
     ext
     simp only [zero_apply, smul_apply, smul_zero]
 
-instance [Semiring S] [Module S R] [SMulCommClass S R R] : Module S (QuadraticForm R M) where
+instance [Semiring S] [Module S R] [SMulCommClass S R R] [SMulCommClass R S R] :
+    Module S (QuadraticForm R M) where
   zero_smul Q := by
     ext
     simp only [zero_apply, smul_apply, zero_smul]
@@ -512,7 +518,7 @@ instance : Neg (QuadraticForm R M) :=
       toFun_smul := fun a x => by simp only [Pi.neg_apply, map_smul, mul_neg]
       exists_companion' :=
         let ⟨B, h⟩ := Q.exists_companion
-        ⟨-B, fun x y => by simp_rw [Pi.neg_apply, h, BilinForm.neg_apply, neg_add]⟩ }⟩
+        ⟨-B, fun x y => by simp_rw [Pi.neg_apply, h, LinearMap.neg_apply, neg_add]⟩ }⟩
 
 @[simp]
 theorem coeFn_neg (Q : QuadraticForm R M) : ⇑(-Q) = -Q :=
@@ -555,7 +561,7 @@ def comp (Q : QuadraticForm R N) (f : M →ₗ[R] N) : QuadraticForm R M where
   toFun_smul a x := by simp only [map_smul, f.map_smul]
   exists_companion' :=
     let ⟨B, h⟩ := Q.exists_companion
-    ⟨B.comp f f, fun x y => by simp_rw [f.map_add, h, BilinForm.comp_apply]⟩
+    ⟨B.compl₁₂ f f, fun x y => by simp_rw [f.map_add]; exact h (f x) (f y)⟩
 #align quadratic_form.comp QuadraticForm.comp
 
 @[simp]
@@ -571,7 +577,9 @@ def _root_.LinearMap.compQuadraticForm [CommSemiring S] [Algebra S R] [Module S
   toFun_smul b x := by simp only [Q.map_smul_of_tower b x, f.map_smul, smul_eq_mul]
   exists_companion' :=
     let ⟨B, h⟩ := Q.exists_companion
-    ⟨f.compBilinForm B, fun x y => by simp_rw [h, f.map_add, LinearMap.compBilinForm_apply]⟩
+    ⟨(LinearMap.restrictScalars S (LinearMap.restrictScalars S B.flip).flip).compr₂ f, fun x y => by
+      simp_rw [h, f.map_add]
+      rfl⟩
 #align linear_map.comp_quadratic_form LinearMap.compQuadraticForm
 
 end Comp
@@ -587,9 +595,10 @@ def linMulLin (f g : M →ₗ[R] R) : QuadraticForm R M where
     simp only [smul_eq_mul, RingHom.id_apply, Pi.mul_apply, LinearMap.map_smulₛₗ]
     ring
   exists_companion' :=
-    ⟨BilinForm.linMulLin f g + BilinForm.linMulLin g f, fun x y => by
-      simp only [Pi.mul_apply, map_add, BilinForm.add_apply, BilinForm.linMulLin_apply]
-      ring⟩
+    ⟨LinearMap.linMulLin f g + LinearMap.linMulLin g f, fun x y => by
+      simp only [Pi.mul_apply, map_add, LinearMap.linMulLin, LinearMap.add_apply,
+        LinearMap.mk₂_apply]
+      ring_nf⟩
 #align quadratic_form.lin_mul_lin QuadraticForm.linMulLin
 
 @[simp]
@@ -654,13 +663,19 @@ section Semiring
 
 variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 
+/-- A bilinear map into `R` gives a quadratic form by applying the argument twice. -/
+def _root_.LinearMap.toQuadraticForm (B: M →ₗ[R] M →ₗ[R] R) : QuadraticForm R M where
+  toFun x := B x x
+  toFun_smul a x := by
+    simp only [SMulHomClass.map_smul, LinearMap.smul_apply, smul_eq_mul, mul_assoc]
+  exists_companion' := ⟨B + B.flip,
+    fun x y => by simp only [map_add, LinearMap.add_apply, LinearMap.flip_apply]; abel⟩
+
 variable {B : BilinForm R M}
 
 /-- A bilinear form gives a quadratic form by applying the argument twice. -/
-def toQuadraticForm (B : BilinForm R M) : QuadraticForm R M where
-  toFun x := B x x
-  toFun_smul a x := by simp only [mul_assoc, smul_right, smul_left]
-  exists_companion' := ⟨B + BilinForm.flipHom ℕ B, fun x y => by simp [add_add_add_comm, add_comm]⟩
+def toQuadraticForm (B : BilinForm R M) : QuadraticForm R M :=
+  B.toLin.toQuadraticForm
 #align bilin_form.to_quadratic_form BilinForm.toQuadraticForm
 
 @[simp]
@@ -686,8 +701,9 @@ theorem toQuadraticForm_add (B₁ B₂ : BilinForm R M) :
 #align bilin_form.to_quadratic_form_add BilinForm.toQuadraticForm_add
 
 @[simp]
-theorem toQuadraticForm_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (a : S)
-    (B : BilinForm R M) : (a • B).toQuadraticForm = a • B.toQuadraticForm :=
+theorem toQuadraticForm_smul [Monoid S] [DistribMulAction S R] [SMulCommClass S R R]
+    [SMulCommClass R S R] (a : S) (B : BilinForm R M) :
+    (a • B).toQuadraticForm = a • B.toQuadraticForm :=
   rfl
 #align bilin_form.to_quadratic_form_smul BilinForm.toQuadraticForm_smul
 
@@ -705,7 +721,7 @@ def toQuadraticFormAddMonoidHom : BilinForm R M →+ QuadraticForm R M where
 
 /-- `BilinForm.toQuadraticForm` as a linear map -/
 @[simps!]
-def toQuadraticFormLinearMap [Semiring S] [Module S R] [SMulCommClass S R R] :
+def toQuadraticFormLinearMap [Semiring S] [Module S R] [SMulCommClass S R R] [SMulCommClass R S R] :
     BilinForm R M →ₗ[S] QuadraticForm R M where
   toFun := toQuadraticForm
   map_smul' := toQuadraticForm_smul
@@ -1276,16 +1292,17 @@ variable (R)
 
 The weights are applied using `•`; typically this definition is used either with `S = R` or
 `[Algebra S R]`, although this is stated more generally. -/
-def weightedSumSquares [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] (w : ι → S) :
-    QuadraticForm R (ι → R) :=
+def weightedSumSquares [Monoid S] [DistribMulAction S R] [SMulCommClass S R R] [SMulCommClass R S R]
+    (w : ι → S) : QuadraticForm R (ι → R) :=
   ∑ i : ι, w i • proj i i
 #align quadratic_form.weighted_sum_squares QuadraticForm.weightedSumSquares
 
 end
 
 @[simp]
 theorem weightedSumSquares_apply [Monoid S] [DistribMulAction S R] [SMulCommClass S R R]
-    (w : ι → S) (v : ι → R) : weightedSumSquares R w v = ∑ i : ι, w i • (v i * v i) :=
+    [SMulCommClass R S R] (w : ι → S) (v : ι → R) :
+    weightedSumSquares R w v = ∑ i : ι, w i • (v i * v i) :=
   QuadraticForm.sum_apply _ _ _
 #align quadratic_form.weighted_sum_squares_apply QuadraticForm.weightedSumSquares_apply
 

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

@@ -13,7 +13,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Prod
 
 ## Main definitions
 
-* `BilinForm.dualProd R M`, the bilinear form on `(f, x) : Module.Dual R M × M` defined as
+* `LinearMap.dualProd R M`, the bilinear form on `(f, x) : Module.Dual R M × M` defined as
   `f x`.
 * `QuadraticForm.dualProd R M`, the quadratic form on `(f, x) : Module.Dual R M × M` defined as
   `f x`.
@@ -25,7 +25,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Prod
 
 variable (R M N : Type*)
 
-namespace BilinForm
+namespace LinearMap
 
 section Semiring
 
@@ -34,50 +34,46 @@ variable [CommSemiring R] [AddCommMonoid M] [Module R M]
 /-- The symmetric bilinear form on `Module.Dual R M × M` defined as
 `B (f, x) (g, y) = f y + g x`. -/
 @[simps!]
-def dualProd : BilinForm R (Module.Dual R M × M) :=
-  LinearMap.toBilin <|
-    (LinearMap.applyₗ.comp (LinearMap.snd R (Module.Dual R M) M)).compl₂
-        (LinearMap.fst R (Module.Dual R M) M) +
-      ((LinearMap.applyₗ.comp (LinearMap.snd R (Module.Dual R M) M)).compl₂
-          (LinearMap.fst R (Module.Dual R M) M)).flip
-#align bilin_form.dual_prod BilinForm.dualProd
+def dualProd : (Module.Dual R M × M) →ₗ[R] (Module.Dual R M × M) →ₗ[R] R :=
+    (applyₗ.comp (snd R (Module.Dual R M) M)).compl₂ (fst R (Module.Dual R M) M) +
+      ((applyₗ.comp (snd R (Module.Dual R M) M)).compl₂ (fst R (Module.Dual R M) M)).flip
+#align bilin_form.dual_prod LinearMap.dualProd
 
 theorem isSymm_dualProd : (dualProd R M).IsSymm := fun _x _y => add_comm _ _
-#align bilin_form.is_symm_dual_prod BilinForm.isSymm_dualProd
+#align bilin_form.is_symm_dual_prod LinearMap.isSymm_dualProd
 
 end Semiring
 
 section Ring
 
 variable [CommRing R] [AddCommGroup M] [Module R M]
 
-theorem nondenerate_dualProd :
-    (dualProd R M).Nondegenerate ↔ Function.Injective (Module.Dual.eval R M) := by
+theorem separatingLeft_dualProd :
+    (dualProd R M).SeparatingLeft ↔ Function.Injective (Module.Dual.eval R M) := by
   classical
-  rw [nondegenerate_iff_ker_eq_bot]
-  rw [LinearMap.ker_eq_bot]
+  rw [separatingLeft_iff_ker_eq_bot, ker_eq_bot]
   let e := LinearEquiv.prodComm R _ _ ≪≫ₗ Module.dualProdDualEquivDual R (Module.Dual R M) M
-  let h_d := e.symm.toLinearMap.comp (BilinForm.toLin <| dualProd R M)
+  let h_d := e.symm.toLinearMap.comp (dualProd R M)
   refine' (Function.Injective.of_comp_iff e.symm.injective
-    (BilinForm.toLin <| dualProd R M)).symm.trans _
-  rw [← LinearEquiv.coe_toLinearMap, ← LinearMap.coe_comp]
+    (dualProd R M)).symm.trans _
+  rw [← LinearEquiv.coe_toLinearMap, ← coe_comp]
   change Function.Injective h_d ↔ _
-  have : h_d = LinearMap.prodMap LinearMap.id (Module.Dual.eval R M) := by
-    refine' LinearMap.ext fun x => Prod.ext _ _
+  have : h_d = prodMap id (Module.Dual.eval R M) := by
+    refine' ext fun x => Prod.ext _ _
     · ext
       dsimp [Module.Dual.eval, LinearEquiv.prodComm]
       simp
     · ext
       dsimp [Module.Dual.eval, LinearEquiv.prodComm]
       simp
-  rw [this, LinearMap.coe_prodMap]
+  rw [this, coe_prodMap]
   refine' Prod.map_injective.trans _
   exact and_iff_right Function.injective_id
-#align bilin_form.nondenerate_dual_prod BilinForm.nondenerate_dualProd
+#align bilin_form.nondenerate_dual_prod LinearMap.separatingLeft_dualProd
 
 end Ring
 
-end BilinForm
+end LinearMap
 
 namespace QuadraticForm
 
@@ -94,18 +90,18 @@ def dualProd : QuadraticForm R (Module.Dual R M × M) where
     rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, LinearMap.map_smul, smul_eq_mul,
       smul_eq_mul, mul_assoc]
   exists_companion' :=
-    ⟨BilinForm.dualProd R M, fun p q => by
+    ⟨LinearMap.dualProd R M, fun p q => by
       dsimp only  -- porting note: added
-      rw [BilinForm.dualProd_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
+      rw [LinearMap.dualProd_apply_apply, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add,
         map_add, add_right_comm _ (q.1 q.2), add_comm (q.1 p.2) (p.1 q.2), ← add_assoc, ←
         add_assoc]⟩
 #align quadratic_form.dual_prod QuadraticForm.dualProd
 
 @[simp]
-theorem _root_.BilinForm.dualProd.toQuadraticForm :
-    (BilinForm.dualProd R M).toQuadraticForm = 2 • dualProd R M :=
+theorem _root_.LinearMap.dualProd.toQuadraticForm :
+    (LinearMap.dualProd R M).toQuadraticForm = 2 • dualProd R M :=
   ext fun _a => (two_nsmul _).symm
-#align bilin_form.dual_prod.to_quadratic_form BilinForm.dualProd.toQuadraticForm
+#align bilin_form.dual_prod.to_quadratic_form LinearMap.dualProd.toQuadraticForm
 
 variable {R M N}