Complexification of a clifford algebra #

In this file we show the isomorphism

clifford_algebra.equiv_complexify Q : clifford_algebra Q.complexify ≃ₐ[ℂ] (ℂ ⊗[ℝ] clifford_algebra Q) with forward direction clifford_algebra.to_complexify Q and reverse direction clifford_algebra.of_complexify Q.

where

quadratic_form.complexify Q : quadratic_form ℂ (ℂ ⊗[ℝ] V), which is defined in terms of a more general quadratic_form.base_change.

This covers §2.2 of https://empg.maths.ed.ac.uk/Activities/Spin/Lecture2.pdf.

We show:

clifford_algebra.to_complexify_ι: the effect of complexifying pure vectors.
clifford_algebra.of_complexify_tmul_ι: the effect of un-complexifying a tensor of pure vectors.
clifford_algebra.to_complexify_involute: the effect of complexifying an involution.
clifford_algebra.to_complexify_reverse: the effect of complexifying a reversal.

Note that all the results in this file are already in Mathlib4 due to https://github.com/leanprover-community/mathlib4/pull/6778.

source

def quadratic_form.base_change {R : Type uR} (A : Type uA) {V : Type uV} [comm_ring R] [comm_ring A] [algebra R A] [invertible 2] [add_comm_group V] [module R V] (Q : quadratic_form R V) :

quadratic_form A (tensor_product R A V)

Change the base of a quadratic form, defined by $Q_A(a ⊗_R v) = a^2Q(v)$.

Equations

quadratic_form.base_change A Q = ((⇑linear_map.to_bilin (linear_map.mul A A)).tmul' (⇑quadratic_form.associated Q)).to_quadratic_form

source

@[simp]

theorem quadratic_form.base_change_apply {R : Type uR} {A : Type uA} {V : Type uV} [comm_ring R] [comm_ring A] [algebra R A] [invertible 2] [add_comm_group V] [module R V] (Q : quadratic_form R V) (c : A) (v : V) :

⇑(quadratic_form.base_change A Q) (c ⊗ₜ[R] v) = c * c * ⇑(algebra_map R A) (⇑Q v)

source

theorem quadratic_form.base_change.polar_bilin {R : Type uR} (A : Type uA) {V : Type uV} [comm_ring R] [comm_ring A] [algebra R A] [invertible 2] [add_comm_group V] [module R V] (Q : quadratic_form R V) :

(quadratic_form.base_change A Q).polar_bilin = (⇑linear_map.to_bilin (linear_map.mul A A)).tmul' Q.polar_bilin

source

@[simp]

theorem quadratic_form.base_change_polar_apply {R : Type uR} (A : Type uA) {V : Type uV} [comm_ring R] [comm_ring A] [algebra R A] [invertible 2] [add_comm_group V] [module R V] (Q : quadratic_form R V) (c₁ : A) (v₁ : V) (c₂ : A) (v₂ : V) :

quadratic_form.polar ⇑(quadratic_form.base_change A Q) (c₁ ⊗ₜ[R] v₁) (c₂ ⊗ₜ[R] v₂) = c₁ * c₂ * ⇑(algebra_map R A) (quadratic_form.polar ⇑Q v₁ v₂)

source

@[reducible]

noncomputable def quadratic_form.complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

quadratic_form ℂ (tensor_product ℝ ℂ V)

The complexification of a quadratic form, defined by $Q_ℂ(z ⊗ v) = z^2Q(v)$.

Equations

Q.complexify = quadratic_form.base_change ℂ Q

source

@[protected, instance]

def free_algebra.algebra' {V : Type uV} [add_comm_group V] [module ℝ V] :

algebra ℝ (free_algebra ℂ (tensor_product ℝ ℂ V))

Equations

free_algebra.algebra' = restrict_scalars.algebra ℝ ℂ (free_algebra ℂ (tensor_product ℝ ℂ V))

source

@[protected, instance]

def tensor_algebra.algebra' {V : Type uV} [add_comm_group V] [module ℝ V] :

algebra ℝ (tensor_algebra ℂ (tensor_product ℝ ℂ V))

Equations

tensor_algebra.algebra' = ring_quot.algebra (tensor_algebra.rel ℂ (tensor_product ℝ ℂ V))

source

@[protected, instance]

def tensor_algebra.is_scalar_tower' {V : Type uV} [add_comm_group V] [module ℝ V] :

is_scalar_tower ℝ ℂ (tensor_algebra ℂ (tensor_product ℝ ℂ V))

source

@[protected, instance]

def clifford_algebra.algebra' {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

algebra ℝ (clifford_algebra Q.complexify)

Equations

clifford_algebra.algebra' Q = ring_quot.algebra (clifford_algebra.rel Q.complexify)

source

@[protected, instance]

def clifford_algebra.is_scalar_tower {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

is_scalar_tower ℝ ℂ (clifford_algebra Q.complexify)

source

@[protected, instance]

def clifford_algebra.smul_comm_class {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

smul_comm_class ℝ ℂ (clifford_algebra Q.complexify)

source

@[protected, instance]

def clifford_algebra.smul_comm_class' {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

smul_comm_class ℂ ℝ (clifford_algebra Q.complexify)

source

noncomputable def clifford_algebra.of_complexify_aux {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

clifford_algebra Q →ₐ[ℝ ] clifford_algebra Q.complexify

Auxiliary construction: note this is really just a heterobasic clifford_algebra.map.

Equations

clifford_algebra.of_complexify_aux Q = ⇑(clifford_algebra.lift Q) ⟨(linear_map.restrict_scalars ℝ (clifford_algebra.ι Q.complexify)).comp (⇑(tensor_product.mk ℝ ℂ V) 1), _⟩

source

@[simp]

theorem clifford_algebra.of_complexify_aux_ι {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (v : V) :

⇑(clifford_algebra.of_complexify_aux Q) (⇑(clifford_algebra.ι Q) v) = ⇑(clifford_algebra.ι Q.complexify) (1 ⊗ₜ[ℝ ] v)

source

noncomputable def clifford_algebra.of_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

tensor_product ℝ ℂ (clifford_algebra Q) →ₐ[ℂ ] clifford_algebra Q.complexify

Convert from the complexified clifford algebra to the clifford algebra over a complexified module.

Equations

clifford_algebra.of_complexify Q = algebra.tensor_product.alg_hom_of_linear_map_tensor_product' (tensor_product.algebra_tensor_module.lift (let f : ℂ →ₗ[ℂ ] module.End ℂ (clifford_algebra Q.complexify) := (algebra.lsmul ℂ (clifford_algebra Q.complexify)).to_linear_map in (({to_fun := λ (f : clifford_algebra Q.complexify →ₗ[ℂ ] clifford_algebra Q.complexify), linear_map.restrict_scalars ℝ f, map_add' := _, map_smul' := _}.comp f).flip.comp (clifford_algebra.of_complexify_aux Q).to_linear_map).flip)) _ _

source

@[simp]

theorem clifford_algebra.of_complexify_tmul_ι {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (z : ℂ) (v : V) :

⇑(clifford_algebra.of_complexify Q) (z ⊗ₜ[ℝ ] ⇑(clifford_algebra.ι Q) v) = ⇑(clifford_algebra.ι Q.complexify) (z ⊗ₜ[ℝ ] v)

source

@[simp]

theorem clifford_algebra.of_complexify_tmul_one {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (z : ℂ) :

⇑(clifford_algebra.of_complexify Q) (z ⊗ₜ[ℝ ] 1) = ⇑(algebra_map ℂ (clifford_algebra Q.complexify)) z

source

noncomputable def clifford_algebra.to_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

clifford_algebra Q.complexify →ₐ[ℂ ] tensor_product ℝ ℂ (clifford_algebra Q)

Convert from the clifford algebra over a complexified module to the complexified clifford algebra.

Equations

clifford_algebra.to_complexify Q = ⇑(clifford_algebra.lift Q.complexify) (let φ : tensor_product ℝ ℂ V →ₗ[ℂ ] tensor_product ℝ ℂ (clifford_algebra Q) := tensor_product.algebra_tensor_module.map linear_map.id (clifford_algebra.ι Q) in ⟨φ, _⟩)

source

@[simp]

theorem clifford_algebra.to_complexify_ι {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (z : ℂ) (v : V) :

⇑(clifford_algebra.to_complexify Q) (⇑(clifford_algebra.ι Q.complexify) (z ⊗ₜ[ℝ ] v)) = z ⊗ₜ[ℝ ] ⇑(clifford_algebra.ι Q) v

source

theorem clifford_algebra.to_complexify_comp_involute {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

(clifford_algebra.to_complexify Q).comp clifford_algebra.involute = (algebra.tensor_product.map' (alg_hom.id ℂ ℂ) clifford_algebra.involute).comp (clifford_algebra.to_complexify Q)

source

theorem clifford_algebra.to_complexify_involute {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) :

⇑(clifford_algebra.to_complexify Q) (⇑clifford_algebra.involute x) = ⇑(tensor_product.map linear_map.id clifford_algebra.involute.to_linear_map) (⇑(clifford_algebra.to_complexify Q) x)

The involution acts only on the right of the tensor product.

source

Auxiliary lemma used to prove to_complexify_reverse without needing induction.

source

theorem clifford_algebra.to_complexify_reverse {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) :

⇑(clifford_algebra.to_complexify Q) (⇑clifford_algebra.reverse x) = ⇑(tensor_product.map linear_map.id clifford_algebra.reverse) (⇑(clifford_algebra.to_complexify Q) x)

reverse acts only on the right of the tensor product.

source

theorem clifford_algebra.to_complexify_comp_of_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

(clifford_algebra.to_complexify Q).comp (clifford_algebra.of_complexify Q) = alg_hom.id ℂ (tensor_product ℝ ℂ (clifford_algebra Q))

source

@[simp]

theorem clifford_algebra.to_complexify_of_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (x : tensor_product ℝ ℂ (clifford_algebra Q)) :

⇑(clifford_algebra.to_complexify Q) (⇑(clifford_algebra.of_complexify Q) x) = x

source

theorem clifford_algebra.of_complexify_comp_to_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

(clifford_algebra.of_complexify Q).comp (clifford_algebra.to_complexify Q) = alg_hom.id ℂ (clifford_algebra Q.complexify)

source

@[simp]

theorem clifford_algebra.of_complexify_to_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (x : clifford_algebra Q.complexify) :

⇑(clifford_algebra.of_complexify Q) (⇑(clifford_algebra.to_complexify Q) x) = x

source

@[simp]

theorem clifford_algebra.equiv_complexify_apply {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (ᾰ : clifford_algebra Q.complexify) :

⇑(clifford_algebra.equiv_complexify Q) ᾰ = ⇑(clifford_algebra.to_complexify Q) ᾰ

source

noncomputable def clifford_algebra.equiv_complexify {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) :

clifford_algebra Q.complexify ≃ₐ[ℂ ] tensor_product ℝ ℂ (clifford_algebra Q)

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 clifford_algebra.to_complexify and clifford_algebra.of_complexify as an equivalence.

Equations

clifford_algebra.equiv_complexify Q = alg_equiv.of_alg_hom (clifford_algebra.to_complexify Q) (clifford_algebra.of_complexify Q) _ _

source

@[simp]

theorem clifford_algebra.equiv_complexify_symm_apply {V : Type uV} [add_comm_group V] [module ℝ V] (Q : quadratic_form ℝ V) (ᾰ : tensor_product ℝ ℂ (clifford_algebra Q)) :

⇑((clifford_algebra.equiv_complexify Q).symm) ᾰ = ⇑(clifford_algebra.of_complexify Q) ᾰ