Documentation

TauCeti.Geometry.Symplectic.Complex.QuadraticForm

Almost complex structures preserving a quadratic form #

Let Q be a quadratic form on a real vector space V and J an almost complex structure on V preserving Q. Then J preserves the polar form of Q and is antisymmetric for it. The complex-linear extension of J to ℂ ⊗[ℝ] V preserves Q.baseChange ℂ, so its eigenspaces ker (J - i) and ker (J + i) are totally isotropic: if J w = ± i w then Q w = Q (J w) = (± i)² Q w = -Q w.

The pairing of the (1,0)- and (0,1)-parts v^(1,0) = (v - i J v) / 2 and v^(0,1) = (v + i J v) / 2 is computed from the real polar form:

polar (v^(1,0)) (w^(0,1)) = (polar Q v w + i · polar Q v (J w)) / 2.

Main definitions #

Main results #

J as an isometry of Q #

source
def TauCeti.AlmostComplexStructure.toIsometry {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) :
Q →qᵢ Q

A Q-preserving almost complex structure, as an isometry of Q.

Instances For
    source
    @[simp]
    theorem TauCeti.AlmostComplexStructure.toIsometry_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (v : V) :
    (J.toIsometry hQJ) v = J.toLinearMap v
    source
    @[simp]
    theorem TauCeti.AlmostComplexStructure.polar_apply_apply {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (v w : V) :
    QuadraticMap.polar (⇑Q) (J.toLinearMap v) (J.toLinearMap w) = QuadraticMap.polar (⇑Q) v w

    The polar form of a quadratic form is preserved by a Q-preserving almost complex structure.

    source
    theorem TauCeti.AlmostComplexStructure.polar_apply_left_eq_neg_polar_apply_right {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (v w : V) :
    QuadraticMap.polar (⇑Q) (J.toLinearMap v) w = -QuadraticMap.polar (⇑Q) v (J.toLinearMap w)

    The polar form of a J-preserved quadratic form is antisymmetric under moving J across: polar Q (J v) w = -polar Q v (J w).

    source
    @[simp]
    theorem TauCeti.AlmostComplexStructure.baseChange_apply_baseChange {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (w : TensorProduct ℝ ℂ V) :
    (QuadraticForm.baseChange ℂ Q) ((LinearMap.baseChange ℂ J.toLinearMap) w) = (QuadraticForm.baseChange ℂ Q) w

    The complexification of a Q-preserving almost complex structure preserves the base-changed form.

    Isotropy of the eigenspaces #

    source
    theorem TauCeti.AlmostComplexStructure.isTotallyIsotropic_eigenspace_baseChange_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) :
    QuadraticMap.IsTotallyIsotropic (QuadraticForm.baseChange ℂ Q) (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I)

    The i-eigenspace of the complexification of a Q-preserving almost complex structure is totally isotropic for the base-changed form.

    source
    theorem TauCeti.AlmostComplexStructure.isTotallyIsotropic_eigenspace_baseChange_neg_I {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) :
    QuadraticMap.IsTotallyIsotropic (QuadraticForm.baseChange ℂ Q) (Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I))

    The -i-eigenspace of the complexification of a Q-preserving almost complex structure is totally isotropic for the base-changed form.

    The pairing of the two parts #

    source
    theorem TauCeti.AlmostComplexStructure.polar_holomorphicPart_antiholomorphicPart {V : Type u} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {Q : QuadraticForm ℝ V} (hQJ : ∀ (v : V), Q (J.toLinearMap v) = Q v) (v w : V) :
    QuadraticMap.polar (⇑(QuadraticForm.baseChange ℂ Q)) (J.holomorphicPart v) (J.antiholomorphicPart w) = 2⁻¹ * (↑(QuadraticMap.polar (⇑Q) v w) + Complex.I * ↑(QuadraticMap.polar (⇑Q) v (J.toLinearMap w)))

    The pairing of the (1,0)- and (0,1)-parts. For a quadratic form Q preserved by J, the base-changed polar form pairs v^(1,0) with w^(0,1) to (polar Q v w + i · polar Q v (J w)) / 2.