A generalized almost complex structure is determined by its -eigenbundle
ProvedGeneralizedComplex.eq_of_plusIEigenspace_eqLet be generalized almost complex structures on with the same -eigenbundle:
Then .
This is the uniqueness half of the eigenbundle correspondence.
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_of_plusIEigenspace_eq {N : ℕ} (J₁ J₂ : Matrix (GIdx N) (GIdx N) ℝ)
(h₁ : IsGenAlmostComplex J₁) (h₂ : IsGenAlmostComplex J₂)
(h : plusIEigenspace J₁ = plusIEigenspace J₂) : J₁ = J₂ := by sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.