feat(LinearAlgebra/QuadraticForm/Basic): more lemmas (#7196)

This also adds a handful of missing lemmas about `Set.center` for inverses and numeric literals.

Author: eric-wieser

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -4,7 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser, Jireh Loreaux
 -/
 import Mathlib.Algebra.Ring.Defs
+import Mathlib.Algebra.Group.Commute.Units
+import Mathlib.Algebra.Invertible.Basic
 import Mathlib.GroupTheory.Subsemigroup.Operations
+import Mathlib.Data.Int.Cast.Lemmas
 
 #align_import group_theory.subsemigroup.center from "leanprover-community/mathlib"@"1ac8d4304efba9d03fa720d06516fac845aa5353"
 
@@ -56,6 +59,19 @@ theorem one_mem_center [MulOneClass M] : (1 : M) ∈ Set.center M := by simp [me
 theorem zero_mem_center [MulZeroClass M] : (0 : M) ∈ Set.center M := by simp [mem_center_iff]
 #align set.zero_mem_center Set.zero_mem_center
 
+@[simp]
+theorem natCast_mem_center [NonAssocSemiring M] (n : ℕ) : (n : M) ∈ Set.center M :=
+  (Nat.commute_cast · _)
+
+@[simp]
+theorem ofNat_mem_center [NonAssocSemiring M] (n : ℕ) [n.AtLeastTwo] :
+    OfNat.ofNat n ∈ Set.center M :=
+  natCast_mem_center M n
+
+@[simp]
+theorem intCast_mem_center [NonAssocRing M] (n : ℤ) : (n : M) ∈ Set.center M :=
+  (Int.commute_cast · _)
+
 variable {M}
 
 @[to_additive (attr := simp) add_mem_addCenter]
@@ -100,14 +116,23 @@ theorem center_units_eq [GroupWithZero M] : Set.center Mˣ = ((↑) : Mˣ → M)
   Subset.antisymm center_units_subset subset_center_units
 #align set.center_units_eq Set.center_units_eq
 
+@[simp]
+theorem units_inv_mem_center [Monoid M] {a : Mˣ} (ha : ↑a ∈ Set.center M) :
+    ↑a⁻¹ ∈ Set.center M :=
+  (Commute.units_inv_right <| ha ·)
+
+@[simp]
+theorem invOf_mem_center [Monoid M] {a : M} [Invertible a] (ha : a ∈ Set.center M) :
+    ⅟a ∈ Set.center M :=
+  (Commute.invOf_right <| ha ·)
+
 @[simp]
 theorem inv_mem_center₀ [GroupWithZero M] {a : M} (ha : a ∈ Set.center M) : a⁻¹ ∈ Set.center M := by
   obtain rfl | ha0 := eq_or_ne a 0
   · rw [inv_zero]
     exact zero_mem_center M
-  rcases IsUnit.mk0 _ ha0 with ⟨a, rfl⟩
-  rw [← Units.val_inv_eq_inv_val]
-  exact center_units_subset (inv_mem_center (subset_center_units ha))
+  · lift a to Mˣ using IsUnit.mk0 _ ha0
+    simpa only [Units.val_inv_eq_inv_val] using units_inv_mem_center ha
 #align set.inv_mem_center₀ Set.inv_mem_center₀
 
 @[to_additive (attr := simp) sub_mem_addCenter]

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -553,7 +553,7 @@ theorem comp_apply (Q : QuadraticForm R N) (f : M →ₗ[R] N) (x : M) : (Q.comp
 
 /-- Compose a quadratic form with a linear function on the left. -/
 @[simps (config := { simpRhs := true })]
-def _root_.LinearMap.compQuadraticForm {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
+def _root_.LinearMap.compQuadraticForm [CommSemiring S] [Algebra S R] [Module S M]
     [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) : QuadraticForm S M where
   toFun x := f (Q x)
   toFun_smul b x := by simp only [Q.map_smul_of_tower b x, f.map_smul, smul_eq_mul]
@@ -732,11 +732,6 @@ variable [Ring R] [AddCommGroup M] [Module R M]
 
 variable {B : BilinForm R M}
 
-theorem polar_to_quadratic_form (x y : M) : polar (fun x => B x x) x y = B x y + B y x := by
-  simp only [add_assoc, add_sub_cancel', add_right, polar, add_left_inj, add_neg_cancel_left,
-    add_left, sub_eq_add_neg _ (B y y), add_comm (B y x) _]
-#align bilin_form.polar_to_quadratic_form BilinForm.polar_to_quadratic_form
-
 @[simp]
 theorem toQuadraticForm_neg (B : BilinForm R M) : (-B).toQuadraticForm = -B.toQuadraticForm :=
   rfl
@@ -748,6 +743,24 @@ theorem toQuadraticForm_sub (B₁ B₂ : BilinForm R M) :
   rfl
 #align bilin_form.to_quadratic_form_sub BilinForm.toQuadraticForm_sub
 
+theorem polar_toQuadraticForm (x y : M) : polar (toQuadraticForm B) x y = B x y + B y x := by
+  simp only [toQuadraticForm_apply, add_assoc, add_sub_cancel', add_right, polar, add_left_inj,
+    add_neg_cancel_left, add_left, sub_eq_add_neg _ (B y y), add_comm (B y x) _]
+#align bilin_form.polar_to_quadratic_form BilinForm.polar_toQuadraticForm
+
+theorem polarBilin_toQuadraticForm : polarBilin (toQuadraticForm B) = B + flip' B :=
+  BilinForm.ext polar_toQuadraticForm
+
+variable [CommRing S] [Algebra S R] [Module S M] [IsScalarTower S R M]
+
+theorem _root_.LinearMap.compQuadraticForm_polar (f : R →ₗ[S] S) (Q : QuadraticForm R M) (x y : M) :
+    polar (f.compQuadraticForm Q) x y = f (polar Q x y) := by
+  simp [polar]
+
+theorem _root_.LinearMap.compQuadraticForm_polarBilin (f : R →ₗ[S] S) (Q : QuadraticForm R M) :
+    (f.compQuadraticForm Q).polarBilin = f.compBilinForm Q.polarBilin :=
+  ext <| LinearMap.compQuadraticForm_polar _ _
+
 end Ring
 
 end BilinForm
@@ -771,18 +784,11 @@ where `S` is a commutative subring of `R`.
 Over a commutative ring, use `QuadraticForm.associated`, which gives an `R`-linear map.  Over a
 general ring with no nontrivial distinguished commutative subring, use `QuadraticForm.associated'`,
 which gives an additive homomorphism (or more precisely a `ℤ`-linear map.) -/
-def associatedHom : QuadraticForm R M →ₗ[S] BilinForm R M where
-  toFun Q :=
-    (⟨⅟ 2, fun x => (Commute.ofNat_right x 2).invOf_right⟩ : Submonoid.center R) • Q.polarBilin
-  map_add' Q Q' := by
-    ext
-    simp only [BilinForm.add_apply, BilinForm.smul_apply, coeFn_mk, polarBilin_apply, polar_add,
-      coeFn_add, smul_add]
-  map_smul' s Q := by
-    ext
-    -- porting note: added type annotations
-    simp only [RingHom.id_apply, polar_smul, smul_comm s (_ : Submonoid.center R) (_ : R),
-      polarBilin_apply, coeFn_mk, coeFn_smul, BilinForm.smul_apply]
+def associatedHom : QuadraticForm R M →ₗ[S] BilinForm R M :=
+  (⟨⅟2, Set.invOf_mem_center (Set.ofNat_mem_center _ _)⟩ : Submonoid.center R) •
+    { toFun := polarBilin
+      map_add' := fun _x _y => BilinForm.ext <| polar_add _ _
+      map_smul' :=  fun _c _x => BilinForm.ext <| polar_smul _ _ }
 #align quadratic_form.associated_hom QuadraticForm.associatedHom
 
 variable (Q : QuadraticForm R M)
@@ -792,6 +798,11 @@ theorem associated_apply (x y : M) : associatedHom S Q x y = ⅟ 2 * (Q (x + y)
   rfl
 #align quadratic_form.associated_apply QuadraticForm.associated_apply
 
+@[simp] theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by
+  ext
+  dsimp
+  rw [←smul_mul_assoc, two_nsmul, invOf_two_add_invOf_two, one_mul, polar]
+
 theorem associated_isSymm : (associatedHom S Q).IsSymm := fun x y => by
   simp only [associated_apply, add_comm, add_left_comm, sub_eq_add_neg, add_assoc]
 #align quadratic_form.associated_is_symm QuadraticForm.associated_isSymm
@@ -805,7 +816,7 @@ theorem associated_comp {N : Type v} [AddCommGroup N] [Module R N] (f : N →ₗ
 
 theorem associated_toQuadraticForm (B : BilinForm R M) (x y : M) :
     associatedHom S B.toQuadraticForm x y = ⅟ 2 * (B x y + B y x) := by
-  simp only [associated_apply, ← polar_to_quadratic_form, polar, toQuadraticForm_apply]
+  simp only [associated_apply, ← polar_toQuadraticForm, polar]
 #align quadratic_form.associated_to_quadratic_form QuadraticForm.associated_toQuadraticForm
 
 theorem associated_left_inverse (h : B₁.IsSymm) : associatedHom S B₁.toQuadraticForm = B₁ :=
@@ -859,7 +870,7 @@ end AssociatedHom
 
 section Associated
 
-variable [CommRing R₁] [AddCommGroup M] [Module R₁ M]
+variable [CommSemiring S] [CommRing R₁] [AddCommGroup M] [Algebra S R₁] [Module R₁ M]
 
 variable [Invertible (2 : R₁)]
 
@@ -871,6 +882,11 @@ abbrev associated : QuadraticForm R₁ M →ₗ[R₁] BilinForm R₁ M :=
   associatedHom R₁
 #align quadratic_form.associated QuadraticForm.associated
 
+variable (S) in
+theorem coe_associatedHom :
+    ⇑(associatedHom S : QuadraticForm R₁ M →ₗ[S] BilinForm R₁ M) = associated :=
+  rfl
+
 @[simp]
 theorem associated_linMulLin (f g : M →ₗ[R₁] R₁) :
     associated (R₁ := R₁) (linMulLin f g) =

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -69,6 +69,13 @@ theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂
   dsimp
   convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂))
 
+theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
+    polarBilin (Q₁.tmul Q₂) = ⅟(2 : A) • (polarBilin Q₁).tmul (polarBilin Q₂) := by
+  simp_rw [←two_nsmul_associated A, ←two_nsmul_associated R, BilinForm.tmul, map_smul, tmul_smul,
+    ←smul_tmul', map_nsmul, associated_tmul]
+  rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two,
+    one_smul]
+
 variable (A) in
 /-- The base change of a quadratic form. -/
 protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) :=
@@ -79,12 +86,17 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) :
     Q.baseChange A (a ⊗ₜ m₂) = Q m₂ • (a * a) :=
   tensorDistrib_tmul _ _ _ _
 
-
 theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂)  :
     associated (R₁ := A) (Q.baseChange A) = (associated (R₁ := R) Q).baseChange A := by
   dsimp only [QuadraticForm.baseChange, BilinForm.baseChange]
   rw [associated_tmul (QuadraticForm.sq (R := A)) Q, associated_sq]
 
+theorem polarBilin_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂)  :
+    polarBilin (Q.baseChange A) = (polarBilin Q).baseChange A := by
+  rw [QuadraticForm.baseChange, BilinForm.baseChange, polarBilin_tmul, BilinForm.tmul,
+    ←LinearMap.map_smul, smul_tmul', ←two_nsmul_associated R, coe_associatedHom, associated_sq,
+    smul_comm, ← smul_assoc, two_smul, invOf_two_add_invOf_two, one_smul]
+
 end CommRing
 
 end QuadraticForm