The type is invariant under B-field shifts
ProvedGeneralizedComplex.genType_bShiftLet be a generalized almost complex structure on and a real 2-form on . Then the B-field transform is again a generalized almost complex structure, and
where denotes the -eigenbundle.
Formalization Note At the level of a single fiber the closedness of required in the source plays no role (it matters only for integrability), so is an arbitrary skew matrix.
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_bShift {N : ℕ} (J : Matrix (GIdx N) (GIdx N) ℝ) (hJ : IsGenAlmostComplex J)
(B : Matrix (Fin N) (Fin N) ℝ) (hB : Bᵀ = -B) :
IsGenAlmostComplex (bShift B * J * bShift (-B)) ∧
genType (plusIEigenspace (bShift B * J * bShift (-B))) = genType (plusIEigenspace J) := by
sorry
end GeneralizedComplexConfirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.