feat: Generalize quadratic isometries to quadratic maps (#14719)

Also `.prod` and `.pi`, since these are heavily entangled with `Isometry` and `IsometryEquiv`.

Follows on from #7569.

Author: eric-wieser

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -333,7 +333,7 @@ theorem map_apply_ι (f : Q₁ →qᵢ Q₂) (m : M₁) : map f (ι Q₁ m) = ι
 
 variable (Q₁) in
 @[simp]
-theorem map_id : map (QuadraticForm.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁) := by
+theorem map_id : map (QuadraticMap.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁) := by
   ext m; exact map_apply_ι _ m
 #align clifford_algebra.map_id CliffordAlgebra.map_id
 
@@ -342,7 +342,7 @@ theorem map_comp_map (f : Q₂ →qᵢ Q₃) (g : Q₁ →qᵢ Q₂) :
     (map f).comp (map g) = map (f.comp g) := by
   ext m
   dsimp only [LinearMap.comp_apply, AlgHom.comp_apply, AlgHom.toLinearMap_apply, AlgHom.id_apply]
-  rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticForm.Isometry.comp_apply]
+  rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticMap.Isometry.comp_apply]
 #align clifford_algebra.map_comp_map CliffordAlgebra.map_comp_map
 
 @[simp]
@@ -358,7 +358,7 @@ is a retraction of `CliffordAlgebra.map f`. -/
 lemma leftInverse_map_of_leftInverse {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
     (f : Q₁ →qᵢ Q₂) (g : Q₂ →qᵢ Q₁) (h : LeftInverse g f) : LeftInverse (map g) (map f) := by
   refine fun x => ?_
-  replace h : g.comp f = QuadraticForm.Isometry.id Q₁ := DFunLike.ext _ _ h
+  replace h : g.comp f = QuadraticMap.Isometry.id Q₁ := DFunLike.ext _ _ h
   rw [← AlgHom.comp_apply, map_comp_map, h, map_id, AlgHom.coe_id, id_eq]
 
 /-- If a linear map preserves the quadratic forms and is surjective, then the algebra
@@ -401,7 +401,7 @@ theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q
 
 @[simp]
 theorem equivOfIsometry_refl :
-    (equivOfIsometry <| QuadraticForm.IsometryEquiv.refl Q₁) = AlgEquiv.refl := by
+    (equivOfIsometry <| QuadraticMap.IsometryEquiv.refl Q₁) = AlgEquiv.refl := by
   ext x
   exact AlgHom.congr_fun (map_id Q₁) x
 #align clifford_algebra.equiv_of_isometry_refl CliffordAlgebra.equivOfIsometry_refl

Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean

@@ -259,8 +259,7 @@ variable {R : Type*} [CommRing R] (c₁ c₂ : R)
 /-- `Q c₁ c₂` is a quadratic form over `R × R` such that `CliffordAlgebra (Q c₁ c₂)` is isomorphic
 as an `R`-algebra to `ℍ[R,c₁,c₂]`. -/
 def Q : QuadraticForm R (R × R) :=
-   -- Porting note: Added `(R := R)`
-  QuadraticForm.prod (c₁ • QuadraticMap.sq (R := R)) (c₂ • QuadraticMap.sq)
+  (c₁ • QuadraticMap.sq).prod (c₂ • QuadraticMap.sq)
 set_option linter.uppercaseLean3 false in
 #align clifford_algebra_quaternion.Q CliffordAlgebraQuaternion.Q
 

Mathlib/LinearAlgebra/CliffordAlgebra/Prod.lean

@@ -115,7 +115,7 @@ def ofProd : CliffordAlgebra (Q₁.prod Q₂) →ₐ[R] (evenOdd Q₁ ᵍ⊗[R]
           ∘ₗ (evenOdd Q₂ 1).subtype ∘ₗ (ι Q₂).codRestrict _ (ι_mem_evenOdd_one Q₂)),
     fun m => by
       simp_rw [LinearMap.coprod_apply, LinearMap.coe_comp, Function.comp_apply,
-        AlgHom.toLinearMap_apply, QuadraticForm.prod_apply, Submodule.coeSubtype,
+        AlgHom.toLinearMap_apply, QuadraticMap.prod_apply, Submodule.coeSubtype,
         GradedTensorProduct.includeLeft_apply, GradedTensorProduct.includeRight_apply, map_add,
         add_mul, mul_add, GradedTensorProduct.algebraMap_def,
         GradedTensorProduct.tmul_one_mul_one_tmul, GradedTensorProduct.tmul_one_mul_coe_tmul,
@@ -135,18 +135,18 @@ def toProd : evenOdd Q₁ ᵍ⊗[R] evenOdd Q₂ →ₐ[R] CliffordAlgebra (Q₁
   GradedTensorProduct.lift _ _
     (CliffordAlgebra.map <| .inl _ _)
     (CliffordAlgebra.map <| .inr _ _)
-    fun _i₁ _i₂ x₁ x₂ => map_mul_map_of_isOrtho_of_mem_evenOdd _ _ (QuadraticForm.IsOrtho.inl_inr) _
+    fun _i₁ _i₂ x₁ x₂ => map_mul_map_of_isOrtho_of_mem_evenOdd _ _ (QuadraticMap.IsOrtho.inl_inr) _
       _ x₁.prop x₂.prop
 
 @[simp]
 lemma toProd_ι_tmul_one (m₁ : M₁) : toProd Q₁ Q₂ (ι _ m₁ ᵍ⊗ₜ 1) = ι _ (m₁, 0) := by
   rw [toProd, GradedTensorProduct.lift_tmul, map_one, mul_one, map_apply_ι,
-    QuadraticForm.Isometry.inl_apply]
+    QuadraticMap.Isometry.inl_apply]
 
 @[simp]
 lemma toProd_one_tmul_ι (m₂ : M₂) : toProd Q₁ Q₂ (1 ᵍ⊗ₜ ι _ m₂) = ι _ (0, m₂) := by
   rw [toProd, GradedTensorProduct.lift_tmul, map_one, one_mul, map_apply_ι,
-    QuadraticForm.Isometry.inr_apply]
+    QuadraticMap.Isometry.inr_apply]
 
 lemma toProd_comp_ofProd : (toProd Q₁ Q₂).comp (ofProd Q₁ Q₂) = AlgHom.id _ _ := by
   ext m <;> dsimp

Mathlib/LinearAlgebra/QuadraticForm/Complex.lean

@@ -34,7 +34,7 @@ noncomputable def isometryEquivSumSquares (w' : ι → ℂ) :
   have hw' : ∀ i : ι, (w i : ℂ) ^ (-(1 / 2 : ℂ)) ≠ 0 := by
     intro i hi
     exact (w i).ne_zero ((Complex.cpow_eq_zero_iff _ _).1 hi).1
-  convert QuadraticForm.isometryEquivBasisRepr (weightedSumSquares ℂ w')
+  convert QuadraticMap.isometryEquivBasisRepr (weightedSumSquares ℂ w')
     ((Pi.basisFun ℂ ι).unitsSMul fun i => (isUnit_iff_ne_zero.2 <| hw' i).unit)
   ext1 v
   erw [basisRepr_apply, weightedSumSquares_apply, weightedSumSquares_apply]

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

@@ -154,7 +154,7 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] :
       sub_eq_add_neg (Q x.1) (Q x.2)]
 #align quadratic_form.to_dual_prod QuadraticForm.toDualProdₓ
 
-#align quadratic_form.to_dual_prod_isometry QuadraticForm.Isometry.map_appₓ
+#align quadratic_form.to_dual_prod_isometry QuadraticMap.Isometry.map_appₓ
 
 /-!
 TODO: show that `QuadraticForm.toDualProd` is an `QuadraticForm.IsometryEquiv`

Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

@@ -10,25 +10,26 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic
 
 ## Main definitions
 
-* `QuadraticForm.Isometry`: `LinearMap`s which map between two different quadratic forms
+* `QuadraticMap.Isometry`: `LinearMap`s which map between two different quadratic forms
 
 ## Notation
 
 `Q₁ →qᵢ Q₂` is notation for `Q₁.Isometry Q₂`.
 -/
 
-variable {ι R M M₁ M₂ M₃ M₄ : Type*}
+variable {ι R M M₁ M₂ M₃ M₄ N : Type*}
 
-namespace QuadraticForm
+namespace QuadraticMap
 
 variable [CommSemiring R]
 variable [AddCommMonoid M]
 variable [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid M₄]
-variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄]
+variable [AddCommMonoid N]
+variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M₄] [Module R N]
 
 /-- An isometry between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
 is a linear map between `M₁` and `M₂` that commutes with the quadratic forms. -/
-structure Isometry (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) extends M₁ →ₗ[R] M₂ where
+structure Isometry (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) extends M₁ →ₗ[R] M₂ where
   /-- The quadratic form agrees across the map. -/
   map_app' : ∀ m, Q₂ (toFun m) = Q₁ m
 
@@ -37,8 +38,8 @@ namespace Isometry
 @[inherit_doc]
 notation:25 Q₁ " →qᵢ " Q₂:0 => Isometry Q₁ Q₂
 
-variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂}
-variable {Q₃ : QuadraticForm R M₃} {Q₄ : QuadraticForm R M₄}
+variable {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N}
+variable {Q₃ : QuadraticMap R M₃ N} {Q₄ : QuadraticMap R M₄ N}
 
 instance instFunLike : FunLike (Q₁ →qᵢ Q₂) M₁ M₂ where
   coe f := f.toLinearMap
@@ -71,18 +72,18 @@ theorem coe_toLinearMap (f : Q₁ →qᵢ Q₂) : ⇑f.toLinearMap = f :=
 
 /-- The identity isometry from a quadratic form to itself. -/
 @[simps!]
-def id (Q : QuadraticForm R M) : Q →qᵢ Q where
+def id (Q : QuadraticMap R M N) : Q →qᵢ Q where
   __ := LinearMap.id
   map_app' _ := rfl
 
 /-- The identity isometry between equal quadratic forms. -/
 @[simps!]
-def ofEq {Q₁ Q₂ : QuadraticForm R M₁} (h : Q₁ = Q₂) : Q₁ →qᵢ Q₂ where
+def ofEq {Q₁ Q₂ : QuadraticMap R M₁ N} (h : Q₁ = Q₂) : Q₁ →qᵢ Q₂ where
   __ := LinearMap.id
   map_app' _ := h ▸ rfl
 
 @[simp]
-theorem ofEq_rfl {Q : QuadraticForm R M₁} : ofEq (rfl : Q = Q) = .id Q := rfl
+theorem ofEq_rfl {Q : QuadraticMap R M₁ N} : ofEq (rfl : Q = Q) = .id Q := rfl
 
 /-- The composition of two isometries between quadratic forms. -/
 @[simps]
@@ -109,7 +110,7 @@ theorem comp_assoc (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →
   ext fun _ => rfl
 
 /-- There is a zero map from any module with the zero form. -/
-instance : Zero ((0 : QuadraticForm R M₁) →qᵢ Q₂) where
+instance : Zero ((0 : QuadraticMap R M₁ N) →qᵢ Q₂) where
   zero := { (0 : M₁ →ₗ[R] M₂) with map_app' := fun _ => map_zero _ }
 
 /-- There is a zero map from the trivial module. -/
@@ -124,4 +125,4 @@ instance [Subsingleton M₂] : Subsingleton (Q₁ →qᵢ Q₂) :=
 
 end Isometry
 
-end QuadraticForm
+end QuadraticMap

Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

@@ -23,34 +23,34 @@ import Mathlib.LinearAlgebra.QuadraticForm.Isometry
 -/
 
 
-variable {ι R K M M₁ M₂ M₃ V : Type*}
+variable {ι R K M M₁ M₂ M₃ V N : Type*}
 
 open QuadraticMap
 
-namespace QuadraticForm
+namespace QuadraticMap
 
 variable [CommSemiring R]
-variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]
-variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃]
+variable [AddCommMonoid M] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid N]
+variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃] [Module R N]
 
 /-- An isometric equivalence between two quadratic spaces `M₁, Q₁` and `M₂, Q₂` over a ring `R`,
 is a linear equivalence between `M₁` and `M₂` that commutes with the quadratic forms. -/
 -- Porting note(#5171): linter not ported yet @[nolint has_nonempty_instance]
-structure IsometryEquiv (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂)
+structure IsometryEquiv (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N)
     extends M₁ ≃ₗ[R] M₂ where
   map_app' : ∀ m, Q₂ (toFun m) = Q₁ m
-#align quadratic_form.isometry QuadraticForm.IsometryEquiv
+#align quadratic_form.isometry QuadraticMap.IsometryEquiv
 
 /-- Two quadratic forms over a ring `R` are equivalent
 if there exists an isometric equivalence between them:
 a linear equivalence that transforms one quadratic form into the other. -/
-def Equivalent (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) : Prop :=
+def Equivalent (Q₁ : QuadraticMap R M₁ N) (Q₂ : QuadraticMap R M₂ N) : Prop :=
   Nonempty (Q₁.IsometryEquiv Q₂)
-#align quadratic_form.equivalent QuadraticForm.Equivalent
+#align quadratic_form.equivalent QuadraticMap.Equivalent
 
 namespace IsometryEquiv
 
-variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
+variable {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N}
 
 instance : EquivLike (Q₁.IsometryEquiv Q₂) M₁ M₂ where
   coe f := f.toLinearEquiv
@@ -73,32 +73,32 @@ instance : CoeOut (Q₁.IsometryEquiv Q₂) (M₁ ≃ₗ[R] M₂) :=
 @[simp]
 theorem coe_toLinearEquiv (f : Q₁.IsometryEquiv Q₂) : ⇑(f : M₁ ≃ₗ[R] M₂) = f :=
   rfl
-#align quadratic_form.isometry.coe_to_linear_equiv QuadraticForm.IsometryEquiv.coe_toLinearEquiv
+#align quadratic_form.isometry.coe_to_linear_equiv QuadraticMap.IsometryEquiv.coe_toLinearEquiv
 
 @[simp]
 theorem map_app (f : Q₁.IsometryEquiv Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
   f.map_app' m
-#align quadratic_form.isometry.map_app QuadraticForm.IsometryEquiv.map_app
+#align quadratic_form.isometry.map_app QuadraticMap.IsometryEquiv.map_app
 
 /-- The identity isometric equivalence between a quadratic form and itself. -/
 @[refl]
-def refl (Q : QuadraticForm R M) : Q.IsometryEquiv Q :=
+def refl (Q : QuadraticMap R M N) : Q.IsometryEquiv Q :=
   { LinearEquiv.refl R M with map_app' := fun _ => rfl }
-#align quadratic_form.isometry.refl QuadraticForm.IsometryEquiv.refl
+#align quadratic_form.isometry.refl QuadraticMap.IsometryEquiv.refl
 
 /-- The inverse isometric equivalence of an isometric equivalence between two quadratic forms. -/
 @[symm]
 def symm (f : Q₁.IsometryEquiv Q₂) : Q₂.IsometryEquiv Q₁ :=
   { (f : M₁ ≃ₗ[R] M₂).symm with
     map_app' := by intro m; rw [← f.map_app]; congr; exact f.toLinearEquiv.apply_symm_apply m }
-#align quadratic_form.isometry.symm QuadraticForm.IsometryEquiv.symm
+#align quadratic_form.isometry.symm QuadraticMap.IsometryEquiv.symm
 
 /-- The composition of two isometric equivalences between quadratic forms. -/
 @[trans]
 def trans (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) : Q₁.IsometryEquiv Q₃ :=
   { (f : M₁ ≃ₗ[R] M₂).trans (g : M₂ ≃ₗ[R] M₃) with
     map_app' := by intro m; rw [← f.map_app, ← g.map_app]; rfl }
-#align quadratic_form.isometry.trans QuadraticForm.IsometryEquiv.trans
+#align quadratic_form.isometry.trans QuadraticMap.IsometryEquiv.trans
 
 /-- Isometric equivalences are isometric maps -/
 @[simps]
@@ -110,43 +110,46 @@ end IsometryEquiv
 
 namespace Equivalent
 
-variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
+variable {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N}
 
 @[refl]
-theorem refl (Q : QuadraticForm R M) : Q.Equivalent Q :=
+theorem refl (Q : QuadraticMap R M N) : Q.Equivalent Q :=
   ⟨IsometryEquiv.refl Q⟩
-#align quadratic_form.equivalent.refl QuadraticForm.Equivalent.refl
+#align quadratic_form.equivalent.refl QuadraticMap.Equivalent.refl
 
 @[symm]
 theorem symm (h : Q₁.Equivalent Q₂) : Q₂.Equivalent Q₁ :=
   h.elim fun f => ⟨f.symm⟩
-#align quadratic_form.equivalent.symm QuadraticForm.Equivalent.symm
+#align quadratic_form.equivalent.symm QuadraticMap.Equivalent.symm
 
 @[trans]
 theorem trans (h : Q₁.Equivalent Q₂) (h' : Q₂.Equivalent Q₃) : Q₁.Equivalent Q₃ :=
   h'.elim <| h.elim fun f g => ⟨f.trans g⟩
-#align quadratic_form.equivalent.trans QuadraticForm.Equivalent.trans
+#align quadratic_form.equivalent.trans QuadraticMap.Equivalent.trans
 
 end Equivalent
 
 /-- A quadratic form composed with a `LinearEquiv` is isometric to itself. -/
-def isometryEquivOfCompLinearEquiv (Q : QuadraticForm R M) (f : M₁ ≃ₗ[R] M) :
+def isometryEquivOfCompLinearEquiv (Q : QuadraticMap R M N) (f : M₁ ≃ₗ[R] M) :
     Q.IsometryEquiv (Q.comp (f : M₁ →ₗ[R] M)) :=
   { f.symm with
     map_app' := by
       intro
       simp only [comp_apply, LinearEquiv.coe_coe, LinearEquiv.toFun_eq_coe,
         LinearEquiv.apply_symm_apply, f.apply_symm_apply] }
-#align quadratic_form.isometry_of_comp_linear_equiv QuadraticForm.isometryEquivOfCompLinearEquiv
+#align quadratic_form.isometry_of_comp_linear_equiv QuadraticMap.isometryEquivOfCompLinearEquiv
 
 variable [Finite ι]
 
 /-- A quadratic form is isometrically equivalent to its bases representations. -/
-noncomputable def isometryEquivBasisRepr (Q : QuadraticForm R M) (v : Basis ι R M) :
+noncomputable def isometryEquivBasisRepr (Q : QuadraticMap R M N) (v : Basis ι R M) :
     IsometryEquiv Q (Q.basisRepr v) :=
   isometryEquivOfCompLinearEquiv Q v.equivFun.symm
-#align quadratic_form.isometry_basis_repr QuadraticForm.isometryEquivBasisRepr
+#align quadratic_form.isometry_basis_repr QuadraticMap.isometryEquivBasisRepr
+
+end QuadraticMap
 
+namespace QuadraticForm
 variable [Field K] [Invertible (2 : K)] [AddCommGroup V] [Module K V]
 
 /-- Given an orthogonal basis, a quadratic form is isometrically equivalent with a weighted sum of