A real space with a linear complex structure has even dimension

Proved

JHolomorphic.exists_finrank_eq_two_mul_of_comp_eq_neg_id

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

linear-algebrapseudoholomorphic-curvessymplectic-geometry

Let $E$ be a finite-dimensional real normed vector space and let $J:E\to E$ be a continuous real-linear map with $J\circ J=-\mathrm{Id}_E$ . Then $\dim_{\mathbb{R}}E$ is even: there is a natural number $n$ with $\dim_{\mathbb{R}}E=2n$ .

This supplies the complex dimension $n$ needed to compare $E$ with $\mathbb{C}^n$ whenever $E$ carries a linear complex structure, for instance the value of an almost complex structure at one point.

Formalization Note The hypothesis is J.comp J = -ContinuousLinearMap.id ℝ E for J : E →L[ℝ] E; the conclusion is ∃ n : ℕ, Module.finrank ℝ E = 2 * n. The case $E=\{0\}$ (with $n=0$ ) is included.

Preamble

import Mathlib.LinearAlgebra.Complex.Module
import Mathlib.LinearAlgebra.Complex.FiniteDimensional
import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.Topology.Algebra.Module.FiniteDimension

Formal statement

namespace JHolomorphic

/-- A finite-dimensional real normed space carrying a continuous linear map `J` with
`J ∘ J = -1` has even real dimension. -/
theorem exists_finrank_eq_two_mul_of_comp_eq_neg_id {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [FiniteDimensional ℝ E] (J : E →L[ℝ] E)
    (hJ : J.comp J = -ContinuousLinearMap.id ℝ E) :
    ∃ n : ℕ, Module.finrank ℝ E = 2 * n := by
  sorry

end JHolomorphic

Source

Standard linear algebra; used in C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2

View graph