structure HasHolomorphicCoords {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) : Prop

Existence of holomorphic coordinates for an almost complex structure $J$: a chart $\varphi$ in which $J$ intertwines with a pointwise complex structure $J_{\mathrm{loc}}^*$ on 1-forms, Lie brackets of vector fields pull back to act trivially on pulled-back forms, and pulled-back forms separate vector fields.

• holo_coords : ∃ (Ω_loc : ℕ → Type) (VF_loc : Type) (inst_loc : DifferentialFormSpace Ω_loc VF_loc) (_J_loc : AlmostComplexStr) (φ : DFSMorphism Ω VF Ω_loc VF_loc) (J_loc_star : Ω_loc 1 → Ω_loc 1), (∀ (X : VF) (α : Ω_loc 1), DifferentialFormSpace.ι (J.J X) (φ.pullback α) = DifferentialFormSpace.ι X (φ.pullback (J_loc_star α))) ∧ (∀ (α : Ω_loc 1), J_loc_star (J_loc_star α) = -α) ∧ (∀ (X Y : VF) (α_loc : Ω_loc 1), DifferentialFormSpace.ι (HasLieBracket.bracket Ω X Y) (φ.pullback α_loc) = 0) ∧ ∀ (Z : VF), (∀ (α_loc : Ω_loc 1), DifferentialFormSpace.ι Z (φ.pullback α_loc) = 0) → ∀ (β : Ω 1), DifferentialFormSpace.ι Z β = 0

theorem nijenhuis_expr_vanishes_on_pullback {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) {Ω_loc : ℕ → Type} {VF_loc : Type} {inst_loc : DifferentialFormSpace Ω_loc VF_loc} (φ : DFSMorphism Ω VF Ω_loc VF_loc) (J_loc_star : Ω_loc 1 → Ω_loc 1) (h_holo : ∀ (X : VF) (α : Ω_loc 1), DifferentialFormSpace.ι (J.J X) (φ.pullback α) = DifferentialFormSpace.ι X (φ.pullback (J_loc_star α))) (h_flat : ∀ (X Y : VF) (α_loc : Ω_loc 1), DifferentialFormSpace.ι (HasLieBracket.bracket Ω X Y) (φ.pullback α_loc) = 0) (X Y : VF) (α_loc : Ω_loc 1) : DifferentialFormSpace.ι (HasLieBracket.bracket Ω (J.J X) (J.J Y)) (φ.pullback α_loc) - DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω (J.J X) Y)) (φ.pullback α_loc) - DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω X (J.J Y))) (φ.pullback α_loc) - DifferentialFormSpace.ι (HasLieBracket.bracket Ω X Y) (φ.pullback α_loc) = 0

Computation lemma: in holomorphic coordinates, the Nijenhuis-tensor expression $[JX, JY] - J[JX, Y] - J[X, JY] - [X, Y]$ pulls back to zero against any local 1-form.

theorem isIntegrable_of_hasHolomorphicCoords {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h_nij : IsNijenhuisOf J nij) (hJ : HasHolomorphicCoords J) : IsIntegrable J nij

Proposition 3 (one direction): if $J$ admits holomorphic coordinates then $J$ is integrable, i.e. the Nijenhuis tensor vanishes, $N_J = 0$.

structure MfdNijenhuis.ACSOnMfd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_1 u_4)

An almost complex structure on a manifold: a pointwise endomorphism $J_x: T_x M \to T_x M$ with $J_x^2 = -\mathrm{id}$.

• J (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x
• sq_neg (x : M) (v : TangentSpace I x) : (self.J x) ((self.J x) v) = -v

noncomputable def MfdNijenhuis.nijenhuisTensorMfd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (Jstr : ACSOnMfd I M) (U V : (x : M) → TangentSpace I x) (x : M) : TangentSpace I x

The Nijenhuis tensor on a manifold: $N_J(U, V) = [JU, JV] - J[U, JV] - J[JU, V] - [U, V]$.

structure MfdNijenhuis.Form01OnMfd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (Jstr : ACSOnMfd I M) : Type (max u_1 u_3)

A $(0,1)$-form on a manifold with almost complex structure $J$: real and imaginary parts $\alpha = \mathrm{re} + i\, \mathrm{im}$ satisfying the type condition $\mathrm{im}(X) = \mathrm{re}(JX)$, so $\alpha \in \wedge^{0,1} T^*M$.

• re (x : M) : TangentSpace I x →L[ℝ] ℝ
• im (x : M) : TangentSpace I x →L[ℝ] ℝ
• type_cond (X : (x : M) → TangentSpace I x) (x : M) : (self.im x) (X x) = (self.re x) ((Jstr.J x) (X x))

structure MfdNijenhuis.CartanDataOnMfd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] (Jstr : ACSOnMfd I M) : Type (max u_1 u_4)

Cartan-calculus data on a manifold: an evaluation map for $d\alpha(X, Y)$ via the Cartan formula $d\alpha(X, Y) = X(\alpha(Y)) - Y(\alpha(X)) - \alpha([X, Y])$, the Lie derivative on functions, and the $(2,0)$-component $(d\alpha)^{(2,0)}$ of $d$ applied to a $(0,1)$-form.

• d_eval : ((x : M) → TangentSpace I x →L[ℝ] ℝ) → ((x : M) → TangentSpace I x) → ((x : M) → TangentSpace I x) → M → ℝ
• lieD : ((x : M) → TangentSpace I x) → (M → ℝ) → M → ℝ
• cartan (α : (x : M) → TangentSpace I x →L[ℝ] ℝ) (X Y : (x : M) → TangentSpace I x) (x : M) : self.d_eval α X Y x = self.lieD X (fun (y : M) => (α y) (Y y)) x - self.lieD Y (fun (y : M) => (α y) (X y)) x - (α x) (VectorField.mlieBracket I X Y x)
• lieD_sub (X : (x : M) → TangentSpace I x) (f g : M → ℝ) (x : M) : self.lieD X (fun (y : M) => f y - g y) x = self.lieD X f x - self.lieD X g x
• lieD_neg (X : (x : M) → TangentSpace I x) (f : M → ℝ) (x : M) : self.lieD X (fun (y : M) => -f y) x = -self.lieD X f x
• d_antisymm (α : (x : M) → TangentSpace I x →L[ℝ] ℝ) (X Y : (x : M) → TangentSpace I x) (x : M) : self.d_eval α X Y x = -self.d_eval α Y X x
• dForm20 : Form01OnMfd Jstr → (x : M) → TangentSpace I x [⋀^Fin 2]→ₗ[ℝ] ℝ
• dForm20_eval (f : Form01OnMfd Jstr) (U V : (x : M) → TangentSpace I x) (x : M) : (self.dForm20 f x) ![U x, V x] = self.d_eval f.re U V x - self.d_eval f.re (fun (y : M) => (Jstr.J y) (U y)) (fun (y : M) => (Jstr.J y) (V y)) x + self.d_eval f.im U (fun (y : M) => (Jstr.J y) (V y)) x + self.d_eval f.im (fun (y : M) => (Jstr.J y) (U y)) V x

noncomputable def MfdNijenhuis.nijDualEvalOnMfd {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (Jstr : ACSOnMfd I M) (f : Form01OnMfd Jstr) (U V : (x : M) → TangentSpace I x) (x : M) : ℝ

Evaluation of the dual Nijenhuis map $N^*\alpha(U, V) = \alpha(N_J(U, V))$ — pair the $(0,1)$-form's real part with the Nijenhuis tensor.

theorem MfdNijenhuis.nijenhuis_dual_map_is_d_20_typed {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (Jstr : ACSOnMfd I M) (ops : CartanDataOnMfd I M Jstr) (f : Form01OnMfd Jstr) (U V : (x : M) → TangentSpace I x) (x : M) : (ops.dForm20 f x) ![U x, V x] = nijDualEvalOnMfd Jstr f U V x

Proposition 4: the dual Nijenhuis map equals the $(2,0)$-component of the exterior derivative on $(0,1)$-forms, $N^*\alpha = (d\alpha)^{(2,0)}$, i.e. $\alpha(N_J(U, V)) = (d\alpha)^{(2,0)}(U, V)$.