Nijenhuis equations in a product trivialization

In a smooth product trivialization with constant base complex structure i, as in linear holomorphic base coordinates, a complex-structure family has block form J(a,v) = (i a, α a + j v). Only α and j vary with the point. Its mixed, horizontal and vertical Nijenhuis components are computed here on the native smooth almost-complex-structure carrier. Total vanishing is equivalent to the mixed, horizontal and fibrewise equations.

The formulas mixedTerm and horizontalTerm follow Robbin–Salamon's corrected family integrability calculation. Their vector-field bracket is the negative of Mathlib's bracket. Consequently the native Nijenhuis values are (0, -j M) and (0, -ζ), respectively. All derivatives below are real derivatives on the total product, so the formulas include both base and fibre variation.

Main declarations

• verticalTerm, fderiv_blockEndomorphism_apply, fderiv_fiber_connection: the vertical family expression and block/fibre Fréchet derivatives.
• blockNijenhuisExpr and blockNijenhuisExpr_horizontal_vertical, blockNijenhuisExpr_horizontal_horizontal, blockNijenhuisExpr_vertical_vertical: raw normed-space Nijenhuis expression and component formulas (without finite-dimensionality).
• nijenhuis_horizontal_vertical and nijenhuis_horizontal_horizontal: the mixed and horizontal component formulas.
• nijenhuis_vertical_vertical: the fibrewise component formula.
• lieBracket_fiber_eq: the native fibre bracket and its sign comparison with the source bracket.
• nijenhuis_eq_zero_iff: the full vanishing criterion.

References

• J. W. Robbin and D. A. Salamon, Corrigendum to A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 9 (2007), 901–905, Lemma A and the subsequent Remark.

def TauCeti.ComplexStructureFamily.blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) : B × V →L[ℝ] B × V

The block endomorphism J(a,v) = (i a, α a + j v) on a product, with constant base block i; only α and j vary with the point.

@[simp]

theorem TauCeti.ComplexStructureFamily.blockEndomorphism_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p w : B × V) : (blockEndomorphism i α j p) w = (i w.1, (α p) w.1 + (j p) w.2)

Evaluation of the block endomorphism on a base and a fibre vector.

theorem TauCeti.ComplexStructureFamily.blockEndomorphism_eq_inl_add_inr {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) : blockEndomorphism i α j p = ContinuousLinearMap.inl ℝ B V ∘SL i ∘SL ContinuousLinearMap.fst ℝ B V + ContinuousLinearMap.inr ℝ B V ∘SL (α p ∘SL ContinuousLinearMap.fst ℝ B V + j p ∘SL ContinuousLinearMap.snd ℝ B V)

Expressing blockEndomorphism via inl and inr exposes its regularity in (α, j).

theorem TauCeti.ComplexStructureFamily.differentiableAt_blockEndomorphism {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {p : B × V} (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) : DifferentiableAt ℝ (blockEndomorphism i α j) p

Differentiability of blockEndomorphism i α j at p from differentiability of α and j.

theorem TauCeti.ComplexStructureFamily.fderiv_blockEndomorphism_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {q : B × V} (hα : DifferentiableAt ℝ α q) (hj : DifferentiableAt ℝ j q) (h w : B × V) : ((fderiv ℝ (blockEndomorphism i α j) q) h) w = (0, ((fderiv ℝ α q) h) w.1 + ((fderiv ℝ j q) h) w.2)

Fréchet derivative of blockEndomorphism i α j: the constant base block differentiates to 0, while the vertical block differentiates to fderiv ℝ α q h w.1 + fderiv ℝ j q h w.2.

noncomputable def TauCeti.ComplexStructureFamily.mixedTerm {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) (a : B) (v : V) : V

The corrected mixed equation dj(a) + j dj(ia) + j L_(αa) j, evaluated on v. The Lie derivative here is L_ξ j = dj(ξ) + j Dξ - Dξ j.

theorem TauCeti.ComplexStructureFamily.mixedTerm_def {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) (a : B) (v : V) : mixedTerm i α j p a v = ((fderiv ℝ j p) (a, 0)) v + (j p) (((fderiv ℝ j p) (i a, 0)) v) + (j p) (((fderiv ℝ j p) (0, (α p) a)) v + (j p) (((fderiv ℝ α p) (0, v)) a) - ((fderiv ℝ α p) (0, (j p) v)) a)

Expansion of the mixed family equation in total-space derivatives.

noncomputable def TauCeti.ComplexStructureFamily.horizontalTerm {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) (a b : B) : V

The corrected horizontal curvature equation, evaluated on two constant base directions. Its last two terms are the source bracket [αa,αb] = D(αa)(αb) - D(αb)(αa), which is the negative of Mathlib's vector-field bracket.

theorem TauCeti.ComplexStructureFamily.horizontalTerm_def {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p : B × V) (a b : B) : horizontalTerm i α j p a b = ((fderiv ℝ α p) (i b, 0)) a - (j p) (((fderiv ℝ α p) (b, 0)) a) - ((fderiv ℝ α p) (i a, 0)) b + (j p) (((fderiv ℝ α p) (a, 0)) b) + ((fderiv ℝ α p) (0, (α p) b)) a - ((fderiv ℝ α p) (0, (α p) a)) b

Expansion of the horizontal family equation in total-space derivatives.

noncomputable def TauCeti.ComplexStructureFamily.verticalTerm {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (j : B × V → V →L[ℝ] V) (p : B × V) (v w : V) : V

The vertical (fibrewise) Nijenhuis expression of j at p, evaluated on fibre vectors v and w. Only fibre derivatives (0, ·) of j occur.

theorem TauCeti.ComplexStructureFamily.verticalTerm_def {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (j : B × V → V →L[ℝ] V) (p : B × V) (v w : V) : verticalTerm j p v w = ((fderiv ℝ j p) (0, (j p) v)) w - ((fderiv ℝ j p) (0, (j p) w)) v + (j p) (((fderiv ℝ j p) (0, w)) v) - (j p) (((fderiv ℝ j p) (0, v)) w)

Expansion of the vertical family equation in total-space derivatives.

theorem TauCeti.ComplexStructureFamily.fderiv_fiber_connection {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {α : B × V → B →L[ℝ] V} {p : B × V} (hα : DifferentiableAt ℝ α p) (a : B) (v : V) : (fderiv ℝ (fun (y : V) => (α (p.1, y)) a) p.2) v = ((fderiv ℝ α p) (0, v)) a

Directional derivative along the fibre {p.1} × V of y ↦ α (p.1, y) a.

theorem TauCeti.ComplexStructureFamily.lieBracket_fiber_eq {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (α : B × V → B →L[ℝ] V) {p : B × V} (hα : DifferentiableAt ℝ α p) (a b : B) : VectorField.lieBracket ℝ (fun (v : V) => (α (p.1, v)) a) (fun (v : V) => (α (p.1, v)) b) p.2 = ((fderiv ℝ α p) (0, (α p) a)) b - ((fderiv ℝ α p) (0, (α p) b)) a

The native bracket of two fibre vector fields from α, in total-space derivatives. The source bracket in horizontalTerm is its negative.

noncomputable def TauCeti.ComplexStructureFamily.blockNijenhuisExpr {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p u w : B × V) : B × V

Pointwise Nijenhuis expression of blockEndomorphism i α j at p on u, w (valid on arbitrary real normed spaces without finite-dimensionality).

theorem TauCeti.ComplexStructureFamily.blockNijenhuisExpr_def {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (p u w : B × V) : blockNijenhuisExpr i α j p u w = ((fderiv ℝ (blockEndomorphism i α j) p) ((blockEndomorphism i α j p) u)) w - ((fderiv ℝ (blockEndomorphism i α j) p) ((blockEndomorphism i α j p) w)) u + (blockEndomorphism i α j p) (((fderiv ℝ (blockEndomorphism i α j) p) w) u) - (blockEndomorphism i α j p) (((fderiv ℝ (blockEndomorphism i α j) p) u) w)

Expansion of blockNijenhuisExpr in terms of fderiv ℝ (blockEndomorphism i α j).

theorem TauCeti.ComplexStructureFamily.blockNijenhuisExpr_horizontal_vertical {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {p : B × V} (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (hj_sq : ∀ (v : V), (j p) ((j p) v) = -v) (a : B) (v : V) : blockNijenhuisExpr i α j p (a, 0) (0, v) = (0, -(j p) (mixedTerm i α j p a v))

Raw mixed component of blockNijenhuisExpr: when j(p)² = -1, its value on (a, 0) and (0, v) is (0, -j p (mixedTerm i α j p a v)).

theorem TauCeti.ComplexStructureFamily.blockNijenhuisExpr_horizontal_horizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} (j : B × V → V →L[ℝ] V) {p : B × V} (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (a b : B) : blockNijenhuisExpr i α j p (a, 0) (b, 0) = (0, -horizontalTerm i α j p a b)

Raw horizontal component of blockNijenhuisExpr: its value on (a, 0) and (b, 0) is (0, -horizontalTerm i α j p a b).

theorem TauCeti.ComplexStructureFamily.blockNijenhuisExpr_vertical_vertical {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {p : B × V} (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (v w : V) : blockNijenhuisExpr i α j p (0, v) (0, w) = (0, verticalTerm j p v w)

Raw vertical component of blockNijenhuisExpr: its value on (0, v) and (0, w) is (0, verticalTerm j p v w), independent of i and α.

Native Nijenhuis tensor on finite-dimensional products

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_blockNijenhuisExpr {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (u w : B × V) : ((J.nijenhuis p) u) w = blockNijenhuisExpr i α j p u w

When J agrees with blockEndomorphism i α j near p and α, j are differentiable at p, the native Nijenhuis tensor J.nijenhuis p agrees with blockNijenhuisExpr i α j p.

theorem TauCeti.ComplexStructureFamily.nijenhuis_horizontal_vertical {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (a : B) (v : V) : ((J.nijenhuis p) (a, 0)) (0, v) = (0, -(j p) (mixedTerm i α j p a v))

The mixed Nijenhuis component in a product trivialization. With the native Lie bracket its sign is the negative of Robbin–Salamon's j M.

theorem TauCeti.ComplexStructureFamily.nijenhuis_horizontal_horizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (a b : B) : ((J.nijenhuis p) (a, 0)) (b, 0) = (0, -horizontalTerm i α j p a b)

The horizontal Nijenhuis component is the negative of the corrected horizontal equation. This term is present even when the mixed equation vanishes.

theorem TauCeti.ComplexStructureFamily.nijenhuis_vertical_vertical {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (v w : V) : ((J.nijenhuis p) (0, v)) (0, w) = (0, verticalTerm j p v w)

The vertical component is the ordinary fibre Nijenhuis expression: only fibre derivatives of j occur, and the connection term α drops out.

theorem TauCeti.ComplexStructureFamily.mixedTerm_eq_zero_of_nijenhuis_eq_zero {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (hN : J.nijenhuis p = 0) (a : B) (v : V) : mixedTerm i α j p a v = 0

Vanishing of the native Nijenhuis tensor forces the corrected mixed equation.

theorem TauCeti.ComplexStructureFamily.horizontalTerm_eq_zero_of_nijenhuis_eq_zero {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) (hN : J.nijenhuis p = 0) (a b : B) : horizontalTerm i α j p a b = 0

Vanishing of the native Nijenhuis tensor also forces the horizontal curvature equation.

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (J : SmoothAlmostComplexStructure (modelWithCornersSelf ℝ (B × V)) (B × V)) (i : B →L[ℝ] B) (α : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) {p : B × V} (hJ : (fun (q : B × V) => J.toEndomorphism q) =ᶠ[nhds p] blockEndomorphism i α j) (hα : DifferentiableAt ℝ α p) (hj : DifferentiableAt ℝ j p) : J.nijenhuis p = 0 ↔ (∀ (a : B) (v : V), mixedTerm i α j p a v = 0) ∧ (∀ (a b : B), horizontalTerm i α j p a b = 0) ∧ ∀ (v w : V), ((J.nijenhuis p) (0, v)) (0, w) = 0

The full product criterion: the mixed and horizontal equations, together with fibrewise vanishing, are equivalent to vanishing of the total Nijenhuis tensor. In particular, when the fibres are integrable, both of the corrected family equations remain necessary.