Integrability of product-trivialized almost complex families

In a product trivialization B × V over a base B with constant complex structure i, an almost complex family of block form J(p)(a, v) = (i a, α(p) a + j(p) v) has three Nijenhuis components (TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff): the mixed equation mixedTerm, the horizontal curvature equation horizontalTerm, and the vertical fibre Nijenhuis component verticalTerm.

This file develops the Lie-derivative and integrability theory of these equations:

1. Lie-derivative and Lie-bracket dictionary: mixedTerm_eq_add_lieDerivEndomorphism rewrites mixedTerm as ∂_a j + j ∂_{i a} j + j L_{α a} j, and horizontalTerm_eq_sub_lieBracket relates horizontalTerm to Mathlib's VectorField.lieBracket (with the opposite sign from Robbin–Salamon's source bracket).
2. Horizontal connection dictionary: when α arises from a horizontal connection lift (a, -v(a)) via connectionOfHorizontal i v j q a = j(q)(v(q) a + j(q)(v(q)(i a))), mixedTerm_connectionOfHorizontal identifies mixedTerm (when verticalTerm j p vanishes) with (∂_a j - L_{v a} j) + j (∂_{i a} j - L_{v(i a)} j), twice the complex-antilinear part 2 • ∂bar^H j of the horizontal covariant derivative ∇^H_a j = ∂_a j - L_{v a} j.
3. Surface-fibre and split-family criteria: when Module.finrank ℝ V ≤ 2 (in particular on real 2-dimensional surface fibres), the vertical Nijenhuis component vanishes automatically (nijenhuis_eq_zero_iff_of_finrank_le_two, nijenhuis_eq_zero_iff_of_finrank_eq_two). When α =ᶠ[𝓝 p] 0, horizontalTerm vanishes and mixedTerm reduces to base-holomorphy ∂_a j + j ∂_{i a} j = 0 (nijenhuis_eq_zero_iff_of_eventuallyEq_zero_of_finrank_le_two).
4. Robbin–Salamon Corrigendum Lemma B: lieDerivEndomorphism_horizontalTerm_eq_zero proves on arbitrary real normed spaces B, V under C² regularity of α and j that if mixedTerm vanishes on a neighborhood of p and verticalTerm also vanishes on a neighborhood of p (the verticalTerm hypothesis being automatic when Module.finrank ℝ V ≤ 2, with mixedTerm vanishing retained as a hypothesis in lieDerivEndomorphism_horizontalTerm_eq_zero_of_finrank_le_two), then the horizontal curvature y ↦ horizontalTerm i α j (p.1, y) a b is an infinitesimal automorphism of the fibre complex structure (L_{ζ(a, b)} j = 0 at p.2). On a product B × V this does not force horizontalTerm = 0 on its own (since (ℝ², j) carries nonzero holomorphic vector fields), so both mixedTerm = 0 and horizontalTerm = 0 remain necessary in a local product chart (nijenhuis_eq_zero_iff_of_finrank_eq_two); Lemma B provides the local chart identity used when globalizing to closed fibres without nonzero holomorphic vector fields.

References

• J. W. Robbin and D. A. Salamon, A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 8 (2006), 611–699, Section 8.9.
• J. W. Robbin and D. A. Salamon, Corrigendum to A construction of the Deligne–Mumford orbifold, J. Eur. Math. Soc. 9 (2007), 901–905, Lemmas A and B and Remark.

Fibre derivatives, Lie derivatives, and bracket form

theorem TauCeti.ComplexStructureFamily.fderiv_fiber_apply {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} (hj : DifferentiableAt ℝ j p) (u v : V) : ((fderiv ℝ (fun (y : V) => j (p.1, y)) p.2) u) v = ((fderiv ℝ j p) (0, u)) v

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

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

The fibre Lie derivative L_{α(a)} j at p.2 matches the last three terms of mixedTerm.

theorem TauCeti.ComplexStructureFamily.mixedTerm_eq_add_lieDerivEndomorphism {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) (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) ((lieDerivEndomorphism (fun (y : V) => (α (p.1, y)) a) (fun (y : V) => j (p.1, y)) p.2) v)

Express mixedTerm in terms of the fibre endomorphism Lie derivative: mixedTerm i α j p a v = ∂_a j(v) + j(∂_{i a} j(v)) + j((L_{α a} j) v).

theorem TauCeti.ComplexStructureFamily.horizontalTerm_eq_sub_lieBracket {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) (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) - VectorField.lieBracket ℝ (fun (y : V) => (α (p.1, y)) a) (fun (y : V) => (α (p.1, y)) b) p.2

Express horizontalTerm in terms of Mathlib's VectorField.lieBracket on the fibre. Because Robbin–Salamon's source bracket is -lieBracket, the bracket appears with a minus sign.

Horizontal connection dictionary (α(a) = j(v(a) + j v(i a)))

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

The off-diagonal connection block a ↦ j(q)(v(q) a + j(q)(v(q)(i a))) induced by a horizontal connection 1-form v (whose horizontal lift of a is (a, -v(q) a)).

@[simp]

theorem TauCeti.ComplexStructureFamily.connectionOfHorizontal_apply {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) (v : B × V → B →L[ℝ] V) (j : B × V → V →L[ℝ] V) (q : B × V) (a : B) : (connectionOfHorizontal i v j q) a = (j q) ((v q) a + (j q) ((v q) (i a)))

theorem TauCeti.ComplexStructureFamily.connectionOfHorizontal_anticommute {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {i : B →L[ℝ] B} (hi : ∀ (a : B), i (i a) = -a) (v : B × V → B →L[ℝ] V) {j : B × V → V →L[ℝ] V} {q : B × V} (hj : ∀ (w : V), (j q) ((j q) w) = -w) (a : B) : (connectionOfHorizontal i v j q) (i a) + (j q) ((connectionOfHorizontal i v j q) a) = 0

When i² = -1 and j(q)² = -1, connectionOfHorizontal i v j q is (i, j(q))-antilinear.

theorem TauCeti.ComplexStructureFamily.differentiableWithinAt_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {s : Set (B × V)} {p : B × V} (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hv : DifferentiableWithinAt ℝ v s p) (hj : DifferentiableWithinAt ℝ j s p) : DifferentiableWithinAt ℝ (connectionOfHorizontal i v j) s p

theorem TauCeti.ComplexStructureFamily.differentiableAt_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {p : B × V} (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hv : DifferentiableAt ℝ v p) (hj : DifferentiableAt ℝ j p) : DifferentiableAt ℝ (connectionOfHorizontal i v j) p

theorem TauCeti.ComplexStructureFamily.contDiffWithinAt_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {s : Set (B × V)} {p : B × V} (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hv : ContDiffWithinAt ℝ n v s p) (hj : ContDiffWithinAt ℝ n j s p) : ContDiffWithinAt ℝ n (connectionOfHorizontal i v j) s p

theorem TauCeti.ComplexStructureFamily.contDiffAt_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} {p : B × V} (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hv : ContDiffAt ℝ n v p) (hj : ContDiffAt ℝ n j p) : ContDiffAt ℝ n (connectionOfHorizontal i v j) p

theorem TauCeti.ComplexStructureFamily.contDiff_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : WithTop ℕ∞} (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} (hv : ContDiff ℝ n v) (hj : ContDiff ℝ n j) : ContDiff ℝ n (connectionOfHorizontal i v j)

theorem TauCeti.ComplexStructureFamily.mixedTerm_connectionOfHorizontal {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] (i : B →L[ℝ] B) {v : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {p : B × V} (hv : DifferentiableAt ℝ v p) (hj : DifferentiableAt ℝ j p) (hj_sq : ∀ᶠ (q : B × V) in nhds p, ∀ (w : V), (j q) ((j q) w) = -w) (hvert : ∀ (u w : V), verticalTerm j p u w = 0) (a : B) (w : V) : mixedTerm i (connectionOfHorizontal i v j) j p a w = ((fderiv ℝ j p) (a, 0)) w - (lieDerivEndomorphism (fun (y : V) => (v (p.1, y)) a) (fun (y : V) => j (p.1, y)) p.2) w + (j p) (((fderiv ℝ j p) (i a, 0)) w - (lieDerivEndomorphism (fun (y : V) => (v (p.1, y)) (i a)) (fun (y : V) => j (p.1, y)) p.2) w)

Horizontal ∂bar^H j identity: when α = connectionOfHorizontal i v j and the vertical Nijenhuis expression verticalTerm j p vanishes, mixedTerm equals (∂_a j - L_{v a} j) + j (∂_{i a} j - L_{v(i a)} j), twice the complex-antilinear part of the covariant horizontal derivative ∇^H_a j = ∂_a j - L_{v a} j along (a, -v(a)).

Surface-fibre (finrank ≤ 2) and split-family (α = 0) integrability

theorem TauCeti.ComplexStructureFamily.verticalTerm_eq_zero_of_finrank_le_two {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (hdim : Module.finrank ℝ V ≤ 2) {j : B × V → V →L[ℝ] V} {p : B × V} (hj : DifferentiableAt ℝ j p) (hj_sq : ∀ᶠ (q : B × V) in nhds p, ∀ (w : V), (j q) ((j q) w) = -w) (u w : V) : verticalTerm j p u w = 0

When V has real dimension at most 2 and j(q)² = -1 on a neighborhood of p, the fibrewise Nijenhuis expression verticalTerm j p vanishes automatically at p.

theorem TauCeti.ComplexStructureFamily.nijenhuis_vertical_vertical_eq_zero_of_finrank_le_two {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) (hdim : Module.finrank ℝ V ≤ 2) (v w : V) : ((J.nijenhuis p) (0, v)) (0, w) = 0

On surface fibres (Module.finrank ℝ V ≤ 2), the vertical Nijenhuis component vanishes automatically.

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff_of_finrank_le_two {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) (hdim : Module.finrank ℝ V ≤ 2) : 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

On fibres of real dimension at most 2, vanishing of J.nijenhuis p reduces to the mixed and horizontal family equations.

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff_of_finrank_eq_two {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) (hdim : Module.finrank ℝ V = 2) : 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

Real surface-fibre (Module.finrank ℝ V = 2) specialization of nijenhuis_eq_zero_iff_of_finrank_le_two.

theorem TauCeti.ComplexStructureFamily.horizontalTerm_eq_zero_of_eventuallyEq_zero {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α : α =ᶠ[nhds p] 0) (a b : B) : horizontalTerm i α j p a b = 0

When α =ᶠ[𝓝 p] 0, the horizontal curvature equation vanishes identically at p.

theorem TauCeti.ComplexStructureFamily.mixedTerm_of_eventuallyEq_zero {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α : α =ᶠ[nhds p] 0) (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)

When α =ᶠ[𝓝 p] 0, mixedTerm reduces to the base-holomorphy expression ∂_a j(v) + j(∂_{i a} j(v)).

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff_of_eventuallyEq_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α0 : α =ᶠ[nhds p] 0) (hj : DifferentiableAt ℝ j p) : J.nijenhuis p = 0 ↔ (∀ (a : B) (v : V), ((fderiv ℝ j p) (a, 0)) v + (j p) (((fderiv ℝ j p) (i a, 0)) v) = 0) ∧ ∀ (v w : V), ((J.nijenhuis p) (0, v)) (0, w) = 0

For a split family (α =ᶠ[𝓝 p] 0), integrability at p is equivalent to base-holomorphy of j together with fibrewise Nijenhuis vanishing.

theorem TauCeti.ComplexStructureFamily.nijenhuis_eq_zero_iff_of_eventuallyEq_zero_of_finrank_le_two {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ B] [FiniteDimensional ℝ V] (hdim : Module.finrank ℝ V ≤ 2) (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α0 : α =ᶠ[nhds p] 0) (hj : DifferentiableAt ℝ j p) : J.nijenhuis p = 0 ↔ ∀ (a : B) (v : V), ((fderiv ℝ j p) (a, 0)) v + (j p) (((fderiv ℝ j p) (i a, 0)) v) = 0

For a split family (α =ᶠ[𝓝 p] 0) on fibres of real dimension at most 2 (Module.finrank ℝ V ≤ 2), base-holomorphy of j is necessary and sufficient for J.nijenhuis p = 0.

Robbin–Salamon Corrigendum Lemma B (L_{ζ(a, b)} j = 0)

theorem TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] {i : B →L[ℝ] B} (hi : ∀ (a : B), i (i a) = -a) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {p : B × V} (hα : ContDiffAt ℝ 2 α p) (hj : ContDiffAt ℝ 2 j p) (hj_sq : ∀ᶠ (q : B × V) in nhds p, ∀ (v : V), (j q) ((j q) v) = -v) (hαj : ∀ᶠ (q : B × V) in nhds p, ∀ (a : B), (α q) (i a) + (j q) ((α q) a) = 0) (hmix : ∀ᶠ (q : B × V) in nhds p, ∀ (a : B) (v : V), mixedTerm i α j q a v = 0) (hvert : ∀ᶠ (q : B × V) in nhds p, ∀ (v w : V), verticalTerm j q v w = 0) (a b : B) : lieDerivEndomorphism (fun (y : V) => horizontalTerm i α j (p.1, y) a b) (fun (y : V) => j (p.1, y)) p.2 = 0

Robbin–Salamon Corrigendum Lemma B (on arbitrary real normed spaces under C² regularity): if i² = -1, j(q)² = -1, α(q)(i a) + j(q)(α(q) a) = 0, mixedTerm i α j q = 0, and verticalTerm j q = 0 on a neighborhood of p, then the fibre vector field y ↦ horizontalTerm i α j (p.1, y) a b has vanishing endomorphism Lie derivative on j(p.1, ·) at p.2.

theorem TauCeti.ComplexStructureFamily.lieDerivEndomorphism_horizontalTerm_eq_zero_of_finrank_le_two {B : Type u_1} {V : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] [NormedAddCommGroup V] [NormedSpace ℝ V] [FiniteDimensional ℝ V] (hdim : Module.finrank ℝ V ≤ 2) {i : B →L[ℝ] B} (hi : ∀ (a : B), i (i a) = -a) {α : B × V → B →L[ℝ] V} {j : B × V → V →L[ℝ] V} {p : B × V} (hα : ContDiffAt ℝ 2 α p) (hj : ContDiffAt ℝ 2 j p) (hj_sq : ∀ᶠ (q : B × V) in nhds p, ∀ (v : V), (j q) ((j q) v) = -v) (hαj : ∀ᶠ (q : B × V) in nhds p, ∀ (a : B), (α q) (i a) + (j q) ((α q) a) = 0) (hmix : ∀ᶠ (q : B × V) in nhds p, ∀ (a : B) (v : V), mixedTerm i α j q a v = 0) (a b : B) : lieDerivEndomorphism (fun (y : V) => horizontalTerm i α j (p.1, y) a b) (fun (y : V) => j (p.1, y)) p.2 = 0

Surface-fibre (Module.finrank ℝ V ≤ 2) version of lieDerivEndomorphism_horizontalTerm_eq_zero: the verticalTerm hypothesis is discharged automatically.