Symplectic forms are generalized complex of type
ProvedGeneralizedComplex.symplecticGen_specLet be a nondegenerate real 2-form on (a skew matrix with ), and write . Then
is a generalized almost complex structure on , and its type equals .
This is the pointwise content of the statement that symplectic manifolds are generalized complex manifolds of type .
Throughout, models a tangent space of an -manifold, its dual (identified with via the standard dual basis), and the generalized tangent space with the natural inner product . A generalized almost complex structure is a real linear map of with and ; its -eigenbundle is .
Formalization Note The statement is fiberwise: is the coordinate space GIdx N → ℝ (vector part on Sum.inl, one-form part on Sum.inr), endomorphisms are matrices indexed by GIdx N, and the complexification is GIdx N → ℂ with the real matrix acting through the coercion . All notions are those of the shared definition file Definitions.Def_GeneralizedComplex_Basic.
import Definitions.Def_GeneralizedComplex_Basic open Matrix
namespace GeneralizedComplex
theorem symplecticGen_spec {N : ℕ} (ω : Matrix (Fin N) (Fin N) ℝ) (hω : ωᵀ = -ω)
(hdet : ω.det ≠ 0) :
IsGenAlmostComplex (symplecticGen ω) ∧ genType (plusIEigenspace (symplecticGen ω)) = 0 := by
sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.