The induced Hermitian form on the (1,0)- and (0,1)-parts

Let g be a real bilinear form on V preserved by an almost complex structure J, and let h (x, y) = g_ℂ (conj x, y) be its sesquilinear complexification (LinearMap.BilinForm.sesqComplexification), the positive Hermitian form on ℂ ⊗[ℝ] V when g is a Euclidean metric. This file computes h on the decomposition 1 ⊗ v = v^(1,0) + v^(0,1) of a real vector into its parts in the i- and -i-eigenspaces W and W' of the complexified complex structure:

• W and W' are h-orthogonal, a case of the h-orthogonality of eigenspaces of any complexified g-preserving map (LinearMap.BilinForm.sesqComplexification_eq_zero_of_mem_eigenspace);
• h (v^(1,0), w^(1,0)) = (g (v, w) - i g (v, J w)) / 2, so for symmetric g, |v^(1,0)|² = h (v^(1,0), v^(1,0)) = g (v, v) / 2.

On the complex vector space (V, J) the Hermitian form g (v, w) - i g (v, J w), conjugate-linear in its first argument, is therefore twice the pullback of h|_W along v ↦ v^(1,0). For g the metric ω (·, J ·) of a J-invariant symplectic form ω, this form is TauCeti.SymplecticForm.complexAssociatedForm.

In the geometric convention for spinors, Q (v) = -g (v, v), the isotropic subspace W carries the exterior model ⋀ W of the spinor module of (V, g, J), and the restriction of h to W is the Hermitian metric on W that induces a Hermitian metric on that model.

Main results

• TauCeti.AlmostComplexStructure.sesqComplexification_eq_zero_of_mem_eigenspace_I_of_mem_neg_I: W and W' are h-orthogonal.
• TauCeti.AlmostComplexStructure.sesqComplexification_holomorphicPart_holomorphicPart: h (v^(1,0), w^(1,0)) = (g (v, w) - i g (v, J w)) / 2.
• TauCeti.AlmostComplexStructure.sesqComplexification_holomorphicPart_self: h (v^(1,0), v^(1,0)) = g (v, v) / 2.
• TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification: the Hermitian form of a J-invariant symplectic form is twice the pullback of h along v ↦ v^(1,0).

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §5, for the Hermitian metric on the isotropic subspace of a complex structure.
• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.1, for the Hermitian form of a compatible pair.

Orthogonality of the (1,0)- and (0,1)-parts

theorem TauCeti.AlmostComplexStructure.sesqComplexification_eq_zero_of_mem_eigenspace_I_of_mem_neg_I {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) {x y : TensorProduct ℝ ℂ V} (hx : x ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) Complex.I) (hy : y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ J.toLinearMap) (-Complex.I)) : (g.sesqComplexification x) y = 0

The i- and -i-eigenspaces of the complexified complex structure are orthogonal for the induced Hermitian form.

@[simp]

theorem TauCeti.AlmostComplexStructure.sesqComplexification_holomorphicPart_antiholomorphicPart {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v w : V) : (g.sesqComplexification (J.holomorphicPart v)) (J.antiholomorphicPart w) = 0

The (1,0)-part of one real vector is orthogonal to the (0,1)-part of another for the induced Hermitian form.

@[simp]

theorem TauCeti.AlmostComplexStructure.sesqComplexification_antiholomorphicPart_holomorphicPart {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v w : V) : (g.sesqComplexification (J.antiholomorphicPart v)) (J.holomorphicPart w) = 0

The (0,1)-part of one real vector is orthogonal to the (1,0)-part of another for the induced Hermitian form.

The induced Hermitian form on the parts

theorem TauCeti.AlmostComplexStructure.sesqComplexification_holomorphicPart_holomorphicPart {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v w : V) : (g.sesqComplexification (J.holomorphicPart v)) (J.holomorphicPart w) = 2⁻¹ * (↑((g v) w) - Complex.I * ↑((g v) (J.toLinearMap w)))

The induced Hermitian form on (1,0)-parts: h (v^(1,0), w^(1,0)) = (g (v, w) - i g (v, J w)) / 2.

theorem TauCeti.AlmostComplexStructure.sesqComplexification_antiholomorphicPart_antiholomorphicPart {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v w : V) : (g.sesqComplexification (J.antiholomorphicPart v)) (J.antiholomorphicPart w) = 2⁻¹ * (↑((g v) w) + Complex.I * ↑((g v) (J.toLinearMap w)))

The induced Hermitian form on (0,1)-parts: h (v^(0,1), w^(0,1)) = (g (v, w) + i g (v, J w)) / 2, the conjugate of its value on the (1,0)-parts.

theorem TauCeti.AlmostComplexStructure.sesqComplexification_holomorphicPart_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hg : g.IsSymm) (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v : V) : (g.sesqComplexification (J.holomorphicPart v)) (J.holomorphicPart v) = 2⁻¹ * ↑((g v) v)

The squared norm of the (1,0)-part of a real vector is half the square of the vector: h (v^(1,0), v^(1,0)) = g (v, v) / 2, that is |v^(1,0)|² = |v|² / 2 for a Euclidean metric g.

theorem TauCeti.AlmostComplexStructure.sesqComplexification_antiholomorphicPart_self {V : Type u_1} [AddCommGroup V] [Module ℝ V] (J : AlmostComplexStructure V) {g : LinearMap.BilinForm ℝ V} (hg : g.IsSymm) (hgJ : ∀ (v w : V), (g (J.toLinearMap v)) (J.toLinearMap w) = (g v) w) (v : V) : (g.sesqComplexification (J.antiholomorphicPart v)) (J.antiholomorphicPart v) = 2⁻¹ * ↑((g v) v)

The squared norm of the (0,1)-part of a real vector is half the square of the vector: h (v^(0,1), v^(0,1)) = g (v, v) / 2.

theorem TauCeti.SymplecticForm.Invariant.complexAssociatedForm_eq_two_mul_sesqComplexification {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : SymplecticForm V} {J : AlmostComplexStructure V} (hinv : ω.Invariant J) (v w : V) : ω.complexAssociatedForm J v w = 2 * ((ω.associatedBilinForm J).sesqComplexification (J.holomorphicPart v)) (J.holomorphicPart w)

The Hermitian form of a J-invariant symplectic form is twice the pullback of the induced Hermitian form along v ↦ v^(1,0): with g = ω (·, J ·) and h its sesquilinear complexification, ω (v, J w) + i ω (v, w) = 2 h (v^(1,0), w^(1,0)).