Complex structures are generalized complex of type
ProvedGeneralizedComplex.complexStructureGen_specLet be a linear complex structure on , i.e. . Then
is a generalized almost complex structure on , and its type equals .
This is the pointwise content of the statement that complex 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 complexStructureGen_spec {N : ℕ} (J₀ : Matrix (Fin N) (Fin N) ℝ) (hJ₀ : J₀ * J₀ = -1) :
IsGenAlmostComplex (complexStructureGen J₀) ∧
genType (plusIEigenspace (complexStructureGen J₀)) = N := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.