Skip to content

Commit eec55af

Browse files
eric-wiesereric-wieser
committed
feat: base change of Clifford algebras (#6778)
The main result here is `CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q`; that is, the `A ⊗[R]` can be moved from `_ : QuadraticForm A (A ⊗[R] _)` to the outside and vice versa.
1 parent 2cd05f0 commit eec55af

3 files changed

Lines changed: 228 additions & 6 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2213,6 +2213,7 @@ import Mathlib.LinearAlgebra.BilinearForm.TensorProduct
22132213
import Mathlib.LinearAlgebra.BilinearMap
22142214
import Mathlib.LinearAlgebra.Charpoly.Basic
22152215
import Mathlib.LinearAlgebra.Charpoly.ToMatrix
2216+
import Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
22162217
import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
22172218
import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
22182219
import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

‎Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean‎

Lines changed: 201 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,201 @@
1+
/-
2+
Copyright (c) 2023 Eric Wieser. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Eric Wieser
5+
-/
6+
import Mathlib.Data.Complex.Module
7+
import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
8+
import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
9+
import Mathlib.LinearAlgebra.TensorProduct.Opposite
10+
import Mathlib.RingTheory.TensorProduct
11+
12+
/-!
13+
# The base change of a clifford algebra
14+
15+
In this file we show the isomorphism
16+
17+
* `CliffordAlgebra.equivBaseChange A Q` :
18+
`CliffordAlgebra (Q.baseChange A) ≃ₐ[A] (A ⊗[R] CliffordAlgebra Q)`
19+
with forward direction `CliffordAlgebra.toBasechange A Q` and reverse direction
20+
`CliffordAlgebra.ofBasechange A Q`.
21+
22+
This covers a more general case of the complexification of clifford algebras (as described in §2.2
23+
of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf), where ℂ and ℝ are replaced by an
24+
`R`-algebra `A` (where `2 : R` is invertible).
25+
26+
We show the additional results:
27+
28+
* `CliffordAlgebra.toBasechange_ι`: the effect of base-changing pure vectors.
29+
* `CliffordAlgebra.ofBasechange_tmul_ι`: the effect of un-base-changing a tensor of a pure vectors.
30+
* `CliffordAlgebra.toBasechange_involute`: the effect of base-changing an involution.
31+
* `CliffordAlgebra.toBasechange_reverse`: the effect of base-changing a reversal.
32+
-/
33+
34+
variable {R A V : Type*}
35+
variable [CommRing R] [CommRing A] [AddCommGroup V]
36+
variable [Algebra R A] [Module R V] [Module A V] [IsScalarTower R A V]
37+
variable [Invertible (2 : R)]
38+
39+
open scoped TensorProduct
40+
41+
namespace CliffordAlgebra
42+
43+
variable (A)
44+
45+
/-- Auxiliary construction: note this is really just a heterobasic `CliffordAlgebra.map`. -/
46+
def ofBaseChangeAux (Q : QuadraticForm R V) :
47+
CliffordAlgebra Q →ₐ[R] CliffordAlgebra (Q.baseChange A) :=
48+
CliffordAlgebra.lift Q <| by
49+
refine ⟨(ι (Q.baseChange A)).restrictScalars R ∘ₗ TensorProduct.mk R A V 1, fun v => ?_⟩
50+
refine (CliffordAlgebra.ι_sq_scalar (Q.baseChange A) (1 ⊗ₜ v)).trans ?_
51+
rw [QuadraticForm.baseChange_tmul, one_mul, ←Algebra.algebraMap_eq_smul_one,
52+
←IsScalarTower.algebraMap_apply]
53+
54+
@[simp] theorem ofBaseChangeAux_ι (Q : QuadraticForm R V) (v : V) :
55+
ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (1 ⊗ₜ v) :=
56+
CliffordAlgebra.lift_ι_apply _ _ v
57+
58+
/-- Convert from the base-changed clifford algebra to the clifford algebra over a base-changed
59+
module. -/
60+
def ofBaseChange (Q : QuadraticForm R V) :
61+
A ⊗[R] CliffordAlgebra Q →ₐ[A] CliffordAlgebra (Q.baseChange A) :=
62+
Algebra.TensorProduct.algHomOfLinearMapTensorProduct
63+
(TensorProduct.AlgebraTensorModule.lift <|
64+
let f : A →ₗ[A] _ := (Algebra.lsmul A A (CliffordAlgebra (Q.baseChange A))).toLinearMap
65+
LinearMap.flip <| LinearMap.flip (({
66+
toFun := fun f : CliffordAlgebra (Q.baseChange A) →ₗ[A] CliffordAlgebra (Q.baseChange A) =>
67+
LinearMap.restrictScalars R f
68+
map_add' := fun f g => LinearMap.ext fun x => rfl
69+
map_smul' := fun (c : A) g => LinearMap.ext fun x => rfl
70+
} : _ →ₗ[A] _) ∘ₗ f) ∘ₗ (ofBaseChangeAux A Q).toLinearMap)
71+
(fun z₁ z₂ b₁ b₂ =>
72+
show (z₁ * z₂) • ofBaseChangeAux A Q (b₁ * b₂)
73+
= z₁ • ofBaseChangeAux A Q b₁ * z₂ • ofBaseChangeAux A Q b₂
74+
by rw [map_mul, smul_mul_smul])
75+
(fun r =>
76+
show r • ofBaseChangeAux A Q 1 = algebraMap A (CliffordAlgebra (Q.baseChange A)) r
77+
by rw [map_one, Algebra.algebraMap_eq_smul_one])
78+
79+
@[simp] theorem ofBaseChange_tmul_ι (Q : QuadraticForm R V) (z : A) (v : V) :
80+
ofBaseChange A Q (z ⊗ₜ ι Q v) = ι (Q.baseChange A) (z ⊗ₜ v) := by
81+
show z • ofBaseChangeAux A Q (ι Q v) = ι (Q.baseChange A) (z ⊗ₜ[R] v)
82+
rw [ofBaseChangeAux_ι, ←map_smul, TensorProduct.smul_tmul', smul_eq_mul, mul_one]
83+
84+
@[simp] theorem ofBaseChange_tmul_one (Q : QuadraticForm R V) (z : A) :
85+
ofBaseChange A Q (z ⊗ₜ 1) = algebraMap _ _ z := by
86+
show z • ofBaseChangeAux A Q 1 = _
87+
rw [map_one, ←Algebra.algebraMap_eq_smul_one]
88+
89+
/-- Convert from the clifford algebra over a base-changed module to the base-changed clifford
90+
algebra. -/
91+
def toBaseChange (Q : QuadraticForm R V) :
92+
CliffordAlgebra (Q.baseChange A) →ₐ[A] A ⊗[R] CliffordAlgebra Q :=
93+
CliffordAlgebra.lift _ <| by
94+
refine ⟨TensorProduct.AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) (ι Q), ?_⟩
95+
letI : Invertible (2 : A) := (Invertible.map (algebraMap R A) 2).copy 2 (map_ofNat _ _).symm
96+
letI : Invertible (2 : A ⊗[R] CliffordAlgebra Q) :=
97+
(Invertible.map (algebraMap R _) 2).copy 2 (map_ofNat _ _).symm
98+
suffices hpure_tensor : ∀ v w, (1 * 1) ⊗ₜ[R] (ι Q v * ι Q w) + (1 * 1) ⊗ₜ[R] (ι Q w * ι Q v) =
99+
QuadraticForm.polarBilin (Q.baseChange A) (1 ⊗ₜ[R] v) (1 ⊗ₜ[R] w) ⊗ₜ[R] 1 by
100+
-- the crux is that by converting to a statement about linear maps instead of quadratic forms,
101+
-- we then have access to all the partially-applied `ext` lemmas.
102+
rw [CliffordAlgebra.forall_mul_self_eq_iff (isUnit_of_invertible _)]
103+
refine TensorProduct.AlgebraTensorModule.curry_injective ?_
104+
ext v w
105+
exact hpure_tensor v w
106+
intros v w
107+
rw [← TensorProduct.tmul_add, CliffordAlgebra.ι_mul_ι_add_swap,
108+
QuadraticForm.polarBilin_baseChange, BilinForm.baseChange_tmul, one_mul,
109+
TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one, QuadraticForm.polarBilin_apply]
110+
111+
@[simp] theorem toBaseChange_ι (Q : QuadraticForm R V) (z : A) (v : V) :
112+
toBaseChange A Q (ι (Q.baseChange A) (z ⊗ₜ v)) = z ⊗ₜ ι Q v :=
113+
CliffordAlgebra.lift_ι_apply _ _ _
114+
115+
theorem toBaseChange_comp_involute (Q : QuadraticForm R V) :
116+
(toBaseChange A Q).comp (involute : CliffordAlgebra (Q.baseChange A) →ₐ[A] _) =
117+
(Algebra.TensorProduct.map (AlgHom.id _ _) involute).comp (toBaseChange A Q) := by
118+
ext v
119+
show toBaseChange A Q (involute (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
120+
= (Algebra.TensorProduct.map (AlgHom.id _ _) involute :
121+
A ⊗[R] CliffordAlgebra Q →ₐ[A] _)
122+
(toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))
123+
rw [toBaseChange_ι, involute_ι, map_neg (toBaseChange A Q), toBaseChange_ι,
124+
Algebra.TensorProduct.map_tmul, AlgHom.id_apply, involute_ι, TensorProduct.tmul_neg]
125+
126+
/-- The involution acts only on the right of the tensor product. -/
127+
theorem toBaseChange_involute (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
128+
toBaseChange A Q (involute x) =
129+
TensorProduct.map LinearMap.id (involute.toLinearMap) (toBaseChange A Q x) :=
130+
FunLike.congr_fun (toBaseChange_comp_involute A Q) x
131+
132+
open MulOpposite
133+
134+
/-- Auxiliary theorem used to prove `toBaseChange_reverse` without needing induction. -/
135+
theorem toBaseChange_comp_reverseOp (Q : QuadraticForm R V) :
136+
(toBaseChange A Q).op.comp (reverseOp) =
137+
((Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)).toAlgHom.comp <|
138+
(Algebra.TensorProduct.map
139+
(AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))).comp
140+
(toBaseChange A Q)) := by
141+
ext v
142+
show op (toBaseChange A Q (reverse (ι (Q.baseChange A) (1 ⊗ₜ[R] v)))) =
143+
Algebra.TensorProduct.opAlgEquiv R A A (CliffordAlgebra Q)
144+
(Algebra.TensorProduct.map (AlgEquiv.toOpposite A A).toAlgHom (reverseOp (Q := Q))
145+
(toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] v))))
146+
rw [toBaseChange_ι, reverse_ι, toBaseChange_ι, Algebra.TensorProduct.map_tmul,
147+
Algebra.TensorProduct.opAlgEquiv_tmul, reverseOp_ι]
148+
rfl
149+
150+
/-- `reverse` acts only on the right of the tensor product. -/
151+
theorem toBaseChange_reverse (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
152+
toBaseChange A Q (reverse x) =
153+
TensorProduct.map LinearMap.id reverse (toBaseChange A Q x) := by
154+
have := FunLike.congr_fun (toBaseChange_comp_reverseOp A Q) x
155+
refine (congr_arg unop this).trans ?_; clear this
156+
refine (LinearMap.congr_fun (TensorProduct.AlgebraTensorModule.map_comp _ _ _ _).symm _).trans ?_
157+
rw [reverse, ←AlgEquiv.toLinearMap, ←AlgEquiv.toLinearEquiv_toLinearMap,
158+
AlgEquiv.toLinearEquiv_toOpposite]
159+
simp
160+
rfl
161+
162+
attribute [ext] TensorProduct.ext
163+
164+
theorem toBaseChange_comp_ofBaseChange (Q : QuadraticForm R V) :
165+
(toBaseChange A Q).comp (ofBaseChange A Q) = AlgHom.id _ _ := by
166+
ext z : 2
167+
· change toBaseChange A Q (ofBaseChange A Q (z ⊗ₜ[R] 1)) = z ⊗ₜ[R] 1
168+
rw [ofBaseChange_tmul_one, AlgHom.commutes, Algebra.TensorProduct.algebraMap_apply,
169+
Algebra.id.map_eq_self]
170+
· ext v : 1
171+
change toBaseChange A Q (ofBaseChange A Q (1 ⊗ₜ[R] ι Q v)) = 1 ⊗ₜ[R] ι Q v
172+
rw [ofBaseChange_tmul_ι, toBaseChange_ι]
173+
174+
@[simp] theorem toBaseChange_ofBaseChange (Q : QuadraticForm R V) (x : A ⊗[R] CliffordAlgebra Q) :
175+
toBaseChange A Q (ofBaseChange A Q x) = x :=
176+
AlgHom.congr_fun (toBaseChange_comp_ofBaseChange A Q : _) x
177+
178+
theorem ofBaseChange_comp_toBaseChange (Q : QuadraticForm R V) :
179+
(ofBaseChange A Q).comp (toBaseChange A Q) = AlgHom.id _ _ := by
180+
ext x
181+
show ofBaseChange A Q (toBaseChange A Q (ι (Q.baseChange A) (1 ⊗ₜ[R] x)))
182+
= ι (Q.baseChange A) (1 ⊗ₜ[R] x)
183+
rw [toBaseChange_ι, ofBaseChange_tmul_ι]
184+
185+
@[simp] theorem ofBaseChange_toBaseChange
186+
(Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
187+
ofBaseChange A Q (toBaseChange A Q x) = x :=
188+
AlgHom.congr_fun (ofBaseChange_comp_toBaseChange A Q : _) x
189+
190+
/-- Base-changing the vector space of a clifford algebra is isomorphic as an A-algebra to
191+
base-changing the clifford algebra itself; <|Cℓ(A ⊗_R V, Q_A) ≅ A ⊗_R Cℓ(V, Q)<|.
192+
193+
This is `CliffordAlgebra.toBaseChange` and `CliffordAlgebra.ofBaseChange` as an equivalence. -/
194+
@[simps!]
195+
def equivBaseChange (Q : QuadraticForm R V) :
196+
CliffordAlgebra (Q.baseChange A) ≃ₐ[A] A ⊗[R] CliffordAlgebra Q :=
197+
AlgEquiv.ofAlgHom (toBaseChange A Q) (ofBaseChange A Q)
198+
(toBaseChange_comp_ofBaseChange A Q)
199+
(ofBaseChange_comp_toBaseChange A Q)
200+
201+
end CliffordAlgebra

‎Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean‎

Lines changed: 26 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -230,16 +230,36 @@ theorem induction {C : CliffordAlgebra Q → Prop}
230230
exact Subtype.prop (lift Q of a)
231231
#align clifford_algebra.induction CliffordAlgebra.induction
232232

233-
/-- The symmetric product of vectors is a scalar -/
234-
theorem ι_mul_ι_add_swap (a b : M) :
235-
ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
233+
theorem mul_add_swap_eq_polar_of_forall_mul_self_eq {A : Type*} [Ring A] [Algebra R A]
234+
(f : M →ₗ[R] A) (hf : ∀ x, f x * f x = algebraMap _ _ (Q x)) (a b : M) :
235+
f a * f b + f b * f a = algebraMap R _ (QuadraticForm.polar Q a b) :=
236236
calc
237-
ι Q a * ι Q b + ι Q b * ι Q a = ι Q (a + b) * ι Q (a + b) - ι Q a * ι Q a - ι Q b * ι Q b := by
238-
rw [(ι Q).map_add, mul_add, add_mul, add_mul]; abel
237+
f a * f b + f b * f a = f (a + b) * f (a + b) - f a * f a - f b * f b := by
238+
rw [f.map_add, mul_add, add_mul, add_mul]; abel
239239
_ = algebraMap R _ (Q (a + b)) - algebraMap R _ (Q a) - algebraMap R _ (Q b) := by
240-
rw [ι_sq_scalar, ι_sq_scalar, ι_sq_scalar]
240+
rw [hf, hf, hf]
241241
_ = algebraMap R _ (Q (a + b) - Q a - Q b) := by rw [← RingHom.map_sub, ← RingHom.map_sub]
242242
_ = algebraMap R _ (QuadraticForm.polar Q a b) := rfl
243+
244+
/-- An alternative way to provide the argument to `CliffordAlgebra.lift` when `2` is invertible.
245+
246+
To show a function squares to the quadratic form, it suffices to show that
247+
`f x * f y + f y * f x = algebraMap _ _ (polar Q x y)` -/
248+
theorem forall_mul_self_eq_iff {A : Type*} [Ring A] [Algebra R A] (h2 : IsUnit (2 : A))
249+
(f : M →ₗ[R] A) :
250+
(∀ x, f x * f x = algebraMap _ _ (Q x)) ↔
251+
(LinearMap.mul R A).compl₂ f ∘ₗ f + (LinearMap.mul R A).flip.compl₂ f ∘ₗ f =
252+
Q.polarBilin.toLin.compr₂ (Algebra.linearMap R A) := by
253+
simp_rw [FunLike.ext_iff]
254+
refine ⟨mul_add_swap_eq_polar_of_forall_mul_self_eq _, fun h x => ?_⟩
255+
change ∀ x y : M, f x * f y + f y * f x = algebraMap R A (QuadraticForm.polar Q x y) at h
256+
apply h2.mul_left_cancel
257+
rw [two_mul, two_mul, h x x, QuadraticForm.polar_self, two_mul, map_add]
258+
259+
/-- The symmetric product of vectors is a scalar -/
260+
theorem ι_mul_ι_add_swap (a b : M) :
261+
ι Q a * ι Q b + ι Q b * ι Q a = algebraMap R _ (QuadraticForm.polar Q a b) :=
262+
mul_add_swap_eq_polar_of_forall_mul_self_eq _ (ι_sq_scalar _) _ _
243263
#align clifford_algebra.ι_mul_ι_add_swap CliffordAlgebra.ι_mul_ι_add_swap
244264

245265
theorem ι_mul_comm (a b : M) :

0 commit comments

Comments
 (0)