The polarization of a complexified quadratic space by a complex structure

Let Q be a quadratic form on a real vector space V and J an almost complex structure on V preserving Q. The complex-linear extension of J to ℂ ⊗[ℝ] V has the two eigenspaces W = ker (J - i) and W' = ker (J + i), which are complementary (TauCeti.AlmostComplexStructure.isCompl_eigenspace_baseChange_I_neg_I) and totally isotropic for the base-changed form (TauCeti.AlmostComplexStructure.isTotallyIsotropic_eigenspace_baseChange_I and TauCeti.AlmostComplexStructure.isTotallyIsotropic_eigenspace_baseChange_neg_I). When Q is nondegenerate and V is finite-dimensional, W and W' therefore polarize Q.baseChange ℂ, and the polar form pairs them perfectly. This is the polarization from which the exterior model ⋀ W of the spinor module of an even-dimensional Euclidean space with an orthogonal complex structure is built; the geometric convention takes Q (v) = -g (v, v) for the metric g.

A real vector v decomposes as 1 ⊗ v = v^(1,0) + v^(0,1), with v^(1,0) = (v - i J v) / 2 ∈ W and v^(0,1) = (v + i J v) / 2 ∈ W' (TauCeti.AlmostComplexStructure.holomorphicPart and TauCeti.AlmostComplexStructure.antiholomorphicPart); this is the decomposition the polarization uses. Their pairing is TauCeti.AlmostComplexStructure.polar_holomorphicPart_antiholomorphicPart.

Main definitions

• TauCeti.AlmostComplexStructure.spinPolarizationData: the polarization of Q.baseChange ℂ by the i- and -i-eigenspaces of the complexified complex structure.

Main results

• TauCeti.AlmostComplexStructure.spinPolarizationData_decompositionEquiv_symm_tmul: the polarization decomposes 1 ⊗ v as (v^(1,0), v^(0,1)).
• TauCeti.AlmostComplexStructure.finrank_spinPolarizationData_W: the isotropic summand W has complex dimension half the real dimension of V, and TauCeti.AlmostComplexStructure.spinPolarizationData_W_ne_bot: it is nonzero when V is.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry, Chapter I, for spinor modules of even-dimensional Euclidean spaces.
• C. Chevalley, The Algebraic Theory of Spinors, Chapter II, for spinor modules attached to a decomposition into complementary totally isotropic subspaces.

The polarization

noncomputable def TauCeti.AlmostComplexStructure.spinPolarizationData {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) : SpinPolarizationData (QuadraticForm.baseChange ℂ Q)

The polarization of a complexified quadratic space by a complex structure. For a nondegenerate quadratic form Q on a finite-dimensional real vector space and an almost complex structure J preserving Q, the i- and -i-eigenspaces of the complexification of J are the two isotropic summands of a polarization of Q.baseChange ℂ, with no orthogonal remainder. Its pairing field identifies the -i-eigenspace with the dual of the i-eigenspace through the polar form.

@[simp]

theorem TauCeti.AlmostComplexStructure.spinPolarizationData_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) : (J.spinPolarizationData hQJ hQ).W = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I

@[simp]

theorem TauCeti.AlmostComplexStructure.spinPolarizationData_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) : (J.spinPolarizationData hQJ hQ).W' = Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)

@[simp]

theorem TauCeti.AlmostComplexStructure.spinPolarizationData_line {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) : (J.spinPolarizationData hQJ hQ).line = ⊥

theorem TauCeti.AlmostComplexStructure.holomorphicPart_mem_spinPolarizationData_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) (v : V) : J.holomorphicPart v ∈ (J.spinPolarizationData hQJ hQ).W

The (1,0)-part of a real vector lies in the first isotropic summand of the polarization.

theorem TauCeti.AlmostComplexStructure.antiholomorphicPart_mem_spinPolarizationData_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) (v : V) : J.antiholomorphicPart v ∈ (J.spinPolarizationData hQJ hQ).W'

The (0,1)-part of a real vector lies in the second isotropic summand of the polarization.

theorem TauCeti.AlmostComplexStructure.tmulConj_mem_spinPolarizationData_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 : TensorProduct ℝ ℂ V} (hx : x ∈ (J.spinPolarizationData hQJ hQ).W) : (tmulConj V) x ∈ (J.spinPolarizationData hQJ hQ).W'

Conjugation of the complexification maps the first isotropic summand of the polarization into the second.

theorem TauCeti.AlmostComplexStructure.tmulConj_mem_spinPolarizationData_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 : TensorProduct ℝ ℂ V} (hy : y ∈ (J.spinPolarizationData hQJ hQ).W') : (tmulConj V) y ∈ (J.spinPolarizationData hQJ hQ).W

Conjugation of the complexification maps the second isotropic summand of the polarization into the first.

@[simp]

theorem TauCeti.AlmostComplexStructure.spinPolarizationData_decompositionEquiv_symm_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.spinPolarizationData hQJ hQ).decompositionEquiv.symm (1 ⊗ₜ[ℝ] v) = ((⟨J.holomorphicPart v, ⋯⟩, ⟨J.antiholomorphicPart v, ⋯⟩), 0)

The decomposition of a real vector 1 ⊗ v along the polarization is (v^(1,0), v^(0,1)), with no component in the orthogonal remainder.

theorem TauCeti.AlmostComplexStructure.finrank_spinPolarizationData_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) : Module.finrank ℂ ↥(J.spinPolarizationData hQJ hQ).W = Module.finrank ℝ V / 2

The isotropic summand W of the polarization has complex dimension half the real dimension of V.

theorem TauCeti.AlmostComplexStructure.spinPolarizationData_W_ne_bot {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) [Nontrivial V] : (J.spinPolarizationData hQJ hQ).W ≠ ⊥

The isotropic summand W of the polarization of a nonzero space is nonzero.