feat(LinearAlgebra/QuadraticForm/Prod): inl, inr, and single ar…

…e isometries (#7723)

Mathlib/LinearAlgebra/QuadraticForm/Prod.lean

@@ -65,6 +65,18 @@ def IsometryEquiv.prod
   toLinearEquiv := LinearEquiv.prod e₁.toLinearEquiv e₂.toLinearEquiv
 #align quadratic_form.isometry.prod QuadraticForm.IsometryEquiv.prod
 
+/-- `LinearMap.inl` as an isometry. -/
+@[simps!]
+def Isometry.inl (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Q₁ →qᵢ (Q₁.prod Q₂) where
+  toLinearMap := LinearMap.inl R _ _
+  map_app' m₁ := by simp
+
+/-- `LinearMap.inr` as an isometry. -/
+@[simps!]
+def Isometry.inr (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Q₂ →qᵢ (Q₁.prod Q₂) where
+  toLinearMap := LinearMap.inr R _ _
+  map_app' m₁ := by simp
+
 theorem Equivalent.prod {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
     {Q₁' : QuadraticForm R N₁} {Q₂' : QuadraticForm R N₂} (e₁ : Q₁.Equivalent Q₁')
     (e₂ : Q₂.Equivalent Q₂') : (Q₁.prod Q₂).Equivalent (Q₁'.prod Q₂') :=
@@ -187,6 +199,12 @@ theorem pi_apply [Fintype ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) (x : ∀ i,
   sum_apply _ _ _
 #align quadratic_form.pi_apply QuadraticForm.pi_apply
 
+theorem pi_apply_single [Fintype ι] [DecidableEq ι]
+    (Q : ∀ i, QuadraticForm R (Mᵢ i)) (i : ι) (m : Mᵢ i) :
+    pi Q (Pi.single i m) = Q i m := by
+  rw [pi_apply, Fintype.sum_eq_single i fun j hj => ?_, Pi.single_eq_same]
+  rw [Pi.single_eq_of_ne hj, map_zero]
+
 /-- An isometry between quadratic forms generated by `QuadraticForm.pi` can be constructed
 from a pair of isometries between the left and right parts. -/
 @[simps toLinearEquiv]
@@ -199,6 +217,13 @@ def IsometryEquiv.pi [Fintype ι]
   toLinearEquiv := LinearEquiv.piCongrRight fun i => (e i : Mᵢ i ≃ₗ[R] Nᵢ i)
 #align quadratic_form.isometry.pi QuadraticForm.IsometryEquiv.pi
 
+/-- `LinearMap.single` as an isometry. -/
+@[simps!]
+def Isometry.single [Fintype ι] [DecidableEq ι] (Q : ∀ i, QuadraticForm R (Mᵢ i)) (i : ι) :
+    Q i →qᵢ pi Q where
+  toLinearMap := LinearMap.single i
+  map_app' := pi_apply_single _ _
+
 theorem Equivalent.pi [Fintype ι] {Q : ∀ i, QuadraticForm R (Mᵢ i)}
     {Q' : ∀ i, QuadraticForm R (Nᵢ i)} (e : ∀ i, (Q i).Equivalent (Q' i)) :
     (pi Q).Equivalent (pi Q') :=