Type- structures are B-shifts of symplectic ones
ProvedGeneralizedComplex.eq_bShift_symplecticGen_of_genType_eq_zeroLet be a generalized almost complex structure on whose -eigenbundle has type . Then there are a real 2-form and a nondegenerate real 2-form on such that
This is the pointwise content of the statement that, up to a shift of the B-field, symplectic structures are the only type- generalized complex structures.
Formalization Note Pointwise, no closedness of or is involved; the global statement in the source additionally needs integrability.
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 eq_bShift_symplecticGen_of_genType_eq_zero {N : ℕ} (J : Matrix (GIdx N) (GIdx N) ℝ)
(hJ : IsGenAlmostComplex J) (h0 : genType (plusIEigenspace J) = 0) :
∃ B ω : Matrix (Fin N) (Fin N) ℝ, Bᵀ = -B ∧ ωᵀ = -ω ∧ ω.det ≠ 0 ∧
J = bShift B * symplecticGen ω * bShift (-B) := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.