Prove2Me

A linear complex structure on a 2n2n-dimensional real space is isomorphic to Cn\mathbb{C}^n

Proved
JHolomorphic.exists_bijective_clm_I_smul_eq

by Mazecto · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrapseudoholomorphic-curvessymplectic-geometry

Let EE be a finite-dimensional real normed vector space with dim⁡RE=2n\dim_{\mathbb{R}} E = 2n, and let J:E→EJ:E\to E be a real-linear map with J∘J=−IdEJ\circ J=-\mathrm{Id}_E. Then there is a real-linear bijection T:Cn→ET:\mathbb{C}^n\to E such that

T(i w)=J(Tw)for all w∈Cn.T(i\,w)=J(T w)\qquad\text{for all } w\in\mathbb{C}^n.

This is the normal form of a linear complex structure: it lets one transport problems about a varying complex structure on EE to the standard structure on Cn\mathbb{C}^n, for instance in local trivializations of Cauchy–Riemann type operators.

Formalization Note Cn\mathbb{C}^n is EuclideanSpace ℂ (Fin n) with its real structure; TT has type EuclideanSpace ℂ (Fin n) →L[ℝ] E and bijectivity is Function.Bijective T.

Preamble
import Mathlib.LinearAlgebra.Complex.Module
import Mathlib.LinearAlgebra.Complex.FiniteDimensional
import Mathlib.Analysis.InnerProductSpace.PiL2
Formal statement
namespace JHolomorphic

/-- A real vector space `E` of dimension `2n` carrying a linear complex structure `J` (`J² = -1`)
admits a real-linear bijection `T : ℂⁿ → E` with `T (i w) = J (T w)` for all `w`. -/
theorem exists_bijective_clm_I_smul_eq {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [FiniteDimensional ℝ E] (n : ℕ) (hn : Module.finrank ℝ E = 2 * n) (J : E →L[ℝ] E)
    (hJ : J.comp J = -ContinuousLinearMap.id ℝ E) :
    ∃ T : EuclideanSpace ℂ (Fin n) →L[ℝ] E, Function.Bijective T ∧
      ∀ w, T (Complex.I • w) = J (T w) := by
  sorry

end JHolomorphic
Source
Standard linear algebra; used for C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2, Theorem 2.26

View graph