From d403caddc5f83512c40def35742393b003854a5c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 19 May 2022 16:29:55 +0000 Subject: [PATCH] chore(linear_algebra/quadratic_form/basic): remove redundant fields (#14246) This renames `quadratic_form.mk_left` to `quadratic_form.mk` by removing the redundant fields in the structure, as the proof of `mk_left` didn't actually use the fact the ring was commutative as it claimed to in the docstring. The only reason we could possibly want these is if addition were non-commutative, which seems extremely unlikely. --- src/linear_algebra/quadratic_form/basic.lean | 90 ++++++-------------- 1 file changed, 24 insertions(+), 66 deletions(-) diff --git a/src/linear_algebra/quadratic_form/basic.lean b/src/linear_algebra/quadratic_form/basic.lean index cc81cb334b3c0..79bbf74cb0fc3 100644 --- a/src/linear_algebra/quadratic_form/basic.lean +++ b/src/linear_algebra/quadratic_form/basic.lean @@ -90,14 +90,15 @@ end quadratic_form variables [module R M] [module R₁ M] open quadratic_form -/-- A quadratic form over a module. -/ +/-- A quadratic form over a module. + +Note we only need the left lemmas about `quadratic_form.polar` as the right lemmas follow from +`quadratic_form.polar_comm`. -/ structure quadratic_form (R : Type u) (M : Type v) [ring R] [add_comm_group M] [module R M] := (to_fun : M → R) (to_fun_smul : ∀ (a : R) (x : M), to_fun (a • x) = a * a * to_fun x) (polar_add_left' : ∀ (x x' y : M), polar to_fun (x + x') y = polar to_fun x y + polar to_fun x' y) (polar_smul_left' : ∀ (a : R) (x y : M), polar to_fun (a • x) y = a • polar to_fun x y) -(polar_add_right' : ∀ (x y y' : M), polar to_fun x (y + y') = polar to_fun x y + polar to_fun x y') -(polar_smul_right' : ∀ (a : R) (x y : M), polar to_fun x (a • y) = a • polar to_fun x y) namespace quadratic_form @@ -163,12 +164,12 @@ by simp only [add_zero, polar, quadratic_form.map_zero, sub_self] @[simp] lemma polar_add_right (x y y' : M) : polar Q x (y + y') = polar Q x y + polar Q x y' := -Q.polar_add_right' x y y' +by rw [polar_comm Q x, polar_comm Q x, polar_comm Q x, polar_add_left] @[simp] lemma polar_smul_right (a : R) (x y : M) : polar Q x (a • y) = a * polar Q x y := -Q.polar_smul_right' a x y +by rw [polar_comm Q x, polar_comm Q x, polar_smul_left] @[simp] lemma polar_neg_right (x y : M) : @@ -222,9 +223,7 @@ protected def copy (Q : quadratic_form R M) (Q' : M → R) (h : Q' = ⇑Q) : qua { to_fun := Q', to_fun_smul := h.symm ▸ Q.to_fun_smul, polar_add_left' := h.symm ▸ Q.polar_add_left', - polar_smul_left' := h.symm ▸ Q.polar_smul_left', - polar_add_right' := h.symm ▸ Q.polar_add_right', - polar_smul_right' := h.symm ▸ Q.polar_smul_right' } + polar_smul_left' := h.symm ▸ Q.polar_smul_left' } section has_scalar @@ -240,10 +239,6 @@ instance : has_scalar S (quadratic_form R M) := polar_add_left' := λ x x' y, by simp only [polar_smul, polar_add_left, smul_add], polar_smul_left' := λ b x y, begin simp only [polar_smul, polar_smul_left, ←mul_smul_comm, smul_eq_mul], - end, - polar_add_right' := λ x y y', by simp only [polar_smul, polar_add_right, smul_add], - polar_smul_right' := λ b x y, begin - simp only [polar_smul, polar_smul_right, ←mul_smul_comm, smul_eq_mul], end } ⟩ @[simp] lemma coe_fn_smul (a : S) (Q : quadratic_form R M) : ⇑(a • Q) = a • Q := rfl @@ -257,9 +252,7 @@ instance : has_zero (quadratic_form R M) := ⟨ { to_fun := λ x, 0, to_fun_smul := λ a x, by simp only [mul_zero], polar_add_left' := λ x x' y, by simp only [add_zero, polar, sub_self], - polar_smul_left' := λ a x y, by simp only [polar, smul_zero, sub_self], - polar_add_right' := λ x y y', by simp only [add_zero, polar, sub_self], - polar_smul_right' := λ a x y, by simp only [polar, smul_zero, sub_self]} ⟩ + polar_smul_left' := λ a x y, by simp only [polar, smul_zero, sub_self] } ⟩ @[simp] lemma coe_fn_zero : ⇑(0 : quadratic_form R M) = 0 := rfl @@ -275,11 +268,7 @@ instance : has_add (quadratic_form R M) := polar_add_left' := λ x x' y, by simp only [polar_add, polar_add_left, add_assoc, add_left_comm], polar_smul_left' := λ a x y, - by simp only [polar_add, smul_eq_mul, mul_add, polar_smul_left], - polar_add_right' := λ x y y', - by simp only [polar_add, polar_add_right, add_assoc, add_left_comm], - polar_smul_right' := λ a x y, - by simp only [polar_add, smul_eq_mul, mul_add, polar_smul_right] } ⟩ + by simp only [polar_add, smul_eq_mul, mul_add, polar_smul_left], } ⟩ @[simp] lemma coe_fn_add (Q Q' : quadratic_form R M) : ⇑(Q + Q') = Q + Q' := rfl @@ -293,11 +282,7 @@ instance : has_neg (quadratic_form R M) := polar_add_left' := λ x x' y, by simp only [polar_neg, polar_add_left, neg_add], polar_smul_left' := λ a x y, - by simp only [polar_neg, polar_smul_left, mul_neg, smul_eq_mul], - polar_add_right' := λ x y y', - by simp only [polar_neg, polar_add_right, neg_add], - polar_smul_right' := λ a x y, - by simp only [polar_neg, polar_smul_right, mul_neg, smul_eq_mul] } ⟩ + by simp only [polar_neg, polar_smul_left, mul_neg, smul_eq_mul], } ⟩ @[simp] lemma coe_fn_neg (Q : quadratic_form R M) : ⇑(-Q) = -Q := rfl @@ -374,13 +359,7 @@ def comp (Q : quadratic_form R N) (f : M →ₗ[R] N) : simp only [polar, f.map_add], polar_smul_left' := λ a x y, by convert polar_smul_left a (f x) (f y) using 1; - simp only [polar, f.map_smul, f.map_add, smul_eq_mul], - polar_add_right' := λ x y y', - by convert polar_add_right (f x) (f y) (f y') using 1; - simp only [polar, f.map_add], - polar_smul_right' := λ a x y, - by convert polar_smul_right a (f x) (f y) using 1; - simp only [polar, f.map_smul, f.map_add, smul_eq_mul] } + simp only [polar, f.map_smul, f.map_add, smul_eq_mul], } @[simp] lemma comp_apply (Q : quadratic_form R N) (f : M →ₗ[R] N) (x : M) : (Q.comp f) x = Q (f x) := rfl @@ -395,38 +374,21 @@ def _root_.linear_map.comp_quadratic_form {S : Type*} to_fun_smul := λ b x, by rw [function.comp_apply, Q.map_smul_of_tower b x, f.map_smul, smul_eq_mul], polar_add_left' := λ x x' y, by simp only [polar_comp, f.map_add, polar_add_left], - polar_smul_left' := λ b x y, by simp only [polar_comp, f.map_smul, polar_smul_left_of_tower], - polar_add_right' := λ x y y', by simp only [polar_comp, f.map_add, polar_add_right], - polar_smul_right' := λ b x y, by simp only [polar_comp, f.map_smul, polar_smul_right_of_tower], } + polar_smul_left' := λ b x y, by simp only [polar_comp, f.map_smul, polar_smul_left_of_tower], } end comp section comm_ring -/-- Create a quadratic form in a commutative ring by proving only one side of the bilinearity. -/ -def mk_left (f : M → R₁) - (to_fun_smul : ∀ a x, f (a • x) = a * a * f x) - (polar_add_left : ∀ x x' y, polar f (x + x') y = polar f x y + polar f x' y) - (polar_smul_left : ∀ a x y, polar f (a • x) y = a * polar f x y) : - quadratic_form R₁ M := -{ to_fun := f, - to_fun_smul := to_fun_smul, - polar_add_left' := polar_add_left, - polar_smul_left' := polar_smul_left, - polar_add_right' := - λ x y y', by rw [polar_comm, polar_add_left, polar_comm f y x, polar_comm f y' x], - polar_smul_right' := - λ a x y, by rw [polar_comm, polar_smul_left, polar_comm f y x, smul_eq_mul] } - /-- The product of linear forms is a quadratic form. -/ def lin_mul_lin (f g : M →ₗ[R₁] R₁) : quadratic_form R₁ M := -mk_left (f * g) - (λ a x, - by { simp only [smul_eq_mul, ring_hom.id_apply, pi.mul_apply, linear_map.map_smulₛₗ], ring }) - (λ x x' y, by { simp only [polar, pi.mul_apply, linear_map.map_add], ring }) - (λ a x y, begin - simp only [polar, pi.mul_apply, linear_map.map_add, linear_map.map_smul, smul_eq_mul], ring - end) +{ to_fun := f * g, + to_fun_smul := λ a x, + by { simp only [smul_eq_mul, ring_hom.id_apply, pi.mul_apply, linear_map.map_smulₛₗ], ring }, + polar_add_left' := λ x x' y, by { simp only [polar, pi.mul_apply, linear_map.map_add], ring }, + polar_smul_left' := λ a x y, begin + simp only [polar, pi.mul_apply, linear_map.map_add, linear_map.map_smul, smul_eq_mul], ring + end } @[simp] lemma lin_mul_lin_apply (f g : M →ₗ[R₁] R₁) (x) : lin_mul_lin f g x = f x * g x := rfl @@ -486,16 +448,12 @@ by { simp only [add_assoc, add_sub_cancel', add_right, polar, add_left_inj, add_ /-- A bilinear form gives a quadratic form by applying the argument twice. -/ def to_quadratic_form (B : bilin_form R M) : quadratic_form R M := -⟨ λ x, B x x, - λ a x, by simp only [mul_assoc, smul_right, smul_left], - λ x x' y, by simp only [add_assoc, add_right, add_left_inj, polar_to_quadratic_form, add_left, - add_left_comm], - λ a x y, by simp only [smul_add, add_left_inj, polar_to_quadratic_form, - smul_right, smul_eq_mul, smul_left, smul_right, mul_add], - λ x y y', by simp only [add_assoc, add_right, add_left_inj, +{ to_fun := λ x, B x x, + to_fun_smul := λ a x, by simp only [mul_assoc, smul_right, smul_left], + polar_add_left' := λ x x' y, by simp only [add_assoc, add_right, add_left_inj, polar_to_quadratic_form, add_left, add_left_comm], - λ a x y, by simp only [smul_add, add_left_inj, polar_to_quadratic_form, - smul_right, smul_eq_mul, smul_left, smul_right, mul_add]⟩ + polar_smul_left' := λ a x y, by simp only [smul_add, add_left_inj, polar_to_quadratic_form, + smul_right, smul_eq_mul, smul_left, smul_right, mul_add] } @[simp] lemma to_quadratic_form_apply (B : bilin_form R M) (x : M) : B.to_quadratic_form x = B x x :=