feat(LinearAlgebra/QuadraticForm): add QuadraticForm.Isometry (#6984)

Also use it to tidy the API of `CliffordAlgebra.map`.

Mathlib.lean

@@ -2310,6 +2310,7 @@ import Mathlib.LinearAlgebra.ProjectiveSpace.Subspace
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
 import Mathlib.LinearAlgebra.QuadraticForm.Complex
 import Mathlib.LinearAlgebra.QuadraticForm.Dual
+import Mathlib.LinearAlgebra.QuadraticForm.Isometry
 import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 import Mathlib.LinearAlgebra.QuadraticForm.Prod
 import Mathlib.LinearAlgebra.QuadraticForm.Real

Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean

@@ -5,6 +5,7 @@ Authors: Eric Wieser, Utensil Song
 -/
 import Mathlib.Algebra.RingQuot
 import Mathlib.LinearAlgebra.TensorAlgebra.Basic
+import Mathlib.LinearAlgebra.QuadraticForm.Isometry
 import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
 
 #align_import linear_algebra.clifford_algebra.basic from "leanprover-community/mathlib"@"d46774d43797f5d1f507a63a6e904f7a533ae74a"
@@ -267,61 +268,58 @@ variable [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃]
 
 variable [Module R M₁] [Module R M₂] [Module R M₃]
 
-variable (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (Q₃ : QuadraticForm R M₃)
+variable {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Q₃ : QuadraticForm R M₃}
 
 /-- Any linear map that preserves the quadratic form lifts to an `AlgHom` between algebras.
 
-See `CliffordAlgebra.equivOfIsometry` for the case when `f` is a `QuadraticForm.Isometry`. -/
-def map (f : M₁ →ₗ[R] M₂) (hf : ∀ m, Q₂ (f m) = Q₁ m) :
+See `CliffordAlgebra.equivOfIsometry` for the case when `f` is a `QuadraticForm.IsometryEquiv`. -/
+def map (f : Q₁ →qᵢ Q₂) :
     CliffordAlgebra Q₁ →ₐ[R] CliffordAlgebra Q₂ :=
   CliffordAlgebra.lift Q₁
-    ⟨(CliffordAlgebra.ι Q₂).comp f, fun m => (ι_sq_scalar _ _).trans <| RingHom.congr_arg _ <| hf m⟩
+    ⟨ι Q₂ ∘ₗ f.toLinearMap, fun m => (ι_sq_scalar _ _).trans <| RingHom.congr_arg _ <| f.map_app m⟩
 #align clifford_algebra.map CliffordAlgebra.map
 
 @[simp]
-theorem map_comp_ι (f : M₁ →ₗ[R] M₂) (hf) :
-    (map Q₁ Q₂ f hf).toLinearMap.comp (ι Q₁) = (ι Q₂).comp f :=
+theorem map_comp_ι (f : Q₁ →qᵢ Q₂) :
+    (map f).toLinearMap ∘ₗ ι Q₁ = ι Q₂ ∘ₗ f.toLinearMap :=
   ι_comp_lift _ _
 #align clifford_algebra.map_comp_ι CliffordAlgebra.map_comp_ι
 
 @[simp]
-theorem map_apply_ι (f : M₁ →ₗ[R] M₂) (hf) (m : M₁) : map Q₁ Q₂ f hf (ι Q₁ m) = ι Q₂ (f m) :=
+theorem map_apply_ι (f : Q₁ →qᵢ Q₂) (m : M₁) : map f (ι Q₁ m) = ι Q₂ (f m) :=
   lift_ι_apply _ _ m
 #align clifford_algebra.map_apply_ι CliffordAlgebra.map_apply_ι
 
+variable (Q₁) in
 @[simp]
-theorem map_id :
-    (map Q₁ Q₁ (LinearMap.id : M₁ →ₗ[R] M₁) fun m => rfl) = AlgHom.id R (CliffordAlgebra Q₁) := by
-  ext m; exact map_apply_ι _ _ _ _ m
+theorem map_id : map (QuadraticForm.Isometry.id Q₁) = AlgHom.id R (CliffordAlgebra Q₁) := by
+  ext m; exact map_apply_ι _ m
 #align clifford_algebra.map_id CliffordAlgebra.map_id
 
 @[simp]
-theorem map_comp_map (f : M₂ →ₗ[R] M₃) (hf) (g : M₁ →ₗ[R] M₂) (hg) :
-    (map Q₂ Q₃ f hf).comp (map Q₁ Q₂ g hg)
-      = map Q₁ Q₃ (f.comp g) fun m => (hf _).trans <| hg m := by
+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_ι, LinearMap.comp_apply]
+  rw [map_apply_ι, map_apply_ι, map_apply_ι, QuadraticForm.Isometry.comp_apply]
 #align clifford_algebra.map_comp_map CliffordAlgebra.map_comp_map
 
 @[simp]
-theorem ι_range_map_map (f : M₁ →ₗ[R] M₂) (hf : ∀ m, Q₂ (f m) = Q₁ m) :
-    (ι Q₁).range.map (map Q₁ Q₂ f hf).toLinearMap = f.range.map (ι Q₂) :=
+theorem ι_range_map_map (f : Q₁ →qᵢ Q₂) :
+    (ι Q₁).range.map (map f).toLinearMap = f.range.map (ι Q₂) :=
   (ι_range_map_lift _ _).trans (LinearMap.range_comp _ _)
 #align clifford_algebra.ι_range_map_map CliffordAlgebra.ι_range_map_map
 
-variable {Q₁ Q₂ Q₃}
-
 /-- Two `CliffordAlgebra`s are equivalent as algebras if their quadratic forms are
 equivalent. -/
 @[simps! apply]
 def equivOfIsometry (e : Q₁.IsometryEquiv Q₂) : CliffordAlgebra Q₁ ≃ₐ[R] CliffordAlgebra Q₂ :=
-  AlgEquiv.ofAlgHom (map Q₁ Q₂ e e.map_app) (map Q₂ Q₁ e.symm e.symm.map_app)
-    ((map_comp_map _ _ _ _ _ _ _).trans <| by
+  AlgEquiv.ofAlgHom (map e.toIsometry) (map e.symm.toIsometry)
+    ((map_comp_map _ _).trans <| by
       convert map_id Q₂ using 2  -- porting note: replaced `_` with `Q₂`
       ext m
       exact e.toLinearEquiv.apply_symm_apply m)
-    ((map_comp_map _ _ _ _ _ _ _).trans <| by
+    ((map_comp_map _ _).trans <| by
       convert map_id Q₁ using 2  -- porting note: replaced `_` with `Q₁`
       ext m
       exact e.toLinearEquiv.symm_apply_apply m)
@@ -337,7 +335,7 @@ theorem equivOfIsometry_symm (e : Q₁.IsometryEquiv Q₂) :
 theorem equivOfIsometry_trans (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) :
     (equivOfIsometry e₁₂).trans (equivOfIsometry e₂₃) = equivOfIsometry (e₁₂.trans e₂₃) := by
   ext x
-  exact AlgHom.congr_fun (map_comp_map Q₁ Q₂ Q₃ _ _ _ _) x
+  exact AlgHom.congr_fun (map_comp_map _ _) x
 #align clifford_algebra.equiv_of_isometry_trans CliffordAlgebra.equivOfIsometry_trans
 
 @[simp]

Mathlib/LinearAlgebra/QuadraticForm/Dual.lean

@@ -17,9 +17,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Prod
   `f x`.
 * `QuadraticForm.dualProd R M`, the quadratic form on `(f, x) : Module.Dual R M × M` defined as
   `f x`.
-* `QuadraticForm.toDualProd : M × M →ₗ[R] Module.Dual R M × M` a form-preserving map from
-  `(Q.prod $ -Q)` to `QuadraticForm.dualProd R M`. Note that we do not have the morphism
-  version of `QuadraticForm.IsometryEquiv`, so for now this is stated without full bundling.
+* `QuadraticForm.toDualProd : (Q.prod <| -Q) →qᵢ QuadraticForm.dualProd R M` a form-preserving map
+  from `(Q.prod <| -Q)` to `QuadraticForm.dualProd R M`.
 
 -/
 
@@ -142,22 +141,25 @@ This is `σ` from Proposition 4.8, page 84 of
 [*Hermitian K-Theory and Geometric Applications*][hyman1973]; though we swap the order of the pairs.
 -/
 @[simps!]
-def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : M × M →ₗ[R] Module.Dual R M × M :=
-  LinearMap.prod
+def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] :
+  (Q.prod <| -Q) →qᵢ QuadraticForm.dualProd R M where
+  toLinearMap := LinearMap.prod
     (Q.associated.toLin.comp (LinearMap.fst _ _ _) + Q.associated.toLin.comp (LinearMap.snd _ _ _))
     (LinearMap.fst _ _ _ - LinearMap.snd _ _ _)
-#align quadratic_form.to_dual_prod QuadraticForm.toDualProd
-
-theorem toDualProd_isometry [Invertible (2 : R)] (Q : QuadraticForm R M) (x : M × M) :
-    QuadraticForm.dualProd R M (toDualProd Q x) = (Q.prod <| -Q) x := by
-  dsimp only [toDualProd, associated, associatedHom]
-  dsimp
-  -- porting note: added `()` around `Submonoid.smul_def`
-  simp [polar_comm _ x.1 x.2, ← sub_add, mul_sub, sub_mul, smul_sub, (Submonoid.smul_def), ←
-    sub_eq_add_neg (Q x.1) (Q x.2)]
-#align quadratic_form.to_dual_prod_isometry QuadraticForm.toDualProd_isometry
-
--- TODO: show that `toDualProd` is an equivalence
+  map_app' x := by
+    dsimp only [associated, associatedHom]
+    dsimp
+    -- porting note: added `()` around `Submonoid.smul_def`
+    simp [polar_comm _ x.1 x.2, ← sub_add, mul_sub, sub_mul, smul_sub, (Submonoid.smul_def), ←
+      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ₓ
+
+/-!
+TODO: show that `QuadraticForm.toDualProd` is an `QuadraticForm.IsometryEquiv`
+-/
+
 end Ring
 
 end QuadraticForm

Mathlib/LinearAlgebra/QuadraticForm/Isometry.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.LinearAlgebra.QuadraticForm.Basic
+
+/-!
+# Isometric linear maps
+
+## Main definitions
+
+* `QuadraticForm.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*}
+
+namespace QuadraticForm
+
+variable [Semiring 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₄]
+
+/-- 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
+  /-- The quadratic form agrees across the map. -/
+  map_app' : ∀ m, Q₂ (toFun m) = Q₁ m
+
+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₄}
+
+instance instLinearMapClass : LinearMapClass (Q₁ →qᵢ Q₂) R M₁ M₂ where
+  coe f := f.toLinearMap
+  coe_injective' f g h := by cases f; cases g; congr; exact FunLike.coe_injective h
+  map_add f := f.toLinearMap.map_add
+  map_smulₛₗ f := f.toLinearMap.map_smul
+
+theorem toLinearMap_injective :
+    Function.Injective (Isometry.toLinearMap : (Q₁ →qᵢ Q₂) → M₁ →ₗ[R] M₂) := fun _f _g h =>
+  FunLike.coe_injective (congr_arg FunLike.coe h : _)
+
+@[ext]
+theorem ext ⦃f g : Q₁ →qᵢ Q₂⦄ (h : ∀ x, f x = g x) : f = g :=
+  FunLike.ext _ _ h
+
+/-- See Note [custom simps projection]. -/
+protected def Simps.apply (f : Q₁ →qᵢ Q₂) : M₁ → M₂ := f
+
+initialize_simps_projections Isometry (toFun → apply)
+
+@[simp]
+theorem map_app (f : Q₁ →qᵢ Q₂) (m : M₁) : Q₂ (f m) = Q₁ m :=
+  f.map_app' m
+
+@[simp]
+theorem coe_toLinearMap (f : Q₁ →qᵢ Q₂) : ⇑f.toLinearMap = f :=
+  rfl
+
+/-- The identity isometry from a quadratic form to itself. -/
+@[simps!]
+def id (Q : QuadraticForm R M) : Q →qᵢ Q where
+  __ := LinearMap.id
+  map_app' _ := rfl
+
+/-- The composition of two isometries between quadratic forms. -/
+@[simps]
+def comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) : Q₁ →qᵢ Q₃ where
+  toFun x := g (f x)
+  map_app' x := by rw [← f.map_app, ← g.map_app]
+  __ := (g.toLinearMap : M₂ →ₗ[R] M₃) ∘ₗ (f.toLinearMap : M₁ →ₗ[R] M₂)
+
+@[simp]
+theorem toLinearMap_comp (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
+    (g.comp f).toLinearMap = g.toLinearMap.comp f.toLinearMap :=
+  rfl
+
+@[simp]
+theorem id_comp (f : Q₁ →qᵢ Q₂) : (id Q₂).comp f = f :=
+  ext fun _ => rfl
+
+@[simp]
+theorem comp_id (f : Q₁ →qᵢ Q₂) : f.comp (id Q₁) = f :=
+  ext fun _ => rfl
+
+theorem comp_assoc (h : Q₃ →qᵢ Q₄) (g : Q₂ →qᵢ Q₃) (f : Q₁ →qᵢ Q₂) :
+    (h.comp g).comp f = h.comp (g.comp f) :=
+  ext fun _ => rfl
+
+/-- There is a zero map from any module with the zero form. -/
+instance : Zero ((0 : QuadraticForm R M₁) →qᵢ Q₂) where
+  zero := { (0 : M₁ →ₗ[R] M₂) with map_app' := fun _ => map_zero _ }
+
+/-- There is a zero map from the trivial module. -/
+instance hasZeroOfSubsingleton [Subsingleton M₁] : Zero (Q₁ →qᵢ Q₂) where
+  zero :=
+  { (0 : M₁ →ₗ[R] M₂) with
+    map_app' := fun m => Subsingleton.elim 0 m ▸ (map_zero _).trans (map_zero _).symm }
+
+/-- Maps into the zero module are trivial -/
+instance [Subsingleton M₂] : Subsingleton (Q₁ →qᵢ Q₂) :=
+  ⟨fun _ _ => ext fun _ => Subsingleton.elim _ _⟩
+
+end Isometry
+
+end QuadraticForm

Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kexing Ying, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.QuadraticForm.Basic
+import Mathlib.LinearAlgebra.QuadraticForm.Isometry
 
 #align_import linear_algebra.quadratic_form.isometry from "leanprover-community/mathlib"@"14b69e9f3c16630440a2cbd46f1ddad0d561dee7"
 
@@ -97,6 +98,12 @@ def trans (f : Q₁.IsometryEquiv Q₂) (g : Q₂.IsometryEquiv Q₃) : Q₁.Iso
     map_app' := by intro m; rw [← f.map_app, ← g.map_app]; rfl }
 #align quadratic_form.isometry.trans QuadraticForm.IsometryEquiv.trans
 
+/-- Isometric equivalences are isometric maps -/
+@[simps]
+def toIsometry (g : Q₁.IsometryEquiv Q₂) : Q₁ →qᵢ Q₂ where
+  toFun x := g x
+  __ := g
+
 end IsometryEquiv
 
 namespace Equivalent