Smooth almost complex structure on a real manifold

Definition

almostComplexToComplexStructure

by wesleyfei · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-geometrydifferential-geometrymanifolds

Let $M$ be a smooth manifold modeled on $\mathbb R^{2n}$ . An almost complex structure is a smooth assignment of a continuous real-linear endomorphism $J_x:T_xM\to T_xM$ to every point, satisfying

J_x(J_xv)=-v

for every tangent vector $v\in T_xM$ . This equips each tangent space with complex linear algebra, but it does not assert that $J$ is integrable or that complex coordinate charts exist.

The definition is reusable as the hypothesis interface for the open almost-complex-to-complex existence problem.

Formalization Note Smoothness is stated for the induced fiber-preserving map on Mathlib's total tangent bundle; no abstract integrability predicate is included.

Definition code

import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
import Mathlib.Geometry.Manifold.Instances.Real

open scoped Manifold ContDiff

set_option autoImplicit false

universe u

namespace AlmostComplexToComplex

/-- A smooth almost complex structure on a real `2 * n`-manifold.

The field `J` is a smoothly varying real-linear endomorphism of the tangent
bundle and `square_eq_neg` is the pointwise identity `J² = -id`.
-/
structure AlmostComplexStructure (n : ℕ) (M : Type u)
    [TopologicalSpace M]
    [ChartedSpace (EuclideanSpace ℝ (Fin (2 * n))) M]
    [IsManifold (𝓡 (2 * n)) ∞ M] where
  J : (x : M) →
    TangentSpace (𝓡 (2 * n)) x →L[ℝ] TangentSpace (𝓡 (2 * n)) x
  square_eq_neg : ∀ (x : M) (v : TangentSpace (𝓡 (2 * n)) x),
    J x (J x v) = -v
  smooth : ContMDiff (𝓡 (2 * n)).tangent (𝓡 (2 * n)).tangent ∞
    (fun p : TangentBundle (𝓡 (2 * n)) M ↦
      (⟨p.1, J p.1 p.2⟩ : TangentBundle (𝓡 (2 * n)) M))

end AlmostComplexToComplex

Source

G. Granja and A. Milivojević, Topology of Almost Complex Structures on Six-Manifolds, SIGMA 18 (2022), 093, Introduction p. 1, https://doi.org/10.3842/SIGMA.2022.093

Read-back

What the Lean code literally says, in plain math · openai-codex/gpt-6-astra

For every natural number $n$ and every type $M$ in an arbitrary universe, equipped with a topology, a charted-space structure modeled on $\mathbb R^{2n}$ , and a $C^\infty$ real manifold structure for those charts, an AlmostComplexStructure on $M$ consists of a family of continuous real-linear maps $J_x:T_xM\to T_xM$ , one for each $x\in M$ , together with the requirements that $J_x(J_x(v))=-v$ for every $x\in M$ and every $v\in T_xM$ , and that the induced total tangent-bundle map $TM\to TM$ , $(x,v)\mapsto(x,J_x(v))$ , is $C^\infty$ for the tangent-bundle manifold structures induced by the given real charts. The parameter $n=0$ is allowed; its tangent spaces are zero-dimensional, so the square identity imposes no nonzero-vector condition. The empty space is also allowed, with the pointwise requirements vacuous. No Hausdorffness, second countability, compactness, connectedness, or nonemptiness assumption is imposed.

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by wesleyfei · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph