Every symplectic vector space carries a compatible almost complex structure

Tameness and compatibility of an almost complex structure J with a symplectic form ω are standard hypotheses of J-holomorphic curve theory. This file supplies compatible structures for an arbitrary symplectic form on an arbitrary finite-dimensional real vector space, proving

TauCeti.SymplecticForm.exists_compatible: for every symplectic form ω on a finite-dimensional real vector space V there is an almost complex structure J with ω.Compatible J.

The proof is the classical linear normal-form induction, splitting off one hyperbolic pair at a time rather than diagonalizing a metric. Nondegeneracy provides, for any x ≠ 0, a partner y with ω x y = 1; the plane L = span {x, y} meets its symplectic complement L^ω only in 0, so ω restricts nondegenerately to both, V = L ⊕ L^ω, and ω is the product of the two restrictions. On L the pair (x, y) identifies (L, ω|_L) with the standard plane (ℝ × ℝ, ω₀) of TauCeti.stdSymplecticForm, which is compatible with TauCeti.AlmostComplexStructure.product; on L^ω, whose dimension has dropped by two, the inductive hypothesis applies. The two structures are recombined by TauCeti.SymplecticForm.prod_compatible and transported back along the splitting. This proves the nonemptiness part of the standard statement that the space of ω-compatible almost complex structures is nonempty and contractible; contractibility is not addressed here. The conventions are those of McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Section 2.2, which TauCeti/Geometry/Symplectic/AlmostComplex.lean already follows.

Main declarations

• TauCeti.SymplecticForm.compatible_prod_transport_of_splitting: compatible structures on the two summands of a symplectic splitting assemble into one on the whole space.
• TauCeti.SymplecticForm.exists_compatible and TauCeti.SymplecticForm.exists_tames: the existence theorems.
• TauCeti.SymplecticForm.even_finrank and TauCeti.SymplecticForm.isEmpty_of_odd_finrank: a symplectic vector space has even dimension, so an odd-dimensional space carries no symplectic form at all.

theorem TauCeti.SymplecticForm.compatible_prod_transport_of_splitting {V : Type u_1} [AddCommGroup V] [Module ℝ V] (ω : SymplecticForm V) {L : Submodule ℝ V} (hcompl : IsCompl L (ω.orthogonal L)) (JL : AlmostComplexStructure ↥L) (JL' : AlmostComplexStructure ↥(ω.orthogonal L)) (hJL : (ω.restrict L ⋯).Compatible JL) (hJL' : (ω.restrict (ω.orthogonal L) ⋯).Compatible JL') : ω.Compatible ((JL.prod JL').transport (L.prodEquivOfIsCompl (ω.orthogonal L) hcompl))

Compatible structures on the two halves of a symplectic splitting V = L ⊕ L^ω assemble into a compatible structure on V.

Hyperbolic pairs and the standard plane

Existence of a compatible almost complex structure

theorem TauCeti.SymplecticForm.exists_compatible {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : ∃ (J : AlmostComplexStructure V), ω.Compatible J

Every symplectic vector space carries a compatible almost complex structure.

For a symplectic form ω on a finite-dimensional real vector space there is an almost complex structure J that is ω-invariant and satisfies ω(v, Jv) > 0 for v ≠ 0. In particular the pointwise compatibility hypothesis on a symplectic vector space is satisfiable; the smooth fibrewise statement is not proved here.

theorem TauCeti.SymplecticForm.exists_tames {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : ∃ (J : AlmostComplexStructure V), ω.Tames J

Every finite-dimensional symplectic vector space is tamed by some almost complex structure.

theorem TauCeti.SymplecticForm.even_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : SymplecticForm V) : Even (Module.finrank ℝ V)

A finite-dimensional symplectic vector space has even dimension.

theorem TauCeti.SymplecticForm.isEmpty_of_odd_finrank {V : Type u_1} [AddCommGroup V] [Module ℝ V] (h : Odd (Module.finrank ℝ V)) : IsEmpty (SymplecticForm V)

A real vector space of odd dimension carries no symplectic form.