The Nijenhuis tensor of a smooth almost complex structure

For a smooth almost complex structure J on a finite-dimensional manifold, the Nijenhuis expression on vector fields is N_J(X, Y) = [JX, JY] - [X, Y] - J[JX, Y] - J[X, JY], with Mathlib's Lie bracket VectorField.mlieBracket. It is linear over differentiable functions in each argument, so it is a tensor: its value at x depends only on X x and Y x. This file constructs that tensor as a continuous bilinear map on each tangent space, through Mathlib's tensoriality criterion TensorialAt.mkHom₂, and proves its basic algebraic identities. The construction follows Mathlib's torsion tensor IsCovariantDerivativeOn.torsion.

The Nijenhuis tensor is the obstruction to integrability of J: the Newlander–Nirenberg theorem says that J comes from a complex atlas exactly when it vanishes. Its vanishing is equivalent to involutivity of the ±i eigenbundles of J in the complexified tangent bundle, and it controls the components of the exterior derivative outside the bidegrees (1,0) and (0,1). The identities N_J(Jv, w) = -J N_J(v, w) proved here are the real form of the type statement that N_J maps two (0,1) vectors to a (1,0) vector. Extended complex-bilinearly to the complexified tangent spaces ℂ ⊗[ℝ] T_x M, the tensor indeed maps two vectors of type (0,1) to a vector of type (1,0), two vectors of type (1,0) to a vector of type (0,1), and vanishes on a vector of type (1,0) and one of type (0,1); on parts of real tangent vectors, N_J(v^(0,1), w^(0,1)) = N_J(v, w)^(1,0).

Main declarations

• TauCeti.SmoothAlmostComplexStructure.nijenhuis: the Nijenhuis tensor at a point.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply: its value on differentiable vector fields is the Nijenhuis expression in Lie brackets.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_eq_zero_iff: the tensor vanishes exactly when [JX, JY] = [X, Y] + J[JX, Y] + J[X, JY] for all differentiable vector fields.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_antisymm: skew-symmetry.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_left, TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_right, TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_both: anti-commutation with J in each argument, and sign reversal under applying J to both arguments.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_neg: -J has the same Nijenhuis tensor.
• SmoothAlmostComplexStructure.baseChange_nijenhuis_antiholomorphicPart_antiholomorphicPart, SmoothAlmostComplexStructure.baseChange_nijenhuis_holomorphicPart_holomorphicPart: N_J(v^(0,1), w^(0,1)) = N_J(v, w)^(1,0) and N_J(v^(1,0), w^(1,0)) = N_J(v, w)^(0,1) for the complex-bilinear extension to the complexified tangent space.
• TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_mem_eigenspace_neg_of_mem_left, SmoothAlmostComplexStructure.baseChange_nijenhuis_eq_zero_of_mem_eigenspace_I_of_mem_neg_I and their companions: the type identities of the complex-bilinear extension on the eigenspaces T^(1,0)_x M and T^(0,1)_x M of the complexified J.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_eq_fderivWithin_inChart: the Nijenhuis tensor through the derivative of J read in a chart, N_J(v, w) = A (J v) w + A v (J w) - A (J w) v - A w (J v). The proof evaluates the Lie brackets of the vector fields with constant coordinates in that chart and of their images under J.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_eq_fderiv: on a vector space, compute the tensor from a local formula for J using real derivatives and Mathlib's bracket sign.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_model_eq_zero_iff: on a vector space, tensor vanishing is equivalent to pointwise vanishing in the model-space instances.
• TauCeti.SmoothAlmostComplexStructure.nijenhuis_const: a constant almost complex structure on a vector space has vanishing Nijenhuis tensor.

Conventions

No factor 1/4 is included; some sources use N_J / 4 instead.

References

• Daniel Huybrechts, Complex Geometry: An Introduction, Universitext, Springer, 2005, Section 2.6.

noncomputable def TauCeti.SmoothAlmostComplexStructure.nijenhuis {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) [FiniteDimensional ℝ E] (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] TangentSpace I x

The Nijenhuis tensor of a smooth almost complex structure J at a point x: the continuous bilinear map on T_x M whose value on the values at x of differentiable vector fields X and Y is [JX, JY] - [X, Y] - J[JX, Y] - J[X, JY] at x (nijenhuis_apply).

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] {X Y : (x : M) → TangentSpace I x} (hX : (MDiffAt fun (x : M) => ⟨x, X x⟩) x) (hY : (MDiffAt fun (x : M) => ⟨x, Y x⟩) x) : ((J.nijenhuis x) (X x)) (Y x) = VectorField.mlieBracket I (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (X y)) (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (Y y)) x - VectorField.mlieBracket I X Y x - (fun (x : M) => ⇑(J.toEndomorphism x)) x (VectorField.mlieBracket I (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (X y)) Y x) - (fun (x : M) => ⇑(J.toEndomorphism x)) x (VectorField.mlieBracket I X (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (Y y)) x)

On vector fields differentiable at x, the Nijenhuis tensor is N_J(X, Y) = [JX, JY] - [X, Y] - J[JX, Y] - J[X, JY].

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_eq_zero_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) [FiniteDimensional ℝ E] : J.nijenhuis = 0 ↔ ∀ {X Y : (x : M) → TangentSpace I x} {x : M}, (MDiffAt fun (x : M) => ⟨x, X x⟩) x → (MDiffAt fun (x : M) => ⟨x, Y x⟩) x → VectorField.mlieBracket I (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (X y)) (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (Y y)) x = VectorField.mlieBracket I X Y x + (fun (x : M) => ⇑(J.toEndomorphism x)) x (VectorField.mlieBracket I (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (X y)) Y x) + (fun (x : M) => ⇑(J.toEndomorphism x)) x (VectorField.mlieBracket I X (fun (y : M) => (fun (x : M) => ⇑(J.toEndomorphism x)) y (Y y)) x)

The Nijenhuis tensor vanishes everywhere exactly when [JX, JY] = [X, Y] + J[JX, Y] + J[X, JY] for all vector fields differentiable at the point.

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_antisymm {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((J.nijenhuis x) v) w = -((J.nijenhuis x) w) v

The Nijenhuis tensor is skew-symmetric.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_self {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v : TangentSpace I x) : ((J.nijenhuis x) v) v = 0

The Nijenhuis tensor vanishes on the diagonal.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((J.nijenhuis x) ((fun (x : M) => ⇑(J.toEndomorphism x)) x v)) w = -(fun (x : M) => ⇑(J.toEndomorphism x)) x (((J.nijenhuis x) v) w)

The Nijenhuis tensor anti-commutes with J in its first argument: N_J(Jv, w) = -J N_J(v, w).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((J.nijenhuis x) v) ((fun (x : M) => ⇑(J.toEndomorphism x)) x w) = -(fun (x : M) => ⇑(J.toEndomorphism x)) x (((J.nijenhuis x) v) w)

The Nijenhuis tensor anti-commutes with J in its second argument: N_J(v, Jw) = -J N_J(v, w).

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_both {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((J.nijenhuis x) ((fun (x : M) => ⇑(J.toEndomorphism x)) x v)) ((fun (x : M) => ⇑(J.toEndomorphism x)) x w) = -((J.nijenhuis x) v) w

Applying J to both arguments of the Nijenhuis tensor changes its sign: N_J(Jv, Jw) = -N_J(v, w).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_neg {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) [FiniteDimensional ℝ E] (x : M) : (-J).nijenhuis x = J.nijenhuis x

The almost complex structures J and -J have the same Nijenhuis tensor.

Type identities on the complexified tangent space

Extend the Nijenhuis tensor complex-bilinearly to the complexification ℂ ⊗[ℝ] T_x M. By its anti-commutation with J in each argument, it maps two vectors of type (0,1) to a vector of type (1,0) and two vectors of type (1,0) to a vector of type (0,1), and it vanishes on a vector of type (1,0) and one of type (0,1). On the (0,1)- and (1,0)-parts of real tangent vectors, N_J(v^(0,1), w^(0,1)) = N_J(v, w)^(1,0) and N_J(v^(1,0), w^(1,0)) = N_J(v, w)^(0,1).

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_mem_eigenspace_neg_of_mem_left {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] {μ : ℂ} {X : TensorProduct ℝ ℂ (TangentSpace I x)} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) μ) (Y : TensorProduct ℝ ℂ (TangentSpace I x)) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) X) Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) (-μ)

The complex-bilinear extension of the Nijenhuis tensor maps an eigenvector of the complexified J for the eigenvalue μ in its first argument into the eigenspace for -μ. In particular it maps a vector of type (0,1) and any second vector to a vector of type (1,0).

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_mem_eigenspace_neg_of_mem_right {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (X : TensorProduct ℝ ℂ (TangentSpace I x)) {μ : ℂ} {Y : TensorProduct ℝ ℂ (TangentSpace I x)} (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) μ) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) X) Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) (-μ)

The complex-bilinear extension of the Nijenhuis tensor maps an eigenvector of the complexified J for the eigenvalue μ in its second argument into the eigenspace for -μ.

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_eq_zero_of_mem_eigenspace_I_of_mem_neg_I {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] {X Y : TensorProduct ℝ ℂ (TangentSpace I x)} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) Complex.I) (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) (-Complex.I)) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) X) Y = 0

The complex-bilinear extension of the Nijenhuis tensor vanishes on a vector of type (1,0) and a vector of type (0,1).

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_eq_zero_of_mem_eigenspace_neg_I_of_mem_I {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] {X Y : TensorProduct ℝ ℂ (TangentSpace I x)} (hX : X ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) (-Complex.I)) (hY : Y ∈ Module.End.eigenspace (LinearMap.baseChange ℂ (J.almostComplexStructureAt x).toLinearMap) Complex.I) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) X) Y = 0

The complex-bilinear extension of the Nijenhuis tensor vanishes on a vector of type (0,1) and a vector of type (1,0).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_holomorphicPart_antiholomorphicPart {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) ((J.almostComplexStructureAt x).holomorphicPart v)) ((J.almostComplexStructureAt x).antiholomorphicPart w) = 0

The complex-bilinear extension of the Nijenhuis tensor vanishes on the (1,0)-part of v and the (0,1)-part of w.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_antiholomorphicPart_holomorphicPart {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) ((J.almostComplexStructureAt x).antiholomorphicPart v)) ((J.almostComplexStructureAt x).holomorphicPart w) = 0

The complex-bilinear extension of the Nijenhuis tensor vanishes on the (0,1)-part of v and the (1,0)-part of w.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_antiholomorphicPart_antiholomorphicPart {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) ((J.almostComplexStructureAt x).antiholomorphicPart v)) ((J.almostComplexStructureAt x).antiholomorphicPart w) = (J.almostComplexStructureAt x).holomorphicPart (((J.nijenhuis x) v) w)

The type identity of the Nijenhuis tensor. Its complex-bilinear extension maps the (0,1)-parts of v and w to the (1,0)-part of N_J(v, w): N_J(v^(0,1), w^(0,1)) = N_J(v, w)^(1,0).

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.baseChange_nijenhuis_holomorphicPart_holomorphicPart {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) {x : M} [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((LinearMap.BilinMap.baseChange ℂ (ContinuousLinearMap.toLinearMap₁₂ (J.nijenhuis x))) ((J.almostComplexStructureAt x).holomorphicPart v)) ((J.almostComplexStructureAt x).holomorphicPart w) = (J.almostComplexStructureAt x).antiholomorphicPart (((J.nijenhuis x) v) w)

The conjugate type identity of the Nijenhuis tensor: its complex-bilinear extension maps the (1,0)-parts of v and w to the (0,1)-part of N_J(v, w): N_J(v^(1,0), w^(1,0)) = N_J(v, w)^(0,1).

The Nijenhuis tensor in a chart

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_apply_eq_fderivWithin_inChart {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] (J : SmoothAlmostComplexStructure I M) (x : M) [FiniteDimensional ℝ E] (v w : TangentSpace I x) : ((J.nijenhuis x) v) w = ((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) ((fun (x : M) => ⇑(J.toEndomorphism x)) x v)) w + ((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) v) ((fun (x : M) => ⇑(J.toEndomorphism x)) x w) - ((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) ((fun (x : M) => ⇑(J.toEndomorphism x)) x w)) v - ((fderivWithin ℝ (J.inChart x) (Set.range ↑I) (↑(extChartAt I x) x)) w) ((fun (x : M) => ⇑(J.toEndomorphism x)) x v)

The Nijenhuis tensor in a chart. Let A be the derivative at the chart point of the almost complex structure read in the chart at x (SmoothAlmostComplexStructure.inChart). Then N_J(v, w) = A (J v) w + A v (J w) - A (J w) v - A w (J v).

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_model_eq_zero_iff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V) (x : V) : J.nijenhuis x = 0 ↔ ∀ (v w : V), ((J.nijenhuis x) v) w = 0

On a vector space, tensor vanishing is equivalent to vanishing on all pairs of model vectors. The right side uses the ordinary zero of the model space, not a tangent-space instance.

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_eq_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ V) V) (A : V → V →L[ℝ] V) (x : V) (hA : (fun (y : V) => J.toEndomorphism y) =ᶠ[nhds x] A) (v w : V) : ((J.nijenhuis x) v) w = (fderiv ℝ (fun (y : V) => (A y) w) x) ((A x) v) - (fderiv ℝ (fun (y : V) => (A y) v) x) ((A x) w) + (A x) ((fderiv ℝ (fun (y : V) => (A y) v) x) w) - (A x) ((fderiv ℝ (fun (y : V) => (A y) w) x) v)

In a vector space, the Nijenhuis tensor can be computed by differentiating the images of constant vector fields. The signs use the native bracket [X,Y] = DY X - DX Y.

@[simp]

theorem TauCeti.SmoothAlmostComplexStructure.nijenhuis_const {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (Jc : V →L[ℝ] V) (hJc : ∀ (v : V), Jc (Jc v) = -v) (x : V) : (const Jc hJc).nijenhuis x = 0

A constant almost complex structure on a finite-dimensional real vector space has vanishing Nijenhuis tensor.