feat(linear_algebra/{bilinear,quadratic}_form): inherit scalar actions from algebras (#6586)

For example, this means a quadratic form over the quaternions inherits an `ℝ` action.

Author: eric-wieser

src/linear_algebra/bilinear_form.lean

@@ -146,27 +146,31 @@ instance : inhabited (bilin_form R M) := ⟨0⟩
 
 section
 
-instance {R : Type*} [comm_semiring R] [semimodule R M] : semimodule R (bilin_form R M) :=
+/-- `quadratic_form A M` inherits the scalar action from any algebra over `A`.
+
+When `A` is commutative, this provides an `A`-action via `algebra.id`. -/
+instance {R A : Type*} [comm_semiring R] [semiring A] [algebra R A] [semimodule A M] :
+  semimodule R (bilin_form A M) :=
 { smul := λ c B,
-  { bilin := λ x y, c * B x y,
+  { bilin := λ x y, c • B x y,
     bilin_add_left := λ x y z,
-      by { unfold coe_fn has_coe_to_fun.coe bilin, rw [bilin_add_left, left_distrib] },
+      by { unfold coe_fn has_coe_to_fun.coe bilin, rw [bilin_add_left, smul_add] },
     bilin_smul_left := λ a x y, by { unfold coe_fn has_coe_to_fun.coe bilin,
-      rw [bilin_smul_left, ←mul_assoc, mul_comm c, mul_assoc] },
+      rw [bilin_smul_left, ←algebra.mul_smul_comm] },
     bilin_add_right := λ x y z, by { unfold coe_fn has_coe_to_fun.coe bilin,
-      rw [bilin_add_right, left_distrib] },
+      rw [bilin_add_right, smul_add] },
     bilin_smul_right := λ a x y, by { unfold coe_fn has_coe_to_fun.coe bilin,
-      rw [bilin_smul_right, ←mul_assoc, mul_comm c, mul_assoc] } },
-  smul_add := λ c B D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw left_distrib },
-  add_smul := λ c B D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw right_distrib },
-  mul_smul := λ a c D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw mul_assoc },
-  one_smul := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw one_mul },
-  zero_smul := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw zero_mul },
-  smul_zero := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw mul_zero } }
+      rw [bilin_smul_right, ←algebra.mul_smul_comm] } },
+  smul_add := λ c B D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw smul_add },
+  add_smul := λ c B D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw add_smul },
+  mul_smul := λ a c D, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw ←smul_assoc, refl },
+  one_smul := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw one_smul },
+  zero_smul := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw zero_smul },
+  smul_zero := λ B, by { ext, unfold coe_fn has_coe_to_fun.coe bilin, rw smul_zero } }
 
 @[simp]
-lemma smul_apply {R : Type*} [comm_semiring R] [semimodule R M]
-  (B : bilin_form R M) (a : R) (x y : M) :
+lemma smul_apply {R A : Type*} [comm_semiring R] [semiring A] [algebra R A] [semimodule A M]
+  (B : bilin_form A M) (a : R) (x y : M) :
   (a • B) x y = a • (B x y) :=
 rfl
 

src/linear_algebra/quadratic_form.lean

@@ -239,28 +239,50 @@ by simp [sub_eq_add_neg]
 @[simp] lemma sub_apply (Q Q' : quadratic_form R M) (x : M) : (Q - Q') x = Q x - Q' x :=
 by simp [sub_eq_add_neg]
 
-instance : has_scalar R₁ (quadratic_form R₁ M) :=
-⟨ λ a Q,
-  { to_fun := a • Q,
-    to_fun_smul := λ b x, by simp only [pi.smul_apply, map_smul, smul_eq_mul, mul_left_comm],
-    polar_add_left' := λ x x' y, by simp only [polar_smul, polar_add_left, mul_add],
-    polar_smul_left' := λ b x y,
-      by simp only [polar_smul, polar_smul_left, smul_eq_mul, mul_left_comm],
-    polar_add_right' := λ x y y', by simp only [polar_smul, polar_add_right, mul_add],
-    polar_smul_right' := λ b x y,
-      by simp only [polar_smul, polar_smul_right, smul_eq_mul, mul_left_comm] } ⟩
-
-@[simp] lemma coe_fn_smul (a : R₁) (Q : quadratic_form R₁ M) : ⇑(a • Q) = a • Q := rfl
+section has_scalar
+variables {R₂ : Type u} [comm_semiring R₂]
 
-@[simp] lemma smul_apply (a : R₁) (Q : quadratic_form R₁ M) (x : M) : (a • Q) x = a * Q x := rfl
+/-- `quadratic_form R M` inherits the scalar action from any algebra over `R`.
 
-instance : module R₁ (quadratic_form R₁ M) :=
-{ mul_smul := λ a b Q, ext (λ x, by simp only [smul_apply, mul_left_comm, mul_assoc]),
+When `R` is commutative, this provides an `R`-action via `algebra.id`. -/
+instance [algebra R₂ R] : has_scalar R₂ (quadratic_form R M) :=
+⟨ λ a Q,
+  { to_fun := a • Q,
+    to_fun_smul := λ b x, by rw [pi.smul_apply, map_smul, pi.smul_apply, algebra.mul_smul_comm],
+    polar_add_left' := λ x x' y, begin
+      rw [← one_smul R ⇑Q, ←smul_assoc],
+      simp only [polar_smul, polar_add_left, mul_add],
+    end,
+    polar_smul_left' := λ b x y, begin
+      rw [← one_smul R ⇑Q, ←smul_assoc],
+      simp only [polar_smul, polar_smul_left, smul_eq_mul, algebra.smul_def, ←mul_assoc, mul_one,
+        one_mul, algebra.commutes],
+    end,
+    polar_add_right' := λ x y y', begin
+      rw [← one_smul R ⇑Q, ←smul_assoc],
+      simp only [polar_smul, polar_add_right, mul_add],
+    end,
+    polar_smul_right' := λ b x y, begin
+      rw [← one_smul R ⇑Q, ←smul_assoc],
+      simp only [polar_smul, polar_smul_right, smul_eq_mul, algebra.smul_def, ←mul_assoc, mul_one,
+        one_mul, algebra.commutes],
+    end } ⟩
+
+@[simp] lemma coe_fn_smul [algebra R₂ R] (a : R₂) (Q : quadratic_form R M) : ⇑(a • Q) = a • Q := rfl
+
+@[simp] lemma smul_apply [algebra R₂ R] (a : R₂) (Q : quadratic_form R M) (x : M) :
+  (a • Q) x = a • Q x := rfl
+
+instance [algebra R₂ R] : semimodule R₂ (quadratic_form R M) :=
+{ mul_smul := λ a b Q, ext (λ x, by
+    simp only [smul_apply, mul_left_comm, ←smul_eq_mul, smul_assoc]),
   one_smul := λ Q, ext (λ x, by simp),
-  smul_add := λ a Q Q', by { ext, simp only [add_apply, smul_apply, mul_add] },
-  smul_zero := λ a, by { ext, simp only [zero_apply, smul_apply, mul_zero] },
-  zero_smul := λ Q, by { ext, simp only [zero_apply, smul_apply, zero_mul] },
-  add_smul := λ a b Q, by { ext, simp only [add_apply, smul_apply, add_mul] } }
+  smul_add := λ a Q Q', by { ext, simp only [add_apply, smul_apply, smul_add] },
+  smul_zero := λ a, by { ext, simp only [zero_apply, smul_apply, smul_zero] },
+  zero_smul := λ Q, by { ext, simp only [zero_apply, smul_apply, zero_smul] },
+  add_smul := λ a b Q, by { ext, simp only [add_apply, smul_apply, add_smul] } }
+
+end has_scalar
 
 section comp