A generalized almost complex structure has type at most
ProvedGeneralizedComplex.genType_leLet be a generalized almost complex structure on , , with -eigenbundle . Then
where is the projection of to the tangent part.
While the type of a subspace can a priori be anything between and , generalized almost complex structures cannot exceed .
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 genType_le {N : ℕ} (J : Matrix (GIdx N) (GIdx N) ℝ) (hJ : IsGenAlmostComplex J) :
genType (plusIEigenspace J) ≤ N := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.