From 7bcd49c6efc8801b1b474c5a8ca5d93643b900c8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 7 Aug 2023 21:59:54 +0000 Subject: [PATCH 01/30] wip --- .../QuadraticForm/TensorProduct.lean | 130 ++++++++++++++++++ 1 file changed, 130 insertions(+) create mode 100644 Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean new file mode 100644 index 00000000000000..5597c5847d9643 --- /dev/null +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -0,0 +1,130 @@ +/- +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.BilinearForm.TensorProduct +import Mathlib.LinearAlgebra.QuadraticForm.Basic + +/-! +# The quadratic form on a tensor product + +## Main definitions + +* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying + `B₁` on `M₁` and `B₂` on `M₂`. +* `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free + modules. + +-/ + + +universe u v w uι uR uA uM₁ uM₂ + +variable {ι : Type _} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} + +open TensorProduct + +namespace QuadraticForm + +section CommSemiring +variable [CommSemiring R] [CommSemiring A] +variable [AddCommMonoid M₁] [AddCommMonoid M₂] +variable [Algebra R A] [Module R M₁] [Module A M₁] +variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] +variable [Module R M₂] [Invertible (2 : R)] + +instance : SMulCommClass R A (QuadraticForm A M₁) := QuadraticForm.smulComm + +instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := + TensorProduct.leftModule +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. + +Note this is heterobasic; the bilinear form on the left can take values in a larger ring than +the one on the right. -/ +def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := +_ ∘ₗ BilinForm.tensorDistrib ∘ₗ AlgebraTensorModule.map _ _ + + +#exit +-- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for +-- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. +@[simp] +theorem tensorDistrib_tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₂ m₂ m₂' • B₁ m₁ m₁' := + rfl +#align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ + +/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +@[reducible] +protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := + tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) +#align bilin_form.tmul QuadraticForm.tmul + +/-- The base change of a bilinear form. -/ +protected def baseChange (B : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B + +@[simp] +theorem baseChange_tmul (B₂ : QuadraticForm R M₂) (a : A) (m₂ : M₂) + (a' : A) (m₂' : M₂) : + B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := + rfl + +end CommSemiring + +section CommRing + +variable [CommRing R] + +variable [AddCommGroup M₁] [AddCommGroup M₂] + +variable [Module R M₁] [Module R M₂] + +variable [Module.Free R M₁] [Module.Finite R M₁] + +variable [Module.Free R M₂] [Module.Finite R M₂] + +variable [Nontrivial R] + +/-- `tensorDistrib` as an equivalence. -/ +noncomputable def tensorDistribEquiv : + QuadraticForm R M₁ ⊗[R] QuadraticForm R M₂ ≃ₗ[R] QuadraticForm R (M₁ ⊗[R] M₂) := + -- the same `LinearEquiv`s as from `tensorDistrib`, + -- but with the inner linear map also as an equiv + TensorProduct.congr (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) + (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) ≪≫ₗ + TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ + (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ + (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin +#align bilin_form.tensor_distrib_equiv QuadraticForm.tensorDistribEquiv + + +@[simp] +theorem tensorDistribEquiv_tmul (B₁ : QuadraticForm R M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₁ m₁ m₁' * B₂ m₂ m₂' := + rfl + +variable (R M₁ M₂) in +-- TODO: make this `rfl` +@[simp] +theorem tensorDistribEquiv_toLinearMap : + (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by + ext B₁ B₂ : 3 + apply toLin.injective + ext + exact mul_comm _ _ + +@[simp] +theorem tensorDistribEquiv_apply (B : QuadraticForm R M₁ ⊗ QuadraticForm R M₂) : + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := + FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B +#align bilin_form.tensor_distrib_equiv_apply QuadraticForm.tensorDistribEquiv_apply + +end CommRing + +end QuadraticForm From b14cba2496274e37aa83df70d21b650219863eb4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 15:13:47 +0000 Subject: [PATCH 02/30] wip --- .../QuadraticForm/TensorProduct.lean | 97 +++++-------------- 1 file changed, 24 insertions(+), 73 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 5597c5847d9643..d0fc69bab291c3 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -11,8 +11,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic ## Main definitions -* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by applying - `B₁` on `M₁` and `B₂` on `M₂`. +* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying + `B₁` on `M₁` and `B₂` on `M₂`. This construction is not available in characteristic two. * `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free modules. @@ -27,33 +27,37 @@ open TensorProduct namespace QuadraticForm -section CommSemiring -variable [CommSemiring R] [CommSemiring A] -variable [AddCommMonoid M₁] [AddCommMonoid M₂] +section CommRing +variable [CommRing R] [CommRing A] +variable [AddCommGroup M₁] [AddCommGroup M₂] variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] [Invertible (2 : R)] -instance : SMulCommClass R A (QuadraticForm A M₁) := QuadraticForm.smulComm - instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := TensorProduct.leftModule -/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -Note this is heterobasic; the bilinear form on the left can take values in a larger ring than + +variable (R A) in +/-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. + +Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right. -/ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := -_ ∘ₗ BilinForm.tensorDistrib ∘ₗ AlgebraTensorModule.map _ _ + BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) + ∘ₗ BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + ∘ₗ AlgebraTensorModule.map + (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticForm.associatedHom R : QuadraticForm R M₁ →ₗ[R] BilinForm R M₁) -#exit --- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for --- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. +-- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for +-- `R = A` of `Q₁ m₁ * Q₂ m₂`. @[simp] -theorem tensorDistrib_tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₂ m₂ m₂' • B₁ m₁ m₁' := + tensorDistrib (A := A) (Q₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = Q₂ m₂ • Q₁ m₁ := rfl #align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ @@ -64,67 +68,14 @@ protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : #align bilin_form.tmul QuadraticForm.tmul /-- The base change of a bilinear form. -/ -protected def baseChange (B : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := - QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B +protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q @[simp] -theorem baseChange_tmul (B₂ : QuadraticForm R M₂) (a : A) (m₂ : M₂) - (a' : A) (m₂' : M₂) : - B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := +theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : + Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := rfl end CommSemiring -section CommRing - -variable [CommRing R] - -variable [AddCommGroup M₁] [AddCommGroup M₂] - -variable [Module R M₁] [Module R M₂] - -variable [Module.Free R M₁] [Module.Finite R M₁] - -variable [Module.Free R M₂] [Module.Finite R M₂] - -variable [Nontrivial R] - -/-- `tensorDistrib` as an equivalence. -/ -noncomputable def tensorDistribEquiv : - QuadraticForm R M₁ ⊗[R] QuadraticForm R M₂ ≃ₗ[R] QuadraticForm R (M₁ ⊗[R] M₂) := - -- the same `LinearEquiv`s as from `tensorDistrib`, - -- but with the inner linear map also as an equiv - TensorProduct.congr (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) - (QuadraticForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) ≪≫ₗ - TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ - (TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ - (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin -#align bilin_form.tensor_distrib_equiv QuadraticForm.tensorDistribEquiv - - -@[simp] -theorem tensorDistribEquiv_tmul (B₁ : QuadraticForm R M₁) (B₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) - (m₁' : M₁) (m₂' : M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₁ m₁ m₁' * B₂ m₂ m₂' := - rfl - -variable (R M₁ M₂) in --- TODO: make this `rfl` -@[simp] -theorem tensorDistribEquiv_toLinearMap : - (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by - ext B₁ B₂ : 3 - apply toLin.injective - ext - exact mul_comm _ _ - -@[simp] -theorem tensorDistribEquiv_apply (B : QuadraticForm R M₁ ⊗ QuadraticForm R M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := - FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B -#align bilin_form.tensor_distrib_equiv_apply QuadraticForm.tensorDistribEquiv_apply - -end CommRing - end QuadraticForm From 4ad432b9abacf2804e0a90bd766bcbfa8fcd004c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 15:36:52 +0000 Subject: [PATCH 03/30] update --- .../QuadraticForm/TensorProduct.lean | 45 +++++++++---------- 1 file changed, 20 insertions(+), 25 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index d0fc69bab291c3..9997d2cb2fd74e 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -11,10 +11,8 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic ## Main definitions -* `QuadraticForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying - `B₁` on `M₁` and `B₂` on `M₂`. This construction is not available in characteristic two. -* `QuadraticForm.tensorDistribEquiv`: `QuadraticForm.tensorDistrib` as an equivalence on finite free - modules. +* `QuadraticForm.tensorDistrib (Q₁ ⊗ₜ Q₂)`: the quadratic form on `M₁ ⊗ M₂` constructed by applying + `Q₁` on `M₁` and `Q₂` on `M₂`. This construction is not available in characteristic two. -/ @@ -34,9 +32,6 @@ variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] [Invertible (2 : R)] -instance : Module A (QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂) := - TensorProduct.leftModule - variable (R A) in /-- The tensor product of two quadratic forms injects into quadratic forms on tensor products. @@ -44,37 +39,37 @@ variable (R A) in Note this is heterobasic; the quadratic form on the left can take values in a larger ring than the one on the right. -/ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] QuadraticForm A (M₁ ⊗[R] M₂) := - BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) - ∘ₗ BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) - ∘ₗ AlgebraTensorModule.map + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + let toQ := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) + let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) + let toB := AlgebraTensorModule.map (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticForm.associatedHom R : QuadraticForm R M₁ →ₗ[R] BilinForm R M₁) - + (QuadraticForm.associatedHom R : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + toQ ∘ₗ tmulB ∘ₗ toB -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for -- `R = A` of `Q₁ m₁ * Q₂ m₂`. @[simp] -theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) - (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (A := A) (Q₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = Q₂ m₂ • Q₁ m₁ := - rfl -#align bilin_form.tensor_distrib_tmul QuadraticForm.tensorDistrib_tmulₓ - -/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ +theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) (m₁ : M₁) (m₂ : M₂) : + tensorDistrib R A (Q₁ ⊗ₜ Q₂) (m₁ ⊗ₜ m₂) = Q₂ m₂ • Q₁ m₁ := + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + (BilinForm.tensorDistrib_tmul _ _ _ _ _ _).trans <| congr_arg₂ _ + (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) + +/-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ @[reducible] -protected def tmul (B₁ : QuadraticForm A M₁) (B₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := - tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) -#align bilin_form.tmul QuadraticForm.tmul +protected def tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + QuadraticForm A (M₁ ⊗[R] M₂) := + tensorDistrib (A := A) (Q₁ ⊗ₜ[R] Q₂) -/-- The base change of a bilinear form. -/ +/-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := - rfl + tensorDistrib_tmul _ _ end CommSemiring From 71a91116cab3bc963b134c7fa910d36b3e192538 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 16:32:59 +0000 Subject: [PATCH 04/30] cleanup --- .../QuadraticForm/TensorProduct.lean | 30 ++++++++++++------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 9997d2cb2fd74e..891cb0ed6e76d2 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -16,10 +16,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic -/ +universe uι uR uA uM₁ uM₂ -universe u v w uι uR uA uM₁ uM₂ - -variable {ι : Type _} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} +variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} open TensorProduct @@ -57,20 +56,31 @@ theorem tensorDistrib_tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R (associated_eq_self_apply _ _ _) (associated_eq_self_apply _ _ _) /-- The tensor product of two quadratic forms, a shorthand for dot notation. -/ -@[reducible] -protected def tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : +protected abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : QuadraticForm A (M₁ ⊗[R] M₂) := - tensorDistrib (A := A) (Q₁ ⊗ₜ[R] Q₂) + tensorDistrib R A (Q₁ ⊗ₜ[R] Q₂) + +theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) : + associated (R₁ := A) (Q₁.tmul Q₂) + = (associated (R₁ := A) Q₁).tmul (associated (R₁ := R) Q₂) := by + rw [QuadraticForm.tmul, tensorDistrib, BilinForm.tmul] + dsimp + convert associated_left_inverse A ((associated_isSymm A Q₁).tmul (associated_isSymm R Q₂)) /-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := - QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq) Q + QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : - Q.baseChange (a ⊗ₜ m₂) = Q m₂ • a := - tensorDistrib_tmul _ _ + Q.baseChange (a ⊗ₜ m₂) = Q m₂ • (a * a) := + tensorDistrib_tmul _ _ _ _ + +@[simp] +theorem associated_baseChange (Q : QuadraticForm R M₂) : + associated (R₁ := A) Q.baseChange = (associated (R := R) Q).baseChange := + associated_tmul _ Q -end CommSemiring +end CommRing end QuadraticForm From 301236d1825bca5c06109b1e8515798a7f3381e7 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 16:36:02 +0000 Subject: [PATCH 05/30] add import --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index ed74b98b7cce33..3eeffbe9c45016 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2259,6 +2259,7 @@ import Mathlib.LinearAlgebra.QuadraticForm.Complex import Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv import Mathlib.LinearAlgebra.QuadraticForm.Prod import Mathlib.LinearAlgebra.QuadraticForm.Real +import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct import Mathlib.LinearAlgebra.Quotient import Mathlib.LinearAlgebra.QuotientPi import Mathlib.LinearAlgebra.Ray From 11339396f023100b4d4407efd6912d412d4736de Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 17:00:30 +0000 Subject: [PATCH 06/30] fix --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 891cb0ed6e76d2..8c3b2607d6f231 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -42,8 +42,8 @@ def tensorDistrib : QuadraticForm A M₁ ⊗[R] QuadraticForm R M₂ →ₗ[A] Q let toQ := BilinForm.toQuadraticFormLinearMap A A (M₁ ⊗[R] M₂) let tmulB := BilinForm.tensorDistrib R A (M₁ := M₁) (M₂ := M₂) let toB := AlgebraTensorModule.map - (QuadraticForm.associatedHom A : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) - (QuadraticForm.associatedHom R : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) + (QuadraticForm.associated : QuadraticForm A M₁ →ₗ[A] BilinForm A M₁) + (QuadraticForm.associated : QuadraticForm R M₂ →ₗ[R] BilinForm R M₂) toQ ∘ₗ tmulB ∘ₗ toB -- TODO: make the RHS `MulOpposite.op (Q₂ m₂) • Q₁ m₁` so that this has a nicer defeq for @@ -77,8 +77,8 @@ theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : tensorDistrib_tmul _ _ _ _ @[simp] -theorem associated_baseChange (Q : QuadraticForm R M₂) : - associated (R₁ := A) Q.baseChange = (associated (R := R) Q).baseChange := +theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : + associated (R₁ := A) Q.baseChange = (associated (R₁ := R) Q).baseChange := associated_tmul _ Q end CommRing From 4f85ca3c3e961515a03e8785ec34faeb9463e3b2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 17:27:09 +0000 Subject: [PATCH 07/30] helper lemma --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 5 +++++ Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 10 ++++++---- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 74e3b800c58e5b..1e9b3dcac3f8ec 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -883,6 +883,11 @@ theorem associated_linMulLin (f g : M →ₗ[R₁] R₁) : ring #align quadratic_form.associated_lin_mul_lin QuadraticForm.associated_linMulLin +@[simp] +lemma associated_sq : associated (R₁ := R₁) sq = LinearMap.toBilin (LinearMap.mul R₁ R₁) := + (associated_linMulLin (LinearMap.id) (LinearMap.id)).trans <| + by simp only [smul_add, invOf_two_smul_add_invOf_two_smul]; rfl + end Associated section Anisotropic diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 8c3b2607d6f231..6fb2cf3223985c 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -67,19 +67,21 @@ 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₂)) +variable (A) in /-- The base change of a quadratic form. -/ protected def baseChange (Q : QuadraticForm R M₂) : QuadraticForm A (A ⊗[R] M₂) := QuadraticForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (QuadraticForm.sq (R := A)) Q @[simp] theorem baseChange_tmul (Q : QuadraticForm R M₂) (a : A) (m₂ : M₂) : - Q.baseChange (a ⊗ₜ m₂) = Q m₂ • (a * a) := + Q.baseChange A (a ⊗ₜ m₂) = Q m₂ • (a * a) := tensorDistrib_tmul _ _ _ _ -@[simp] + theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) : - associated (R₁ := A) Q.baseChange = (associated (R₁ := R) Q).baseChange := - associated_tmul _ Q + 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] end CommRing From 0e1ef110b99da72ddc93230f03494cd06d8d73a4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 18 Aug 2023 07:11:53 +0100 Subject: [PATCH 08/30] Update Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean Co-authored-by: Alex J Best --- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index 6fb2cf3223985c..3e35eb9fbbea8a 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean @@ -16,9 +16,9 @@ import Mathlib.LinearAlgebra.QuadraticForm.Basic -/ -universe uι uR uA uM₁ uM₂ +universe uR uA uM₁ uM₂ -variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} +variable {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} open TensorProduct From 89fef2c950b18d95ddf073c58f3d7a9e8cb96c42 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 09:23:13 +0000 Subject: [PATCH 09/30] feat: base change of Clifford algebras --- Mathlib.lean | 1 + .../CliffordAlgebra/BaseChange.lean | 200 ++++++++++++++++++ 2 files changed, 201 insertions(+) create mode 100644 Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean diff --git a/Mathlib.lean b/Mathlib.lean index 3eeffbe9c45016..0163ac6cc49ec3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2157,6 +2157,7 @@ import Mathlib.LinearAlgebra.BilinearMap import Mathlib.LinearAlgebra.Charpoly.Basic import Mathlib.LinearAlgebra.Charpoly.ToMatrix import Mathlib.LinearAlgebra.CliffordAlgebra.Basic +import Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction import Mathlib.LinearAlgebra.CliffordAlgebra.Equivs diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean new file mode 100644 index 00000000000000..758ea7ba19c815 --- /dev/null +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -0,0 +1,200 @@ +/- +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.TensorProduct +import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation +import Mathlib.Data.Complex.Module +import Mathlib.RingTheory.TensorProduct + +variable {V : Type*} [AddCommGroup V] [Module ℝ V] + +open scoped TensorProduct + +namespace QuadraticForm + +/-- The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$. -/ +@[reducible] +noncomputable def complexify (Q : QuadraticForm ℝ V) : QuadraticForm ℂ (ℂ ⊗[ℝ] V) := + Q.baseChange ℂ + +end QuadraticForm + +namespace CliffordAlgebra + +/-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/ +noncomputable def ofComplexifyAux (Q : QuadraticForm ℝ V) : + CliffordAlgebra Q →ₐ[ℝ] CliffordAlgebra Q.complexify := + CliffordAlgebra.lift Q <| by + letI : Invertible (2 : ℂ) := invertibleTwo + refine ⟨(ι Q.complexify).restrictScalars ℝ ∘ₗ TensorProduct.mk ℝ ℂ V 1, fun v => ?_⟩ + refine (CliffordAlgebra.ι_sq_scalar Q.complexify (1 ⊗ₜ v)).trans ?_ + rw [QuadraticForm.baseChange_tmul, one_mul, ←Algebra.algebraMap_eq_smul_one, + ←IsScalarTower.algebraMap_apply] + +@[simp] lemma ofComplexifyAux_ι (Q : QuadraticForm ℝ V) (v : V) : + ofComplexifyAux Q (ι Q v) = ι Q.complexify (1 ⊗ₜ v) := + CliffordAlgebra.lift_ι_apply _ _ _ + +/-- Convert from the complexified clifford algebra to the clifford algebra over a complexified +module. -/ +noncomputable def ofComplexify (Q : QuadraticForm ℝ V) : + ℂ ⊗[ℝ] CliffordAlgebra Q →ₐ[ℂ] CliffordAlgebra Q.complexify := + Algebra.TensorProduct.algHomOfLinearMapTensorProduct + (TensorProduct.AlgebraTensorModule.lift $ + let f : ℂ →ₗ[ℂ] _ := (Algebra.lsmul ℂ ℂ (CliffordAlgebra Q.complexify)).toLinearMap + LinearMap.flip $ LinearMap.flip (({ + toFun := fun f : CliffordAlgebra Q.complexify →ₗ[ℂ] CliffordAlgebra Q.complexify => + LinearMap.restrictScalars ℝ f + map_add' := fun f g => LinearMap.ext $ fun x => rfl + map_smul' := fun (c : ℂ) g => LinearMap.ext $ fun x => rfl + } : _ →ₗ[ℂ] _) ∘ₗ f) ∘ₗ (ofComplexifyAux Q).toLinearMap) + (fun z₁ z₂ b₁ b₂ => + show (z₁ * z₂) • ofComplexifyAux Q (b₁ * b₂) + = z₁ • ofComplexifyAux Q b₁ * z₂ • ofComplexifyAux Q b₂ + by rw [map_mul, smul_mul_smul]) + (fun r => + show r • ofComplexifyAux Q 1 = algebraMap ℂ (CliffordAlgebra Q.complexify) r + by rw [map_one, Algebra.algebraMap_eq_smul_one]) + +@[simp] lemma ofComplexify_tmul_ι (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : + ofComplexify Q (z ⊗ₜ ι Q v) = ι Q.complexify (z ⊗ₜ v) := by + show z • ofComplexifyAux Q (ι Q v) = ι Q.complexify (z ⊗ₜ[ℝ] v) + rw [ofComplexifyAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one] + +@[simp] lemma ofComplexify_tmul_one (Q : QuadraticForm ℝ V) (z : ℂ) : + ofComplexify Q (z ⊗ₜ 1) = algebraMap _ _ z := by + show z • ofComplexifyAux Q 1 = _ + rw [map_one, ←Algebra.algebraMap_eq_smul_one] + +lemma _root_.CliffordAlgebra.preserves_iff_bilin {R A M} [CommRing R] [Ring A] [Algebra R A] + [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) + (h2 : IsUnit (2 : R)) + (f : M →ₗ[R] A) : + (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔ + ((LinearMap.mul R A).compl₂ f) ∘ₗ f + ((LinearMap.mul R A).flip.compl₂ f) ∘ₗ f = + Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by + simp_rw [FunLike.ext_iff] + dsimp only [LinearMap.compr₂_apply, LinearMap.compl₂_apply, LinearMap.comp_apply, + Algebra.linearMap_apply, LinearMap.mul_apply', BilinForm.toLin_apply, LinearMap.add_apply, + LinearMap.flip_apply] + have h2a := h2.map (algebraMap R A) + refine ⟨fun h x y => ?_, fun h x => ?_⟩ + · rw [QuadraticForm.polarBilin_apply, QuadraticForm.polar, sub_sub, map_sub, map_add, + ←h x, ←h y, ←h (x + y), eq_sub_iff_add_eq, map_add, + add_mul, mul_add, mul_add, add_comm (f x * f x) (f x * f y), + add_add_add_comm] + · apply h2a.mul_left_cancel + simp_rw [←Algebra.smul_def, two_smul] + rw [h x x, QuadraticForm.polarBilin_apply, QuadraticForm.polar_self, two_mul, map_add] + +#check 1 +variable (Q : QuadraticForm ℝ V) in +#synth IsScalarTower ℝ ℂ (ℂ ⊗[ℝ] V →ₗ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q) + +/-- Convert from the clifford algebra over a complexified module to the complexified clifford +algebra. -/ +noncomputable def toComplexify (Q : QuadraticForm ℝ V) : + CliffordAlgebra Q.complexify →ₐ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q := + CliffordAlgebra.lift _ <| by + let φ := TensorProduct.AlgebraTensorModule.map (LinearMap.id : ℂ →ₗ[ℂ] ℂ) (ι Q) + refine ⟨φ, ?_⟩ + rw [CliffordAlgebra.preserves_iff_bilin _ (IsUnit.mk0 (2 : ℂ) two_ne_zero)] + letI : IsScalarTower ℝ ℂ (ℂ ⊗[ℝ] V →ₗ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q) := + LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap + sorry + -- refine TensorProduct.AlgebraTensorModule.curry_injective ?_ + -- ext v w + -- change (1 * 1) ⊗ₜ[ℝ] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[ℝ] (ι Q w * ι Q v) = + -- QuadraticForm.polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) ⊗ₜ[ℝ] 1 + -- rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, + -- QuadraticForm.baseChange_polar_apply, one_mul, one_mul, + -- Algebra.TensorProduct.algebraMap_tmul_one] + +@[simp] lemma toComplexify_ι (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : + toComplexify Q (ι Q.complexify (z ⊗ₜ v)) = z ⊗ₜ ι Q v := + CliffordAlgebra.lift_ι_apply _ _ _ + +lemma toComplexify_comp_involute (Q : QuadraticForm ℝ V) : + (toComplexify Q).comp (involute : CliffordAlgebra Q.complexify →ₐ[ℂ] _) = + (Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toComplexify Q) := by + ext v + show toComplexify Q (involute (ι Q.complexify (1 ⊗ₜ[ℝ] v))) + = (Algebra.TensorProduct.map (AlgHom.id _ _) involute : + ℂ ⊗[ℝ] CliffordAlgebra Q →ₐ[ℂ] _) + (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v))) + rw [toComplexify_ι, involute_ι, map_neg (toComplexify Q), toComplexify_ι, + Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg] + +/-- The involution acts only on the right of the tensor product. -/ +lemma toComplexify_involute (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : + toComplexify Q (involute x) = + TensorProduct.map LinearMap.id (involute.toLinearMap) (toComplexify Q x) := + FunLike.congr_fun (toComplexify_comp_involute Q) x + +open MulOpposite + +-- /-- Auxiliary lemma used to prove `toComplexify_reverse` without needing induction. -/ +-- lemma toComplexify_comp_reverse_aux (Q : QuadraticForm ℝ V) : +-- (toComplexify Q).op.comp (reverse_aux Q.complexify) = +-- ((Algebra.TensorProduct.op_alg_equiv ℂ).to_algHom.comp $ +-- (Algebra.TensorProduct.map' ((algHom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q)).comp +-- (toComplexify Q)) := by +-- ext v +-- show +-- op (toComplexify Q (reverse (ι Q.complexify (1 ⊗ₜ[ℝ] v)))) = +-- Algebra.TensorProduct.op_alg_equiv ℂ +-- (Algebra.TensorProduct.map' ((algHom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q) +-- (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v)))) +-- rw [toComplexify_ι, reverse_ι, toComplexify_ι, Algebra.TensorProduct.map'_tmul, +-- Algebra.TensorProduct.op_alg_equiv_tmul, unop_reverse_aux, reverse_ι] +-- rfl + +-- /-- `reverse` acts only on the right of the tensor product. -/ +-- lemma toComplexify_reverse (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : +-- toComplexify Q (reverse x) = +-- TensorProduct.map LinearMap.id (reverse : _ →ₗ[ℝ] _) (toComplexify Q x) := by +-- have := fun_like.congr_fun (toComplexify_comp_reverse_aux Q) x +-- refine (congr_arg unop this).trans _; clear this +-- refine (TensorProduct.AlgebraTensorModule.map_map _ _ _ _ _).trans _ +-- erw [←reverse_eq_reverse_aux, algHom.toLinearMap_to_opposite, +-- TensorProduct.AlgebraTensorModule.map_apply] + +attribute [ext] TensorProduct.ext + +lemma toComplexify_comp_ofComplexify (Q : QuadraticForm ℝ V) : + (toComplexify Q).comp (ofComplexify Q) = AlgHom.id _ _ := by + ext z : 2 + · change toComplexify Q (ofComplexify Q (z ⊗ₜ[ℝ] 1)) = z ⊗ₜ[ℝ] 1 + rw [ofComplexify_tmul_one, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply, + Algebra.id.map_eq_self] + · ext v : 1 + change toComplexify Q (ofComplexify Q (1 ⊗ₜ[ℝ] ι Q v)) = 1 ⊗ₜ[ℝ] ι Q v + rw [ofComplexify_tmul_ι, toComplexify_ι] + +@[simp] lemma toComplexify_ofComplexify (Q : QuadraticForm ℝ V) (x : ℂ ⊗[ℝ] CliffordAlgebra Q) : + toComplexify Q (ofComplexify Q x) = x := + AlgHom.congr_fun (toComplexify_comp_ofComplexify Q : _) x + +lemma ofComplexify_comp_toComplexify (Q : QuadraticForm ℝ V) : + (ofComplexify Q).comp (toComplexify Q) = AlgHom.id _ _ := by + ext x + show ofComplexify Q (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] x))) = ι Q.complexify (1 ⊗ₜ[ℝ] x) + rw [toComplexify_ι, ofComplexify_tmul_ι] + +@[simp] lemma ofComplexify_toComplexify + (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : + ofComplexify Q (toComplexify Q x) = x := + AlgHom.congr_fun (ofComplexify_comp_toComplexify Q : _) x + +/-- Complexifying the vector space of a clifford algebra is isomorphic as a ℂ-algebra to +complexifying the clifford algebra itself; $Cℓ(ℂ ⊗_ℝ V, Q_ℂ) ≅ ℂ ⊗_ℝ Cℓ(V, Q)$. + +This is `CliffordAlgebra.toComplexify` and `CliffordAlgebra.ofComplexify` as an equivalence. -/ +@[simps!] +noncomputable def equivComplexify (Q : QuadraticForm ℝ V) : + CliffordAlgebra Q.complexify ≃ₐ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q := + AlgEquiv.ofAlgHom (toComplexify Q) (ofComplexify Q) + (toComplexify_comp_ofComplexify Q) + (ofComplexify_comp_toComplexify Q) From 570460e0425f8043301a7e7918b8ec8009bea9b3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 09:48:47 +0000 Subject: [PATCH 10/30] a bit closer to fixed --- .../CliffordAlgebra/BaseChange.lean | 213 +++++++++--------- 1 file changed, 105 insertions(+), 108 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 758ea7ba19c815..56c623bbffa8bc 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -3,72 +3,71 @@ 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.Data.Complex.Module import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation -import Mathlib.Data.Complex.Module +import Mathlib.LinearAlgebra.TensorProduct.Opposite import Mathlib.RingTheory.TensorProduct -variable {V : Type*} [AddCommGroup V] [Module ℝ V] - -open scoped TensorProduct +#check 1 -namespace QuadraticForm +variable {R A V : Type*} +variable [CommRing R] [CommRing A] [AddCommGroup V] +variable [Algebra R A] [Module R V] [Module A V] [IsScalarTower R A V] +variable [Invertible (2 : R)] -/-- The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$. -/ -@[reducible] -noncomputable def complexify (Q : QuadraticForm ℝ V) : QuadraticForm ℂ (ℂ ⊗[ℝ] V) := - Q.baseChange ℂ +open scoped TensorProduct -end QuadraticForm namespace CliffordAlgebra +variable (A) + /-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/ -noncomputable def ofComplexifyAux (Q : QuadraticForm ℝ V) : - CliffordAlgebra Q →ₐ[ℝ] CliffordAlgebra Q.complexify := +noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) : + CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) := CliffordAlgebra.lift Q <| by - letI : Invertible (2 : ℂ) := invertibleTwo - refine ⟨(ι Q.complexify).restrictScalars ℝ ∘ₗ TensorProduct.mk ℝ ℂ V 1, fun v => ?_⟩ - refine (CliffordAlgebra.ι_sq_scalar Q.complexify (1 ⊗ₜ v)).trans ?_ + refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩ + refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_ rw [QuadraticForm.baseChange_tmul, one_mul, ←Algebra.algebraMap_eq_smul_one, ←IsScalarTower.algebraMap_apply] -@[simp] lemma ofComplexifyAux_ι (Q : QuadraticForm ℝ V) (v : V) : - ofComplexifyAux Q (ι Q v) = ι Q.complexify (1 ⊗ₜ v) := - CliffordAlgebra.lift_ι_apply _ _ _ +@[simp] theorem ofBaseChangeAux_ι (Q : QuadraticForm R V) (v : V) : + ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (1 ⊗ₜ v) := + CliffordAlgebra.lift_ι_apply _ _ v -/-- Convert from the complexified clifford algebra to the clifford algebra over a complexified +/-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed module. -/ -noncomputable def ofComplexify (Q : QuadraticForm ℝ V) : - ℂ ⊗[ℝ] CliffordAlgebra Q →ₐ[ℂ] CliffordAlgebra Q.complexify := +noncomputable def ofBaseChange (Q : QuadraticForm R V) : + A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) := Algebra.TensorProduct.algHomOfLinearMapTensorProduct (TensorProduct.AlgebraTensorModule.lift $ - let f : ℂ →ₗ[ℂ] _ := (Algebra.lsmul ℂ ℂ (CliffordAlgebra Q.complexify)).toLinearMap + let f : A →ₗ[A] _ := (Algebra.lsmul A A (CliffordAlgebra (Q.baseChange A))).toLinearMap LinearMap.flip $ LinearMap.flip (({ - toFun := fun f : CliffordAlgebra Q.complexify →ₗ[ℂ] CliffordAlgebra Q.complexify => - LinearMap.restrictScalars ℝ f + toFun := fun f : CliffordAlgebra (Q.baseChange A) →ₗ[A] CliffordAlgebra (Q.baseChange A) => + LinearMap.restrictScalars R f map_add' := fun f g => LinearMap.ext $ fun x => rfl - map_smul' := fun (c : ℂ) g => LinearMap.ext $ fun x => rfl - } : _ →ₗ[ℂ] _) ∘ₗ f) ∘ₗ (ofComplexifyAux Q).toLinearMap) + map_smul' := fun (c : A) g => LinearMap.ext $ fun x => rfl + } : _ →ₗ[A] _) ∘ₗ f) ∘ₗ (ofBaseChangeAux A Q).toLinearMap) (fun z₁ z₂ b₁ b₂ => - show (z₁ * z₂) • ofComplexifyAux Q (b₁ * b₂) - = z₁ • ofComplexifyAux Q b₁ * z₂ • ofComplexifyAux Q b₂ + show (z₁ * z₂) • ofBaseChangeAux A Q (b₁ * b₂) + = z₁ • ofBaseChangeAux A Q b₁ * z₂ • ofBaseChangeAux A Q b₂ by rw [map_mul, smul_mul_smul]) (fun r => - show r • ofComplexifyAux Q 1 = algebraMap ℂ (CliffordAlgebra Q.complexify) r + show r • ofBaseChangeAux A Q 1 = algebraMap A (CliffordAlgebra (Q.baseChange A)) r by rw [map_one, Algebra.algebraMap_eq_smul_one]) -@[simp] lemma ofComplexify_tmul_ι (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : - ofComplexify Q (z ⊗ₜ ι Q v) = ι Q.complexify (z ⊗ₜ v) := by - show z • ofComplexifyAux Q (ι Q v) = ι Q.complexify (z ⊗ₜ[ℝ] v) - rw [ofComplexifyAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one] +@[simp] theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) : + ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v) := by + show z • ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v) + rw [ofBaseChangeAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one] -@[simp] lemma ofComplexify_tmul_one (Q : QuadraticForm ℝ V) (z : ℂ) : - ofComplexify Q (z ⊗ₜ 1) = algebraMap _ _ z := by - show z • ofComplexifyAux Q 1 = _ +@[simp] theorem ofBaseChange_tmul_one (Q : QuadraticForm R V) (z : A) : + ofBaseChange A Q (z ⊗ₜ 1) = algebraMap _ _ z := by + show z • ofBaseChangeAux A Q 1 = _ rw [map_one, ←Algebra.algebraMap_eq_smul_one] -lemma _root_.CliffordAlgebra.preserves_iff_bilin {R A M} [CommRing R] [Ring A] [Algebra R A] +theorem _root_.CliffordAlgebra.preserves_iff_bilin {R A M} [CommRing R] [Ring A] [Algebra R A] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsUnit (2 : R)) (f : M →ₗ[R] A) : @@ -89,73 +88,71 @@ lemma _root_.CliffordAlgebra.preserves_iff_bilin {R A M} [CommRing R] [Ring A] [ simp_rw [←Algebra.smul_def, two_smul] rw [h x x, QuadraticForm.polarBilin_apply, QuadraticForm.polar_self, two_mul, map_add] -#check 1 -variable (Q : QuadraticForm ℝ V) in -#synth IsScalarTower ℝ ℂ (ℂ ⊗[ℝ] V →ₗ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q) - -/-- Convert from the clifford algebra over a complexified module to the complexified clifford +set_option maxHeartbeats 400000 in +/-- Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra. -/ -noncomputable def toComplexify (Q : QuadraticForm ℝ V) : - CliffordAlgebra Q.complexify →ₐ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q := +noncomputable def toBaseChange (Q : QuadraticForm R V) : + CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q := CliffordAlgebra.lift _ <| by - let φ := TensorProduct.AlgebraTensorModule.map (LinearMap.id : ℂ →ₗ[ℂ] ℂ) (ι Q) + let φ := TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q) refine ⟨φ, ?_⟩ - rw [CliffordAlgebra.preserves_iff_bilin _ (IsUnit.mk0 (2 : ℂ) two_ne_zero)] - letI : IsScalarTower ℝ ℂ (ℂ ⊗[ℝ] V →ₗ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q) := + letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm + rw [CliffordAlgebra.preserves_iff_bilin _ (isUnit_of_invertible _)] + letI : IsScalarTower R A (A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) := LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap + refine TensorProduct.AlgebraTensorModule.curry_injective ?_ + ext v w + change (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) = + QuadraticForm.polar (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 + rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap] + -- QuadraticForm.baseChange_polar_apply, one_mul, one_mul, + -- Algebra.TensorProduct.algebraMap_tmul_one] sorry - -- refine TensorProduct.AlgebraTensorModule.curry_injective ?_ - -- ext v w - -- change (1 * 1) ⊗ₜ[ℝ] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[ℝ] (ι Q w * ι Q v) = - -- QuadraticForm.polar (Q.complexify) (1 ⊗ₜ[ℝ] v) (1 ⊗ₜ[ℝ] w) ⊗ₜ[ℝ] 1 - -- rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, - -- QuadraticForm.baseChange_polar_apply, one_mul, one_mul, - -- Algebra.TensorProduct.algebraMap_tmul_one] - -@[simp] lemma toComplexify_ι (Q : QuadraticForm ℝ V) (z : ℂ) (v : V) : - toComplexify Q (ι Q.complexify (z ⊗ₜ v)) = z ⊗ₜ ι Q v := + +@[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) : + toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v := CliffordAlgebra.lift_ι_apply _ _ _ -lemma toComplexify_comp_involute (Q : QuadraticForm ℝ V) : - (toComplexify Q).comp (involute : CliffordAlgebra Q.complexify →ₐ[ℂ] _) = - (Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toComplexify Q) := by +theorem toBaseChange_comp_involute (Q : QuadraticForm R V) : + (toBaseChange A Q).comp (involute : CliffordAlgebra (Q.baseChange A) →ₐ[A] _) = + (Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toBaseChange A Q) := by ext v - show toComplexify Q (involute (ι Q.complexify (1 ⊗ₜ[ℝ] v))) + show toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v))) = (Algebra.TensorProduct.map (AlgHom.id _ _) involute : - ℂ ⊗[ℝ] CliffordAlgebra Q →ₐ[ℂ] _) - (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v))) - rw [toComplexify_ι, involute_ι, map_neg (toComplexify Q), toComplexify_ι, + A ⊗[R] CliffordAlgebra Q →ₐ[A] _) + (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))) + rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι, Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg] /-- The involution acts only on the right of the tensor product. -/ -lemma toComplexify_involute (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : - toComplexify Q (involute x) = - TensorProduct.map LinearMap.id (involute.toLinearMap) (toComplexify Q x) := - FunLike.congr_fun (toComplexify_comp_involute Q) x +theorem toBaseChange_involute (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : + toBaseChange A Q (involute x) = + TensorProduct.map LinearMap.id (involute.toLinearMap) (toBaseChange A Q x) := + FunLike.congr_fun (toBaseChange_comp_involute A Q) x open MulOpposite --- /-- Auxiliary lemma used to prove `toComplexify_reverse` without needing induction. -/ --- lemma toComplexify_comp_reverse_aux (Q : QuadraticForm ℝ V) : --- (toComplexify Q).op.comp (reverse_aux Q.complexify) = --- ((Algebra.TensorProduct.op_alg_equiv ℂ).to_algHom.comp $ --- (Algebra.TensorProduct.map' ((algHom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q)).comp --- (toComplexify Q)) := by +-- /-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/ +-- theorem toBaseChange_comp_reverse_aux (Q : QuadraticForm R V) : +-- (toBaseChange A Q).op.comp (reverse_aux (Q.baseChange A)) = +-- ((Algebra.TensorProduct.op_alg_equiv A).to_algHom.comp $ +-- (Algebra.TensorProduct.map' ((algHom.id A A).to_opposite commute.all) (reverse_aux Q)).comp +-- (toBaseChange A Q)) := by -- ext v -- show --- op (toComplexify Q (reverse (ι Q.complexify (1 ⊗ₜ[ℝ] v)))) = --- Algebra.TensorProduct.op_alg_equiv ℂ --- (Algebra.TensorProduct.map' ((algHom.id ℂ ℂ).to_opposite commute.all) (reverse_aux Q) --- (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] v)))) --- rw [toComplexify_ι, reverse_ι, toComplexify_ι, Algebra.TensorProduct.map'_tmul, +-- op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = +-- Algebra.TensorProduct.op_alg_equiv A +-- (Algebra.TensorProduct.map' ((algHom.id A A).to_opposite commute.all) (reverse_aux Q) +-- (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) +-- rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map'_tmul, -- Algebra.TensorProduct.op_alg_equiv_tmul, unop_reverse_aux, reverse_ι] -- rfl -- /-- `reverse` acts only on the right of the tensor product. -/ --- lemma toComplexify_reverse (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : --- toComplexify Q (reverse x) = --- TensorProduct.map LinearMap.id (reverse : _ →ₗ[ℝ] _) (toComplexify Q x) := by --- have := fun_like.congr_fun (toComplexify_comp_reverse_aux Q) x +-- theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : +-- toBaseChange A Q (reverse x) = +-- TensorProduct.map LinearMap.id (reverse : _ →ₗ[R] _) (toBaseChange A Q x) := by +-- have := fun_like.congr_fun (toBaseChange_comp_reverse_aux Q) x -- refine (congr_arg unop this).trans _; clear this -- refine (TensorProduct.AlgebraTensorModule.map_map _ _ _ _ _).trans _ -- erw [←reverse_eq_reverse_aux, algHom.toLinearMap_to_opposite, @@ -163,38 +160,38 @@ open MulOpposite attribute [ext] TensorProduct.ext -lemma toComplexify_comp_ofComplexify (Q : QuadraticForm ℝ V) : - (toComplexify Q).comp (ofComplexify Q) = AlgHom.id _ _ := by +theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) : + (toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id _ _ := by ext z : 2 - · change toComplexify Q (ofComplexify Q (z ⊗ₜ[ℝ] 1)) = z ⊗ₜ[ℝ] 1 - rw [ofComplexify_tmul_one, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply, + · change toBaseChange A Q (ofBaseChange A Q (z ⊗ₜ[R] 1)) = z ⊗ₜ[R] 1 + rw [ofBaseChange_tmul_one, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply, Algebra.id.map_eq_self] · ext v : 1 - change toComplexify Q (ofComplexify Q (1 ⊗ₜ[ℝ] ι Q v)) = 1 ⊗ₜ[ℝ] ι Q v - rw [ofComplexify_tmul_ι, toComplexify_ι] + change toBaseChange A Q (ofBaseChange A Q (1 ⊗ₜ[R] ι Q v)) = 1 ⊗ₜ[R] ι Q v + rw [ofBaseChange_tmul_ι, toBaseChange_ι] -@[simp] lemma toComplexify_ofComplexify (Q : QuadraticForm ℝ V) (x : ℂ ⊗[ℝ] CliffordAlgebra Q) : - toComplexify Q (ofComplexify Q x) = x := - AlgHom.congr_fun (toComplexify_comp_ofComplexify Q : _) x +@[simp] theorem toBaseChange_ofBaseChange (Q : QuadraticForm R V) (x : A ⊗[R] CliffordAlgebra Q) : + toBaseChange A Q (ofBaseChange A Q x) = x := + AlgHom.congr_fun (toBaseChange_comp_ofBaseChange A Q : _) x -lemma ofComplexify_comp_toComplexify (Q : QuadraticForm ℝ V) : - (ofComplexify Q).comp (toComplexify Q) = AlgHom.id _ _ := by +theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) : + (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _ := by ext x - show ofComplexify Q (toComplexify Q (ι Q.complexify (1 ⊗ₜ[ℝ] x))) = ι Q.complexify (1 ⊗ₜ[ℝ] x) - rw [toComplexify_ι, ofComplexify_tmul_ι] + show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x))) = ι (Q.baseChange A) (1 ⊗ₜ[R] x) + rw [toBaseChange_ι, ofBaseChange_tmul_ι] -@[simp] lemma ofComplexify_toComplexify - (Q : QuadraticForm ℝ V) (x : CliffordAlgebra Q.complexify) : - ofComplexify Q (toComplexify Q x) = x := - AlgHom.congr_fun (ofComplexify_comp_toComplexify Q : _) x +@[simp] theorem ofBaseChange_toBaseChange + (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : + ofBaseChange A Q (toBaseChange A Q x) = x := + AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q : _) x -/-- Complexifying the vector space of a clifford algebra is isomorphic as a ℂ-algebra to -complexifying the clifford algebra itself; $Cℓ(ℂ ⊗_ℝ V, Q_ℂ) ≅ ℂ ⊗_ℝ Cℓ(V, Q)$. +/-- Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to +base-changing the clifford algebra itself; $Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)$. -This is `CliffordAlgebra.toComplexify` and `CliffordAlgebra.ofComplexify` as an equivalence. -/ +This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/ @[simps!] -noncomputable def equivComplexify (Q : QuadraticForm ℝ V) : - CliffordAlgebra Q.complexify ≃ₐ[ℂ] ℂ ⊗[ℝ] CliffordAlgebra Q := - AlgEquiv.ofAlgHom (toComplexify Q) (ofComplexify Q) - (toComplexify_comp_ofComplexify Q) - (ofComplexify_comp_toComplexify Q) +noncomputable def equivBaseChange (Q : QuadraticForm R V) : + CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q := + AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q) + (toBaseChange_comp_ofBaseChange A Q) + (ofBaseChange_comp_toBaseChange A Q) From 9c091cddf4461c384f6ddbb70b5562fbd336a560 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 10:13:14 +0000 Subject: [PATCH 11/30] missing functorial lemmas --- .../LinearAlgebra/TensorProduct/Tower.lean | 23 +++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index a128a867aa6c1c..d537a6c5e25a10 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -49,9 +49,9 @@ namespace TensorProduct namespace AlgebraTensorModule -universe uR uA uB uM uN uP uQ +universe uR uA uB uM uN uP uQ uP' uQ' variable {R : Type uR} {A : Type uA} {B : Type uB} -variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} +variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} open LinearMap open Algebra (lsmul) @@ -70,6 +70,11 @@ variable [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] variable [AddCommMonoid Q] [Module R Q] +variable [AddCommMonoid P'] [Module R P'] [Module A P'] [Module B P'] +variable [IsScalarTower R A P'] [IsScalarTower R B P'] [SMulCommClass A B P'] + +variable [AddCommMonoid Q'] [Module R Q'] + theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R R M a).rTensor N x := rfl #align tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor @@ -197,6 +202,20 @@ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +@[simp] +theorem map_id : map (id : M →ₗ[A] M) (id : N →ₗ[R] N) = .id := + ext fun _ _ => rfl + +theorem map_comp (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : + map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) := + ext fun _ _ => rfl + +@[simp] +theorem map_one : map (1 : M →ₗ[A] M) (1 : N →ₗ[R] N) = 1 := map_id + +theorem map_mul (f₂ : M →ₗ[A] M) (f₁ : M →ₗ[A] M) (g₂ : N →ₗ[R] N) (g₁ : N →ₗ[R] N) : + map (f₂ * f₁) (g₂ * g₁) = map f₂ g₂ * map f₁ g₁ := map_comp _ _ _ _ + theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := by ext From 3eb62336c8bf65ea1cf5b5835b87835df2f3a135 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 10:13:47 +0000 Subject: [PATCH 12/30] expose implementation details of 'reverse' --- .../CliffordAlgebra/Conjugation.lean | 35 +++++++++++++------ 1 file changed, 24 insertions(+), 11 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean index 351d54422c3332..1de525367c5a18 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean @@ -80,15 +80,26 @@ section Reverse open MulOpposite +/-- `CliffordAlgebra.reverse` as an `AlgEquiv` to the opposite algebra -/ +def reverseOp : CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ := + CliffordAlgebra.lift Q + ⟨(MulOpposite.opLinearEquiv R).toLinearMap.comp (ι Q), fun m => + unop_injective <| by simp⟩ + +-- porting note: can't infer `Q` +@[simp] +theorem reverseOp_ι (m : M) : reverseOp (ι Q m) = op (ι Q m) := lift_ι_apply _ _ _ + /-- Grade reversion, inverting the multiplication order of basis vectors. Also called *transpose* in some literature. -/ def reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q := - (opLinearEquiv R).symm.toLinearMap.comp - (CliffordAlgebra.lift Q - ⟨(MulOpposite.opLinearEquiv R).toLinearMap.comp (ι Q), fun m => - unop_injective <| by simp⟩).toLinearMap + (opLinearEquiv R).symm.toLinearMap.comp reverseOp.toLinearMap #align clifford_algebra.reverse CliffordAlgebra.reverse +@[simp] theorem unop_reverseOp (x : CliffordAlgebra Q) : (reverseOp x).unop = reverse x := rfl + +@[simp] theorem op_reverse (x : CliffordAlgebra Q) : op (reverse x) = reverseOp x := rfl + -- porting note: can't infer `Q` @[simp] theorem reverse_ι (m : M) : reverse (Q := Q) (ι Q m) = ι Q m := by simp [reverse] @@ -97,20 +108,21 @@ theorem reverse_ι (m : M) : reverse (Q := Q) (ι Q m) = ι Q m := by simp [reve @[simp] theorem reverse.commutes (r : R) : -- porting note: can't infer `Q` - reverse (Q := Q) (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := by simp [reverse] + reverse (Q := Q) (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := + op_injective <| reverseOp.commutes r #align clifford_algebra.reverse.commutes CliffordAlgebra.reverse.commutes -- porting note: can't infer `Q` @[simp] -theorem reverse.map_one : reverse (Q := Q) (1 : CliffordAlgebra Q) = 1 := by - convert reverse.commutes (Q := Q) (1 : R) <;> simp +theorem reverse.map_one : reverse (Q := Q) (1 : CliffordAlgebra Q) = 1 := + op_injective reverseOp.map_one #align clifford_algebra.reverse.map_one CliffordAlgebra.reverse.map_one @[simp] theorem reverse.map_mul (a b : CliffordAlgebra Q) : - -- porting note: can't infer `Q` - reverse (Q := Q) (a * b) = reverse (Q := Q) b * reverse (Q := Q) a := by - simp [reverse] + -- porting note: can't infer `Q` + reverse (Q := Q) (a * b) = reverse (Q := Q) b * reverse (Q := Q) a := + op_injective (reverseOp.map_mul a b) #align clifford_algebra.reverse.map_mul CliffordAlgebra.reverse.map_mul @[simp] @@ -254,7 +266,8 @@ theorem submodule_map_reverse_eq_comap (p : Submodule R (CliffordAlgebra Q)) : theorem ι_range_map_reverse : (ι Q).range.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = LinearMap.range (ι Q) := by - rw [reverse, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, ← Submodule.map_comp] + rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, + ← Submodule.map_comp] exact Submodule.map_id _ #align clifford_algebra.ι_range_map_reverse CliffordAlgebra.ι_range_map_reverse From 9012171f219bde2cf0eddc2443ed19b1e099c264 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 10:14:15 +0000 Subject: [PATCH 13/30] wip --- .../CliffordAlgebra/BaseChange.lean | 55 ++++++++++--------- 1 file changed, 30 insertions(+), 25 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 56c623bbffa8bc..d9bc1315cfbe3e 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -132,31 +132,36 @@ theorem toBaseChange_involute (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.ba open MulOpposite --- /-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/ --- theorem toBaseChange_comp_reverse_aux (Q : QuadraticForm R V) : --- (toBaseChange A Q).op.comp (reverse_aux (Q.baseChange A)) = --- ((Algebra.TensorProduct.op_alg_equiv A).to_algHom.comp $ --- (Algebra.TensorProduct.map' ((algHom.id A A).to_opposite commute.all) (reverse_aux Q)).comp --- (toBaseChange A Q)) := by --- ext v --- show --- op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = --- Algebra.TensorProduct.op_alg_equiv A --- (Algebra.TensorProduct.map' ((algHom.id A A).to_opposite commute.all) (reverse_aux Q) --- (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) --- rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map'_tmul, --- Algebra.TensorProduct.op_alg_equiv_tmul, unop_reverse_aux, reverse_ι] --- rfl - --- /-- `reverse` acts only on the right of the tensor product. -/ --- theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : --- toBaseChange A Q (reverse x) = --- TensorProduct.map LinearMap.id (reverse : _ →ₗ[R] _) (toBaseChange A Q x) := by --- have := fun_like.congr_fun (toBaseChange_comp_reverse_aux Q) x --- refine (congr_arg unop this).trans _; clear this --- refine (TensorProduct.AlgebraTensorModule.map_map _ _ _ _ _).trans _ --- erw [←reverse_eq_reverse_aux, algHom.toLinearMap_to_opposite, --- TensorProduct.AlgebraTensorModule.map_apply] +/-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/ +theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) : + (toBaseChange A Q).op.comp (reverseOp (Q := Q.baseChange A)) = + ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp $ + (Algebra.TensorProduct.map ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q))).comp + (toBaseChange A Q)) := by + ext v + save + dsimp only [TensorProduct.AlgebraTensorModule.curry_apply, AlgHom.comp_toLinearMap, + TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.coe_comp, + Function.comp_apply, AlgHom.toLinearMap_apply, AlgHom.op_apply_apply, AlgEquiv.toAlgHom_eq_coe, + AlgEquiv.toAlgHom_toLinearMap, AlgEquiv.toLinearMap_apply] + -- show + -- op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = + -- Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q) + -- (Algebra.TensorProduct.map ((algHom.id A A).toOpposite Commute.all) (reverseOp Q) + -- (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) + rw [toBaseChange_ι, reverseOp_ι, unop_op, toBaseChange_ι, Algebra.TensorProduct.map_tmul, + Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι, unop_op] + rfl + +/-- `reverse` acts only on the right of the tensor product. -/ +theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : + toBaseChange A Q (reverse x) = + TensorProduct.map LinearMap.id (reverse (Q := Q)) (toBaseChange A Q x) := by + have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x + refine (congr_arg unop this).trans ?_; clear this + refine (TensorProduct.AlgebraTensorModule.map_comp_map _ _ _ _ _).trans ?_ + erw [reverse, AlgHom.toLinearMap_toOpposite, + TensorProduct.AlgebraTensorModule.map_apply] attribute [ext] TensorProduct.ext From f7c2b81f44ab89678b53fb70962ace667d02de62 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 10:13:14 +0000 Subject: [PATCH 14/30] chore(LinearAlgebra/TensorProduct/Tower): missing functorial lemmas --- .../LinearAlgebra/TensorProduct/Tower.lean | 39 ++++++++++++++++++- 1 file changed, 37 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index a128a867aa6c1c..14cf8c23ee4e6e 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -49,9 +49,9 @@ namespace TensorProduct namespace AlgebraTensorModule -universe uR uA uB uM uN uP uQ +universe uR uA uB uM uN uP uQ uP' uQ' variable {R : Type uR} {A : Type uA} {B : Type uB} -variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} +variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} {P' : Type uP'} {Q' : Type uQ'} open LinearMap open Algebra (lsmul) @@ -70,6 +70,11 @@ variable [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] variable [AddCommMonoid Q] [Module R Q] +variable [AddCommMonoid P'] [Module R P'] [Module A P'] [Module B P'] +variable [IsScalarTower R A P'] [IsScalarTower R B P'] [SMulCommClass A B P'] + +variable [AddCommMonoid Q'] [Module R Q'] + theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R R M a).rTensor N x := rfl #align tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor @@ -197,6 +202,20 @@ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +@[simp] +theorem map_id : map (id : M →ₗ[A] M) (id : N →ₗ[R] N) = .id := + ext fun _ _ => rfl + +theorem map_comp (f₂ : P →ₗ[A] P') (f₁ : M →ₗ[A] P) (g₂ : Q →ₗ[R] Q') (g₁ : N →ₗ[R] Q) : + map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) := + ext fun _ _ => rfl + +@[simp] +protected theorem map_one : map (1 : M →ₗ[A] M) (1 : N →ₗ[R] N) = 1 := map_id + +protected theorem map_mul (f₁ f₂ : M →ₗ[A] M) (g₁ g₂ : N →ₗ[R] N) : + map (f₁ * f₂) (g₁ * g₂) = map f₁ g₁ * map f₂ g₂ := map_comp _ _ _ _ + theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := by ext @@ -250,6 +269,22 @@ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.apply_symm_apply _) (g.apply_symm_apply _)) (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.symm_apply_apply _) (g.symm_apply_apply _)) +@[simp] +theorem congr_refl : congr (.refl A M) (.refl R N) = .refl A _ := + LinearEquiv.toLinearMap_injective <| map_id + +theorem congr_trans (f₁ : M ≃ₗ[A] P) (f₂ : P ≃ₗ[A] P') (g₁ : N ≃ₗ[R] Q) (g₂ : Q ≃ₗ[R] Q') : + congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) := + LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _ + +theorem congr_symm (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : congr f.symm g.symm = (congr f g).symm := rfl + +@[simp] +theorem congr_one : congr (1 : M ≃ₗ[A] M) (1 : N ≃ₗ[R] N) = 1 := congr_refl + +theorem congr_mul (f₁ f₂ : M ≃ₗ[A] M) (g₁ g₂ : N ≃ₗ[R] N) : + congr (f₁ * f₂) (g₁ * g₂) = congr f₁ g₁ * congr f₂ g₂ := congr_trans _ _ _ _ + @[simp] theorem congr_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : congr f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl From 88c111b0335a8ec59bf1830949a4e0c5357145a1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 10:13:47 +0000 Subject: [PATCH 15/30] refactor(LinearAlgebra/CliffordAlgebra/Conjugation): expose implementation details of 'reverse' Having the fully-bundled `AlgHom` (to `MulOpposite`) is occasionally useful for building larger `AlgHom`s, especially if the `MulOpposite` can be cancelled out later. --- .../CliffordAlgebra/Conjugation.lean | 34 ++++++++++++------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean index ad1aaee186269d..bb6a003e892e1f 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Conjugation.lean @@ -80,34 +80,43 @@ section Reverse open MulOpposite +/-- `CliffordAlgebra.reverse` as an `AlgHom` to the opposite algebra -/ +def reverseOp : CliffordAlgebra Q →ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ := + CliffordAlgebra.lift Q + ⟨(MulOpposite.opLinearEquiv R).toLinearMap ∘ₗ ι Q, fun m => unop_injective <| by simp⟩ + +@[simp] +theorem reverseOp_ι (m : M) : reverseOp (ι Q m) = op (ι Q m) := lift_ι_apply _ _ _ + /-- Grade reversion, inverting the multiplication order of basis vectors. Also called *transpose* in some literature. -/ def reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q := - (opLinearEquiv R).symm.toLinearMap.comp - (CliffordAlgebra.lift Q - ⟨(MulOpposite.opLinearEquiv R).toLinearMap.comp (ι Q), fun m => - unop_injective <| by simp⟩).toLinearMap + (opLinearEquiv R).symm.toLinearMap.comp reverseOp.toLinearMap #align clifford_algebra.reverse CliffordAlgebra.reverse +@[simp] theorem unop_reverseOp (x : CliffordAlgebra Q) : (reverseOp x).unop = reverse x := rfl + +@[simp] theorem op_reverse (x : CliffordAlgebra Q) : op (reverse x) = reverseOp x := rfl + @[simp] theorem reverse_ι (m : M) : reverse (ι Q m) = ι Q m := by simp [reverse] #align clifford_algebra.reverse_ι CliffordAlgebra.reverse_ι @[simp] theorem reverse.commutes (r : R) : - reverse (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := by simp [reverse] + reverse (algebraMap R (CliffordAlgebra Q) r) = algebraMap R _ r := + op_injective <| reverseOp.commutes r #align clifford_algebra.reverse.commutes CliffordAlgebra.reverse.commutes @[simp] -theorem reverse.map_one : reverse (1 : CliffordAlgebra Q) = 1 := by - convert reverse.commutes (Q := Q) (1 : R) <;> simp +theorem reverse.map_one : reverse (1 : CliffordAlgebra Q) = 1 := + op_injective reverseOp.map_one #align clifford_algebra.reverse.map_one CliffordAlgebra.reverse.map_one @[simp] theorem reverse.map_mul (a b : CliffordAlgebra Q) : - -- porting note: can't infer `Q` - reverse (a * b) = reverse b * reverse a := by - simp [reverse] + reverse (a * b) = reverse b * reverse a := + op_injective (reverseOp.map_mul a b) #align clifford_algebra.reverse.map_mul CliffordAlgebra.reverse.map_mul @[simp] @@ -174,7 +183,6 @@ section List /-- Taking the reverse of the product a list of $n$ vectors lifted via `ι` is equivalent to taking the product of the reverse of that list. -/ theorem reverse_prod_map_ι : - -- porting note: can't infer `Q` ∀ l : List M, reverse (l.map <| ι Q).prod = (l.map <| ι Q).reverse.prod | [] => by simp | x::xs => by simp [reverse_prod_map_ι xs] @@ -249,7 +257,8 @@ theorem submodule_map_reverse_eq_comap (p : Submodule R (CliffordAlgebra Q)) : theorem ι_range_map_reverse : (ι Q).range.map (reverse : CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q) = LinearMap.range (ι Q) := by - rw [reverse, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, ← Submodule.map_comp] + rw [reverse, reverseOp, Submodule.map_comp, ι_range_map_lift, LinearMap.range_comp, + ← Submodule.map_comp] exact Submodule.map_id _ #align clifford_algebra.ι_range_map_reverse CliffordAlgebra.ι_range_map_reverse @@ -310,7 +319,6 @@ theorem involute_mem_evenOdd_iff {x : CliffordAlgebra Q} {n : ZMod 2} : @[simp] theorem reverse_mem_evenOdd_iff {x : CliffordAlgebra Q} {n : ZMod 2} : - -- porting note: cannot infer `Q` reverse x ∈ evenOdd Q n ↔ x ∈ evenOdd Q n := SetLike.ext_iff.mp (evenOdd_comap_reverse Q n) x #align clifford_algebra.reverse_mem_even_odd_iff CliffordAlgebra.reverse_mem_evenOdd_iff From f758ce7890c750e2c97131637bf437a0713f18bf Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 13:41:43 +0000 Subject: [PATCH 16/30] docstring --- .../CliffordAlgebra/BaseChange.lean | 21 ++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index d9bc1315cfbe3e..2699f3630bc6ec 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -9,7 +9,26 @@ import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation import Mathlib.LinearAlgebra.TensorProduct.Opposite import Mathlib.RingTheory.TensorProduct -#check 1 +/-! +# The base change of a clifford algebra + +In this file we show the isomorphism + +* `CliffordAlgebra.equivBaseChange A Q` : + `CliffordAlgebra (Q.baseChange A) ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q)` + with forward direction `CliffordAlgebra.toBasechange A Q` and reverse direction + `CliffordAlgebra.ofBasechange A Q`. + +This covers a more general case of §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf, +where ℂ and ℝ are relaced by an `R`-algebra `A`. + +We show: + +* `CliffordAlgebra.toBasechange_ι`: the effect of base-changing pure vectors. +* `CliffordAlgebra.ofBasechange_tmul_ι`: the effect of un-base-changing a tensor of a pure vectors. +* `CliffordAlgebra.toBasechange_involute`: the effect of base-changing an involution. +* `CliffordAlgebra.toBasechange_reverse`: the effect of base-changing a reversal. +-/ variable {R A V : Type*} variable [CommRing R] [CommRing A] [AddCommGroup V] From f678bc87df5f937531b827641acd1e1078126549 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 13:52:01 +0000 Subject: [PATCH 17/30] add AlgHom versions too --- Mathlib/RingTheory/TensorProduct.lean | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index ec57b0a0b2341c..479fd0e2cb2fe1 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -32,7 +32,7 @@ multiplication is characterized by `(a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (a -/ -universe u uS v₁ v₂ v₃ v₄ +universe u uS v₁ v₂ v₃ v₄ v₅ v₆ open scoped TensorProduct @@ -588,10 +588,14 @@ variable {A : Type v₁} [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower variable {B : Type v₂} [Semiring B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] +variable {B' : Type v₅} [Semiring B'] [Algebra R B'] [Algebra S B'] [IsScalarTower R S B'] + variable {C : Type v₃} [Semiring C] [Algebra R C] variable {D : Type v₄} [Semiring D] [Algebra R D] +variable {D' : Type v₆} [Semiring D'] [Algebra R D'] + section variable (R A) @@ -708,6 +712,14 @@ theorem map_tmul (f : A →ₐ[S] B) (g : C →ₐ[R] D) (a : A) (c : C) : map f rfl #align algebra.tensor_product.map_tmul Algebra.TensorProduct.map_tmul +@[simp] +theorem map_id : map (.id S A) (.id R C) = .id S _:= + ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl) + +theorem map_comp (f₂ : B →ₐ[S] B') (f₁ : A →ₐ[S] B) (g₂ : D →ₐ[R] D') (g₁ : C →ₐ[R] D) : + map (f₂.comp f₁) (g₂.comp g₁) = (map f₂ g₂).comp (map f₁ g₁) := + ext (AlgHom.ext fun _ => rfl) (AlgHom.ext fun _ => rfl) + @[simp] theorem map_comp_includeLeft (f : A →ₐ[S] B) (g : C →ₐ[R] D) : (map f g).comp includeLeft = includeLeft.comp f := @@ -757,6 +769,16 @@ theorem congr_symm_apply (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) (x) : rfl #align algebra.tensor_product.congr_symm_apply Algebra.TensorProduct.congr_symm_apply +@[simp] +theorem congr_refl : congr (.refl : A ≃ₐ[S] A) (.refl : C ≃ₐ[R] C) = .refl := + AlgEquiv.coe_algHom_injective <| map_id + +theorem congr_trans (f₁ : A ≃ₐ[S] B) (f₂ : B ≃ₐ[S] B') (g₁ : C ≃ₐ[R] D) (g₂ : D ≃ₐ[R] D') : + congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) := + AlgEquiv.coe_algHom_injective <| map_comp _ _ _ _ + +theorem congr_symm (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) : congr f.symm g.symm = (congr f g).symm := rfl + end end Monoidal From 146896302643707199dc7850236307c4359a4747 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 14:01:32 +0000 Subject: [PATCH 18/30] fix build --- Mathlib/RingTheory/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 479fd0e2cb2fe1..64b333ffdf827d 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -775,7 +775,7 @@ theorem congr_refl : congr (.refl : A ≃ₐ[S] A) (.refl : C ≃ₐ[R] C) = .re theorem congr_trans (f₁ : A ≃ₐ[S] B) (f₂ : B ≃ₐ[S] B') (g₁ : C ≃ₐ[R] D) (g₂ : D ≃ₐ[R] D') : congr (f₁.trans f₂) (g₁.trans g₂) = (congr f₁ g₁).trans (congr f₂ g₂) := - AlgEquiv.coe_algHom_injective <| map_comp _ _ _ _ + AlgEquiv.coe_algHom_injective <| map_comp f₂.toAlgHom f₁.toAlgHom g₂.toAlgHom g₁.toAlgHom theorem congr_symm (f : A ≃ₐ[S] B) (g : C ≃ₐ[R] D) : congr f.symm g.symm = (congr f g).symm := rfl From c97d8351809b0f642f3005839f45a1902d09b7b5 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 25 Aug 2023 14:30:38 +0000 Subject: [PATCH 19/30] partial fix --- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 2699f3630bc6ec..28f786afdb1029 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -178,7 +178,7 @@ theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.bas TensorProduct.map LinearMap.id (reverse (Q := Q)) (toBaseChange A Q x) := by have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x refine (congr_arg unop this).trans ?_; clear this - refine (TensorProduct.AlgebraTensorModule.map_comp_map _ _ _ _ _).trans ?_ + refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_ erw [reverse, AlgHom.toLinearMap_toOpposite, TensorProduct.AlgebraTensorModule.map_apply] From 5e46b50e2497727f21863de3d0375be9883a93eb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 8 Sep 2023 16:00:49 +0000 Subject: [PATCH 20/30] fix docstrings --- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 28f786afdb1029..b964ebcf631e75 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -19,8 +19,9 @@ In this file we show the isomorphism with forward direction `CliffordAlgebra.toBasechange A Q` and reverse direction `CliffordAlgebra.ofBasechange A Q`. -This covers a more general case of §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf, -where ℂ and ℝ are relaced by an `R`-algebra `A`. +This covers a more general case of §2.2 of the complexification of clifford algebras (as described +in https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an +`R`-algebra `A`. We show: From 40489e9386a8bd795585c008a5640eb423989b1a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Tue, 12 Sep 2023 00:31:59 +0000 Subject: [PATCH 21/30] sorry-free but messy --- .../CliffordAlgebra/BaseChange.lean | 42 ++++++------------- .../LinearAlgebra/CliffordAlgebra/Basic.lean | 19 +++++++++ .../LinearAlgebra/QuadraticForm/Basic.lean | 5 +++ .../QuadraticForm/TensorProduct.lean | 16 ++++++- 4 files changed, 52 insertions(+), 30 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index b964ebcf631e75..7f0c8c61a0b866 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -87,27 +87,6 @@ noncomputable def ofBaseChange (Q : QuadraticForm R V) : show z • ofBaseChangeAux A Q 1 = _ rw [map_one, ←Algebra.algebraMap_eq_smul_one] -theorem _root_.CliffordAlgebra.preserves_iff_bilin {R A M} [CommRing R] [Ring A] [Algebra R A] - [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) - (h2 : IsUnit (2 : R)) - (f : M →ₗ[R] A) : - (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔ - ((LinearMap.mul R A).compl₂ f) ∘ₗ f + ((LinearMap.mul R A).flip.compl₂ f) ∘ₗ f = - Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by - simp_rw [FunLike.ext_iff] - dsimp only [LinearMap.compr₂_apply, LinearMap.compl₂_apply, LinearMap.comp_apply, - Algebra.linearMap_apply, LinearMap.mul_apply', BilinForm.toLin_apply, LinearMap.add_apply, - LinearMap.flip_apply] - have h2a := h2.map (algebraMap R A) - refine ⟨fun h x y => ?_, fun h x => ?_⟩ - · rw [QuadraticForm.polarBilin_apply, QuadraticForm.polar, sub_sub, map_sub, map_add, - ←h x, ←h y, ←h (x + y), eq_sub_iff_add_eq, map_add, - add_mul, mul_add, mul_add, add_comm (f x * f x) (f x * f y), - add_add_add_comm] - · apply h2a.mul_left_cancel - simp_rw [←Algebra.smul_def, two_smul] - rw [h x x, QuadraticForm.polarBilin_apply, QuadraticForm.polar_self, two_mul, map_add] - set_option maxHeartbeats 400000 in /-- Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra. -/ @@ -117,17 +96,19 @@ noncomputable def toBaseChange (Q : QuadraticForm R V) : let φ := TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q) refine ⟨φ, ?_⟩ letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm - rw [CliffordAlgebra.preserves_iff_bilin _ (isUnit_of_invertible _)] + letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) := + (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm + rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)] letI : IsScalarTower R A (A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) := LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap refine TensorProduct.AlgebraTensorModule.curry_injective ?_ ext v w change (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) = - QuadraticForm.polar (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 - rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap] - -- QuadraticForm.baseChange_polar_apply, one_mul, one_mul, - -- Algebra.TensorProduct.algebraMap_tmul_one] - sorry + QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 + rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, + QuadraticForm.polarBilin_baseChange, BilinForm.baseChange_tmul, one_mul, + TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one] + rfl @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) : toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v := @@ -180,8 +161,11 @@ theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.bas have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x refine (congr_arg unop this).trans ?_; clear this refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_ - erw [reverse, AlgHom.toLinearMap_toOpposite, - TensorProduct.AlgebraTensorModule.map_apply] + erw [reverse, AlgHom.toLinearMap_toOpposite] + dsimp + simp + rfl + -- rw [TensorProduct.AlgebraTensorModule.map_tmul] attribute [ext] TensorProduct.ext diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index c8e7d240665f04..fa6a1e584e9c38 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -229,6 +229,25 @@ theorem induction {C : CliffordAlgebra Q → Prop} exact Subtype.prop (lift Q of a) #align clifford_algebra.induction CliffordAlgebra.induction +/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible. -/ +theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A)) + (f : M →ₗ[R] A) : + (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔ + ((LinearMap.mul R A).compl₂ f) ∘ₗ f + ((LinearMap.mul R A).flip.compl₂ f) ∘ₗ f = + Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by + simp_rw [FunLike.ext_iff] + dsimp only [LinearMap.compr₂_apply, LinearMap.compl₂_apply, LinearMap.comp_apply, + Algebra.linearMap_apply, LinearMap.mul_apply', BilinForm.toLin_apply, LinearMap.add_apply, + LinearMap.flip_apply] + refine ⟨fun h x y => ?_, fun h x => ?_⟩ + · rw [QuadraticForm.polarBilin_apply, QuadraticForm.polar, sub_sub, map_sub, map_add, + ←h x, ←h y, ←h (x + y), eq_sub_iff_add_eq, map_add, + add_mul, mul_add, mul_add, add_comm (f x * f x) (f x * f y), + add_add_add_comm] + · apply h2.mul_left_cancel + simp_rw [two_mul] + rw [h x x, QuadraticForm.polarBilin_apply, QuadraticForm.polar_self, two_mul, map_add] + /-- The symmetric product of vectors is a scalar -/ theorem ι_mul_ι_add_swap (a b : M) : ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) := diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index f45859791b8deb..dd8f86b859c120 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -792,6 +792,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 +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 diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean index ec9ca8c28c422a..d652ed23ff50c7 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean +++ b/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,19 @@ 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] + erw [associated_sq] + rw [smul_comm (_ : A) (_ : ℕ), ← smul_assoc, two_smul _ (_ : A), invOf_two_add_invOf_two, + one_smul] + end CommRing end QuadraticForm From 6d5d036bf3b66ed20d6ba7b40379ff1419516473 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 13 Sep 2023 20:00:18 +0000 Subject: [PATCH 22/30] style fixes --- .../CliffordAlgebra/BaseChange.lean | 41 +++++++++---------- 1 file changed, 19 insertions(+), 22 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 7f0c8c61a0b866..7d6d2fa0331c01 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -61,13 +61,13 @@ module. -/ noncomputable def ofBaseChange (Q : QuadraticForm R V) : A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) := Algebra.TensorProduct.algHomOfLinearMapTensorProduct - (TensorProduct.AlgebraTensorModule.lift $ + (TensorProduct.AlgebraTensorModule.lift <| let f : A →ₗ[A] _ := (Algebra.lsmul A A (CliffordAlgebra (Q.baseChange A))).toLinearMap - LinearMap.flip $ LinearMap.flip (({ + LinearMap.flip <| LinearMap.flip (({ toFun := fun f : CliffordAlgebra (Q.baseChange A) →ₗ[A] CliffordAlgebra (Q.baseChange A) => LinearMap.restrictScalars R f - map_add' := fun f g => LinearMap.ext $ fun x => rfl - map_smul' := fun (c : A) g => LinearMap.ext $ fun x => rfl + map_add' := fun f g => LinearMap.ext fun x => rfl + map_smul' := fun (c : A) g => LinearMap.ext fun x => rfl } : _ →ₗ[A] _) ∘ₗ f) ∘ₗ (ofBaseChangeAux A Q).toLinearMap) (fun z₁ z₂ b₁ b₂ => show (z₁ * z₂) • ofBaseChangeAux A Q (b₁ * b₂) @@ -136,22 +136,17 @@ open MulOpposite /-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/ theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) : (toBaseChange A Q).op.comp (reverseOp (Q := Q.baseChange A)) = - ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp $ - (Algebra.TensorProduct.map ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q))).comp - (toBaseChange A Q)) := by + ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <| + (Algebra.TensorProduct.map + ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q))).comp + (toBaseChange A Q)) := by ext v - save - dsimp only [TensorProduct.AlgebraTensorModule.curry_apply, AlgHom.comp_toLinearMap, - TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.coe_comp, - Function.comp_apply, AlgHom.toLinearMap_apply, AlgHom.op_apply_apply, AlgEquiv.toAlgHom_eq_coe, - AlgEquiv.toAlgHom_toLinearMap, AlgEquiv.toLinearMap_apply] - -- show - -- op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = - -- Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q) - -- (Algebra.TensorProduct.map ((algHom.id A A).toOpposite Commute.all) (reverseOp Q) - -- (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) - rw [toBaseChange_ι, reverseOp_ι, unop_op, toBaseChange_ι, Algebra.TensorProduct.map_tmul, - Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι, unop_op] + show op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = + Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q) + (Algebra.TensorProduct.map ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q)) + (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) + rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul, + Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι] rfl /-- `reverse` acts only on the right of the tensor product. -/ @@ -165,7 +160,6 @@ theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.bas dsimp simp rfl - -- rw [TensorProduct.AlgebraTensorModule.map_tmul] attribute [ext] TensorProduct.ext @@ -186,7 +180,8 @@ theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) : theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) : (ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _ := by ext x - show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x))) = ι (Q.baseChange A) (1 ⊗ₜ[R] x) + show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x))) + = ι (Q.baseChange A) (1 ⊗ₜ[R] x) rw [toBaseChange_ι, ofBaseChange_tmul_ι] @[simp] theorem ofBaseChange_toBaseChange @@ -195,7 +190,7 @@ theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) : AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q : _) x /-- Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to -base-changing the clifford algebra itself; $Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)$. +base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|. This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/ @[simps!] @@ -204,3 +199,5 @@ noncomputable def equivBaseChange (Q : QuadraticForm R V) : AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q) (toBaseChange_comp_ofBaseChange A Q) (ofBaseChange_comp_toBaseChange A Q) + +end CliffordAlgebra From 08115ab56d28998acfa47208db00df57f37b2323 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 13 Sep 2023 20:26:06 +0000 Subject: [PATCH 23/30] fix Mathlib order --- Mathlib.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib.lean b/Mathlib.lean index 164b5b7e685501..ebcfa0ac928503 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2199,8 +2199,8 @@ import Mathlib.LinearAlgebra.BilinearForm.TensorProduct import Mathlib.LinearAlgebra.BilinearMap import Mathlib.LinearAlgebra.Charpoly.Basic import Mathlib.LinearAlgebra.Charpoly.ToMatrix -import Mathlib.LinearAlgebra.CliffordAlgebra.Basic import Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange +import Mathlib.LinearAlgebra.CliffordAlgebra.Basic import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction import Mathlib.LinearAlgebra.CliffordAlgebra.Equivs From a17529cc670813d7bfb5d8a0151e6eb1cee4178d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Sep 2023 23:19:47 +0000 Subject: [PATCH 24/30] minor statement golf --- .../LinearAlgebra/CliffordAlgebra/BaseChange.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 7d6d2fa0331c01..7a2f197d2ce204 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -135,15 +135,15 @@ open MulOpposite /-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/ theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) : - (toBaseChange A Q).op.comp (reverseOp (Q := Q.baseChange A)) = + (toBaseChange A Q).op.comp (reverseOp) = ((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <| (Algebra.TensorProduct.map - ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q))).comp + (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))).comp (toBaseChange A Q)) := by ext v show op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) = Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q) - (Algebra.TensorProduct.map ((AlgHom.id A A).toOpposite Commute.all) (reverseOp (Q := Q)) + (Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q)) (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul, Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι] @@ -152,12 +152,12 @@ theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) : /-- `reverse` acts only on the right of the tensor product. -/ theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) : toBaseChange A Q (reverse x) = - TensorProduct.map LinearMap.id (reverse (Q := Q)) (toBaseChange A Q x) := by + TensorProduct.map LinearMap.id reverse (toBaseChange A Q x) := by have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x refine (congr_arg unop this).trans ?_; clear this refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_ - erw [reverse, AlgHom.toLinearMap_toOpposite] - dsimp + rw [reverse, ←AlgEquiv.toLinearMap, ←AlgEquiv.toLinearEquiv_toLinearMap, + AlgEquiv.toLinearEquiv_toOpposite] simp rfl From f37187ca2973fc5abf995e1e47475c00d574091e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Sep 2023 23:32:28 +0000 Subject: [PATCH 25/30] golf --- .../LinearAlgebra/CliffordAlgebra/Basic.lean | 39 ++++++++++--------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index d22e872d8c9e4b..672f0b98ae46ce 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -230,35 +230,36 @@ theorem induction {C : CliffordAlgebra Q → Prop} exact Subtype.prop (lift Q of a) #align clifford_algebra.induction CliffordAlgebra.induction -/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible. -/ +theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A] + (f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) : + f a * f b + f b * f a = algebraMap R _ (QuadraticForm.polar Q a b) := + calc + f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by + rw [f.map_add, mul_add, add_mul, add_mul]; abel + _ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by + rw [hf, hf, hf] + _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub] + _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl + +/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible. + +To show a function squares to the quadratic form, it suffices to show that +`f x * f y + f y * f x = algebraMap _ _ (polar Q x y)` -/ theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A)) (f : M →ₗ[R] A) : (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔ ((LinearMap.mul R A).compl₂ f) ∘ₗ f + ((LinearMap.mul R A).flip.compl₂ f) ∘ₗ f = Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by simp_rw [FunLike.ext_iff] - dsimp only [LinearMap.compr₂_apply, LinearMap.compl₂_apply, LinearMap.comp_apply, - Algebra.linearMap_apply, LinearMap.mul_apply', BilinForm.toLin_apply, LinearMap.add_apply, - LinearMap.flip_apply] - refine ⟨fun h x y => ?_, fun h x => ?_⟩ - · rw [QuadraticForm.polarBilin_apply, QuadraticForm.polar, sub_sub, map_sub, map_add, - ←h x, ←h y, ←h (x + y), eq_sub_iff_add_eq, map_add, - add_mul, mul_add, mul_add, add_comm (f x * f x) (f x * f y), - add_add_add_comm] - · apply h2.mul_left_cancel - simp_rw [two_mul] - rw [h x x, QuadraticForm.polarBilin_apply, QuadraticForm.polar_self, two_mul, map_add] + refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩ + change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticForm.polar Q x y) at h + apply h2.mul_left_cancel + rw [two_mul, two_mul, h x x, QuadraticForm.polar_self, two_mul, map_add] /-- The symmetric product of vectors is a scalar -/ theorem ι_mul_ι_add_swap (a b : M) : ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) := - calc - ι Q a * ι Q b + ι Q b * ι Q a = ι Q (a + b) * ι Q (a + b) - ι Q a * ι Q a - ι Q b * ι Q b := by - rw [(ι Q).map_add, mul_add, add_mul, add_mul]; abel - _ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by - rw [ι_sq_scalar, ι_sq_scalar, ι_sq_scalar] - _ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub] - _ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl + mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _ #align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap theorem ι_mul_comm (a b : M) : From 8b34aec7c7d2f35eba25df0fad037d3e310cda55 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Sep 2023 23:46:59 +0000 Subject: [PATCH 26/30] helper lemmas --- .../LinearAlgebra/CliffordAlgebra/Basic.lean | 2 +- .../LinearAlgebra/QuadraticForm/Basic.lean | 20 +++++++++++++------ 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean index 672f0b98ae46ce..9b9eea02676ef0 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean @@ -248,7 +248,7 @@ To show a function squares to the quadratic form, it suffices to show that theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A)) (f : M →ₗ[R] A) : (∀ x, f x * f x = algebraMap _ _ (Q x)) ↔ - ((LinearMap.mul R A).compl₂ f) ∘ₗ f + ((LinearMap.mul R A).flip.compl₂ f) ∘ₗ f = + (LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f = Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by simp_rw [FunLike.ext_iff] refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩ diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 35214ee53b5d2c..4b01f148737817 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -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,19 @@ 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 + +theorem _root_.LinearMap.compQuadraticForm_polarBilin {S : Type*} [CommRing S] [Algebra S R] + [Module S M] [IsScalarTower S R M] (f : R →ₗ[S] S) (Q : QuadraticForm R M) : + (f.compQuadraticForm Q).polarBilin = f.compBilinForm Q.polarBilin := by + ext; simp [polar] + end Ring end BilinForm @@ -810,7 +818,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₁ := From 20e4ec39aa312849b118761bd9648368e8b2d5be Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Sep 2023 23:55:41 +0000 Subject: [PATCH 27/30] golf --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index 4b01f148737817..dbcaecc23564d8 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -779,18 +779,12 @@ 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 := + DistribMulAction.toLinearMap _ _ + (⟨⅟2, fun x => (Commute.ofNat_right x 2).invOf_right⟩ : 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) From 48985e98e9d3a48241b6c1f50343e37397659ec1 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 14 Sep 2023 23:56:59 +0000 Subject: [PATCH 28/30] even more golf --- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean index dbcaecc23564d8..175f6a027f752f 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean @@ -780,11 +780,10 @@ Over a commutative ring, use `QuadraticForm.associated`, which gives an `R`-line 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 := - DistribMulAction.toLinearMap _ _ - (⟨⅟2, fun x => (Commute.ofNat_right x 2).invOf_right⟩ : Submonoid.center R) ∘ₗ - { toFun := polarBilin - map_add' := fun _x _y => BilinForm.ext <| polar_add _ _ - map_smul' := fun _c _x => BilinForm.ext <| polar_smul _ _ } + (⟨⅟2, fun x => (Commute.ofNat_right x 2).invOf_right⟩ : 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) From 9e292261f8de161f25d431929eef25764045485e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 16 Sep 2023 17:24:33 +0000 Subject: [PATCH 29/30] golf slightly, and make more readable --- .../CliffordAlgebra/BaseChange.lean | 35 +++++++++---------- 1 file changed, 17 insertions(+), 18 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index 7a2f197d2ce204..f9df13c672393b 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -23,7 +23,7 @@ This covers a more general case of §2.2 of the complexification of clifford alg in https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an `R`-algebra `A`. -We show: +We show the additional results: * `CliffordAlgebra.toBasechange_ι`: the effect of base-changing pure vectors. * `CliffordAlgebra.ofBasechange_tmul_ι`: the effect of un-base-changing a tensor of a pure vectors. @@ -44,7 +44,7 @@ namespace CliffordAlgebra variable (A) /-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/ -noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) : +def ofBaseChangeAux (Q : QuadraticForm R V) : CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) := CliffordAlgebra.lift Q <| by refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩ @@ -58,7 +58,7 @@ noncomputable def ofBaseChangeAux (Q : QuadraticForm R V) : /-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed module. -/ -noncomputable def ofBaseChange (Q : QuadraticForm R V) : +def ofBaseChange (Q : QuadraticForm R V) : A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) := Algebra.TensorProduct.algHomOfLinearMapTensorProduct (TensorProduct.AlgebraTensorModule.lift <| @@ -87,28 +87,27 @@ noncomputable def ofBaseChange (Q : QuadraticForm R V) : show z • ofBaseChangeAux A Q 1 = _ rw [map_one, ←Algebra.algebraMap_eq_smul_one] -set_option maxHeartbeats 400000 in /-- Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra. -/ -noncomputable def toBaseChange (Q : QuadraticForm R V) : +def toBaseChange (Q : QuadraticForm R V) : CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q := CliffordAlgebra.lift _ <| by - let φ := TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q) - refine ⟨φ, ?_⟩ + refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩ letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) := - (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm - rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)] - letI : IsScalarTower R A (A ⊗[R] V →ₗ[A] A ⊗[R] CliffordAlgebra Q) := - LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap - refine TensorProduct.AlgebraTensorModule.curry_injective ?_ - ext v w - change (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) = - QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 + (Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm + suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) = + QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by + -- the crux is that by converting to a statement about linear maps instead of quadratic forms, + -- we then have access to all the partially-applied `ext` lemmas. + rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)] + refine TensorProduct.AlgebraTensorModule.curry_injective ?_ + ext v w + exact hpure_tensor v w + intros v w rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap, QuadraticForm.polarBilin_baseChange, BilinForm.baseChange_tmul, one_mul, - TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one] - rfl + TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply] @[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) : toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v := @@ -194,7 +193,7 @@ base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R C This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/ @[simps!] -noncomputable def equivBaseChange (Q : QuadraticForm R V) : +def equivBaseChange (Q : QuadraticForm R V) : CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q := AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q) (toBaseChange_comp_ofBaseChange A Q) From 8467a30225ba09ba2067c00ab1ad2984507402ee Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Sat, 16 Sep 2023 17:29:51 +0000 Subject: [PATCH 30/30] fix docstring --- Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean index f9df13c672393b..ee26f754e4e311 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean @@ -19,9 +19,9 @@ In this file we show the isomorphism with forward direction `CliffordAlgebra.toBasechange A Q` and reverse direction `CliffordAlgebra.ofBasechange A Q`. -This covers a more general case of §2.2 of the complexification of clifford algebras (as described -in https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an -`R`-algebra `A`. +This covers a more general case of the complexification of clifford algebras (as described in §2.2 +of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an +`R`-algebra `A` (where `2 : R` is invertible). We show the additional results: @@ -38,7 +38,6 @@ variable [Invertible (2 : R)] open scoped TensorProduct - namespace CliffordAlgebra variable (A)