Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)verified 2026-11-04 (gpt-6.1-sol)
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Kodaira–Spencer forms form a differential graded Lie algebra

Statement

Let X be a complex manifold of complex dimension n with complex structure J. Write TXC:=TX⊗RC, with the complex-linear extension JC of J, and define TX1,0:=ker⁡(JC−iI),TX0,1:=ker⁡(JC+iI). The holomorphic coordinate transitions give TX1,0 its holomorphic tangent-bundle structure. For 0≤p≤n, define the smooth vector-valued (0,p)-forms by A0,p(X,TX1,0):=Γ∞ ⁣(X,Λp(TX0,1)∗⊗CTX1,0),Lp:=A0,p(X,TX1,0), and set Lp=0 outside this range. On scalar complex-valued forms, let ∂ˉ be the (0,1)-type component of the exterior differential. In a holomorphic frame ∂1,…,∂n of TX1,0, define ∂ˉ ⁣(∑iαi⊗∂i):=∑i(∂ˉαi)⊗∂i. This is independent of the holomorphic frame because frame-transition coefficients are holomorphic. In holomorphic coordinates (z1,…,zn), write ∂a=∂/∂za and define the bracket by [α,β]i=αa∧∂aβi−(−1)pqβa∧∂aαi,α∈Lp,β∈Lq. Then this bracket is coordinate-independent, has degree p+q, is graded antisymmetric and satisfies graded Jacobi; with differential ∂ˉ, it satisfies ∂ˉ[α,β]=[∂ˉα,β]+(−1)p[α,∂ˉβ],∂ˉ2=0. Thus (L∙,∂ˉ,[−,−]) is a cohomological differential graded Lie algebra.

Facts & Assumptions

Given: A complex manifold X with holomorphic tangent bundle TX1,0.

[F1]

Holomorphic coordinate changes have holomorphic transition maps and induce the holomorphic tangent-bundle transition maps (Complex manifolds, holomorphic vector bundles and Hermitian metrics).

Proof

technique · direct
1.1F1givenalgebra

For α∈Lp, contraction with the (1,0) part of exterior differentiation defines an intrinsic degree-p operator Dα:A0,∙(X)→A0,∙+p(X) by Dαω=αi∧∂iω. Intrinsicity follows because both the tensor contraction and the (1,0) exterior derivative are coordinate-independent under the holomorphic changes in [F1]. The product rule for ∂i and moving the degree-p form αi past a degree-r form gives Dα(ω∧η)=Dαω∧η+(−1)prω∧Dαη; hence Dα is a graded derivation. Computing the graded commutator on a function cancels the symmetric second-derivative terms ∂a∂if=∂i∂af and leaves coefficient αa∧∂aβi−(−1)pqβa∧∂aαi. Therefore [Dα,Dβ]=D[α,β] with the stated formula; applying the equality to local coordinate functions shows the coefficient tensor is unique.

2.1F1step 1.1givenalgebra∎

In any associative graded endomorphism algebra the graded commutator is graded antisymmetric and satisfies graded Jacobi: expanding each nested commutator yields each of the six ordered triple products twice with opposite signs. Commutators of degree-p and degree-q derivations are derivations of degree p+q, as follows by expanding both sides of the graded Leibniz rule and cancelling the two mixed terms. These facts transfer through the injective map α↦Dα to the bracket on L. Finally, in holomorphic coordinates ∂ˉ∂i=∂i∂ˉ on coefficients, and the graded Leibniz rule gives [∂ˉ,Dα]=D∂ˉα. The graded Jacobi identity for the commutator with ∂ˉ now yields ∂ˉ[α,β]=[∂ˉα,β]+(−1)p[α,∂ˉβ]. Since ∂ˉ2=0 on forms, all differential graded Lie algebra identities hold.

Remarks

The formula fixes the sign convention used in the Maurer–Cartan equation. It establishes the DGLA identities, but does not identify this DGLA's Maurer–Cartan groupoid with the analytic deformation groupoid; that comparison belongs to the Kuranishi argument.

Depends on

Dependency tree · 2 levels

Sources