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.
The d, partial and dbar identities
Statement
Let be open and let all forms below be smooth and complex-valued. Then For and , The identities hold at bidegree endpoints as well, with components outside interpreted as zero.
Facts & Assumptions
Given: The open set and smooth complex-valued forms on .
Complex forms decompose uniquely by bidegree, and and are the two bidegree components of (Bigraded complex forms and the Dolbeault operators).
The published exterior derivative satisfies on smooth differential forms (The exterior derivative squares to zero).
For homogeneous real forms, the published exterior derivative obeys the graded product rule (The exterior derivative is a graded derivation).
Proof
Write a complex form with real forms . The coordinate formula defining on complex coefficients is the complex-linear extension of the real exterior derivative, so by [F2].
The real graded product rule [F3] extends to complex forms: write each complex form as real part plus times imaginary part, expand the wedge product by complex bilinearity, and apply [F3] to each real pair. The coordinate definition of in [F1] is complex-linear, so the resulting identity is the same signed rule for complex forms.
For a pure type form , [F1] gives and hence by step 1.1. These three terms have respective bidegrees , , and ; the direct sum uniqueness in [F1] forces each component to vanish, including when an endpoint component is zero by convention.
Let and . Wedge products add the two bidegrees (and vanish if a repeated differential occurs). In the complex graded-derivation identity from step 1.2, the terms involving have bidegree and those involving have bidegree . Projecting onto these distinct summands yields the two displayed Leibniz identities.
Every smooth complex form is a finite sum of its bidegree components, and both operators and wedge product are additive. Applying step 2.2 componentwise proves the graded Leibniz rules for all homogeneous forms; applying step 2.1 componentwise proves all three square and anticommutation identities for arbitrary forms.
Depends on
Used by
- Hartogs extension by a compact-support dbar correction Corollary
- A nonclosed dbar form cannot have a potential Counterexample
- Dolbeault cohomology of a domain Definition
- Cutoff extension across a puncture in complex dimension two Example
- Elementary partial and dbar calculations Example
- Positive-degree Dolbeault cohomology vanishes on polydiscs Theorem
- The Bochner–Martinelli formula for C1 functions Theorem
- The local Dolbeault lemma on nested polydiscs Theorem
Dependency tree · two levels
14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Lebl, Tasty Bits of Several Complex Variables, v4.4, Chapter 4 §4.4 (standard reference, not scraped)
- Jabbari, Notes for Analysis and Geometry of Several Complex Variables, §3.2 (standard reference, not scraped)
- Guillemin and Campbell, MIT 18.117 Lecture Notes, Lectures 1–4 (standard reference, not scraped)