The normalized Fock action of a complex structure

Let Q be a nondegenerate quadratic form on a finite-dimensional real vector space V and J an almost complex structure preserving Q. The i-eigenspace W of the complexified complex structure and the -i-eigenspace W' polarize Q.baseChange ℂ (TauCeti.AlmostComplexStructure.spinPolarizationData), so TauCeti.spinAction makes ⋀ W a module over the complexified Clifford algebra. On a real vector v, with 1 ⊗ v = v^(1,0) + v^(0,1), this native action is exterior multiplication by v^(1,0) plus contraction against the polar form QuadraticMap.polar (Q.baseChange ℂ) · v^(0,1).

In the geometric convention Q (v) = -g (v, v) for a metric g, the polar form is -2 g_ℂ, so the native action is ε(v^(1,0)) - 2 ι(v^(0,1)), where ι contracts against g_ℂ. Its two halves carry different factors. Conjugating by the degree scaling T of ⋀ W by √2, which acts on ⋀^p W by √2 ^ p = 2 ^ (p / 2), gives the √2-normalized Fock action c(v) = √2 (ε(v^(1,0)) - ι(v^(0,1))), in which both halves carry the factor √2. This file defines that action and proves the intertwining equation T ∘ spinAction a = fockAction a ∘ T together with the formula for c(v).

Main definitions

• TauCeti.AlmostComplexStructure.fockAction: the √2-normalized Fock action.
• TauCeti.AlmostComplexStructure.realFockAction: its restriction to the real Clifford algebra CliffordAlgebra Q, making ⋀ W a complex Clifford module of the real space (V, Q).

Main results

• TauCeti.AlmostComplexStructure.spinAction_ι_one_tmul: the native action of a real vector.
• TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp: the degree scaling by √2 intertwines the native action with the normalized one.
• TauCeti.AlmostComplexStructure.fockAction_bijective: the normalized action is an isomorphism onto the endomorphisms of ⋀ W.
• TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul: the normalized action of a real vector, c(v) = √2 (ε(v^(1,0)) + (1/2) · contraction against polar (Q.baseChange ℂ) · v^(0,1)).
• TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul_mul_self: the Clifford relation c(v) ^ 2 = Q v, which is -|v|² Id in the geometric convention.
• TauCeti.AlmostComplexStructure.fockAction_ι_coe_W: a vector of W acts by √2 times exterior multiplication, and TauCeti.AlmostComplexStructure.fockAction_ι_coe_W': a vector of W' acts by 1 / √2 times contraction.
• TauCeti.AlmostComplexStructure.realFockAction_ι: a real generator ι Q v acts by c(v).
• TauCeti.AlmostComplexStructure.realFockAction_ι_mul_ι_apply_apply_one: on the vacuum, c(u) c(J u) 1 = i Q(u).

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §5.

theorem TauCeti.AlmostComplexStructure.scaledSpinAction_ι_one_tmul {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (r : ℂˣ) (v : V) : ((J.spinPolarizationData hQJ hQ).scaledSpinAction r) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) = ↑r • (J.spinPolarizationData hQJ hQ).wedge ⟨J.holomorphicPart v, ⋯⟩ + ↑r⁻¹ • (J.spinPolarizationData hQJ hQ).contract ⟨J.antiholomorphicPart v, ⋯⟩

The rescaled action of a real vector splits into its holomorphic creation part and antiholomorphic contraction part.

theorem TauCeti.AlmostComplexStructure.spinAction_ι_one_tmul {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (v : V) : (spinAction (QuadraticForm.baseChange ℂ Q) (J.spinPolarizationData hQJ hQ)) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) = (J.spinPolarizationData hQJ hQ).wedge ⟨J.holomorphicPart v, ⋯⟩ + (J.spinPolarizationData hQJ hQ).contract ⟨J.antiholomorphicPart v, ⋯⟩

The native action of a real vector on the spinor module ⋀ W of the polarization by a complex structure: exterior multiplication by v^(1,0) plus contraction against QuadraticMap.polar (Q.baseChange ℂ) · v^(0,1).

noncomputable def TauCeti.AlmostComplexStructure.fockAction {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) : CliffordAlgebra (QuadraticForm.baseChange ℂ Q) →ₐ[ℂ] Module.End ℂ (ExteriorAlgebra ℂ ↥(J.spinPolarizationData hQJ hQ).W)

The √2-normalized Fock action of the complexified Clifford algebra on ⋀ W: the conjugate of the native action TauCeti.spinAction by the degree scaling of ⋀ W by √2. A real vector v acts by √2 (ε(v^(1,0)) - ι(v^(0,1))), where ι contracts against the complex-bilinear form g_ℂ = -polar Q_ℂ / 2 (TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul).

theorem TauCeti.AlmostComplexStructure.fockAction_eq_scaledSpinAction {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) {r : ℂˣ} (hr : ↑r = ↑√2) : J.fockAction hQJ hQ = (J.spinPolarizationData hQJ hQ).scaledSpinAction r

The normalized Fock action is the rescaled spinor representation for any unit of value √2.

theorem TauCeti.AlmostComplexStructure.degreeScaling_comp_spinAction_eq_fockAction_comp {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) {r : ℂˣ} (hr : ↑r = ↑√2) (a : CliffordAlgebra (QuadraticForm.baseChange ℂ Q)) : (ExteriorAlgebra.degreeScaling r).toLinearMap ∘ₗ (spinAction (QuadraticForm.baseChange ℂ Q) (J.spinPolarizationData hQJ hQ)) a = (J.fockAction hQJ hQ) a ∘ₗ (ExteriorAlgebra.degreeScaling r).toLinearMap

The degree scaling by √2 intertwines the native and the normalized Fock actions: T ∘ spinAction a = fockAction a ∘ T, where T multiplies ⋀^p W by √2 ^ p (TauCeti.ExteriorAlgebra.degreeScaling_of_mem_exteriorPower).

theorem TauCeti.AlmostComplexStructure.fockAction_bijective {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) : Function.Bijective ⇑(J.fockAction hQJ hQ)

The normalized Fock action is bijective: like the native action TauCeti.spinAction, of which it is a conjugate, it identifies the complexified Clifford algebra with the endomorphisms of ⋀ W. The dimension of V is even because V carries the complex structure J.

theorem TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (v : V) : (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) = ↑√2 • ((J.spinPolarizationData hQJ hQ).wedge ⟨J.holomorphicPart v, ⋯⟩ + 2⁻¹ • (J.spinPolarizationData hQJ hQ).contract ⟨J.antiholomorphicPart v, ⋯⟩)

The normalized Fock action of a real vector: c(v) is √2 times exterior multiplication by v^(1,0) plus √2 / 2 times contraction against QuadraticMap.polar (Q.baseChange ℂ) · v^(0,1). In the geometric convention Q (v) = -g (v, v) that contraction is -2 ι(v^(0,1)) for the contraction ι against g_ℂ, so this is c(v) = √2 (ε(v^(1,0)) - ι(v^(0,1))).

theorem TauCeti.AlmostComplexStructure.fockAction_ι_one_tmul_mul_self {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (v : V) : (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) * (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v)) = (algebraMap ℂ (Module.End ℂ (ExteriorAlgebra ℂ ↥(J.spinPolarizationData hQJ hQ).W))) ↑(Q v)

The Clifford relation for the normalized Fock action: c(v) ^ 2 = Q v. In the geometric convention Q (v) = -g (v, v) this is c(v) ^ 2 = -|v|² Id.

@[simp]

theorem TauCeti.AlmostComplexStructure.fockAction_ι_coe_W {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (x : ↥(J.spinPolarizationData hQJ hQ).W) : (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) ↑x) = ↑√2 • (J.spinPolarizationData hQJ hQ).wedge x

In the normalized Fock action a vector of W acts by √2 times exterior multiplication.

@[simp]

theorem TauCeti.AlmostComplexStructure.fockAction_ι_coe_W' {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (y : ↥(J.spinPolarizationData hQJ hQ).W') : (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) ↑y) = (↑√2)⁻¹ • (J.spinPolarizationData hQJ hQ).contract y

In the normalized Fock action a vector of W' acts by 1 / √2 times contraction.

noncomputable def TauCeti.AlmostComplexStructure.realFockAction {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) : CliffordAlgebra Q →ₐ[ℝ] Module.End ℂ (ExteriorAlgebra ℂ ↥(J.spinPolarizationData hQJ hQ).W)

The Fock action of the real Clifford algebra: the normalized Fock action TauCeti.AlmostComplexStructure.fockAction restricted along the canonical map CliffordAlgebra.ofBaseChangeAux : CliffordAlgebra Q → CliffordAlgebra (Q.baseChange ℂ), which sends ι Q v to ι (1 ⊗ v). It makes ⋀ W a complex Clifford module of the real quadratic space (V, Q), on which a real vector v acts by c(v) = √2 (ε(v^(1,0)) - ι(v^(0,1))).

theorem TauCeti.AlmostComplexStructure.realFockAction_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (a : CliffordAlgebra Q) : (J.realFockAction hQJ hQ) a = (J.fockAction hQJ hQ) ((CliffordAlgebra.ofBaseChangeAux ℂ Q) a)

Unfolding lemma for TauCeti.AlmostComplexStructure.realFockAction.

@[simp]

theorem TauCeti.AlmostComplexStructure.realFockAction_ι {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (v : V) : (J.realFockAction hQJ hQ) ((CliffordAlgebra.ι Q) v) = (J.fockAction hQJ hQ) ((CliffordAlgebra.ι (QuadraticForm.baseChange ℂ Q)) (1 ⊗ₜ[ℝ] v))

In the real Fock action a real generator ι Q v acts by the normalized Fock operator c(v) of 1 ⊗ v.

theorem TauCeti.AlmostComplexStructure.realFockAction_ι_mul_ι_apply_apply_one {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} [FiniteDimensional ℝ V] (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (hQ : QuadraticMap.Nondegenerate) (u : V) : ((J.realFockAction hQJ hQ) ((CliffordAlgebra.ι Q) u * (CliffordAlgebra.ι Q) (J.toLinearMap u))) 1 = (Complex.I * ↑(Q u)) • 1

The Fock operators of u and J u on the vacuum: c(u) c(J u) 1 = i Q(u) for the vacuum 1 of ⋀ W.