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 geometric Dirac operator is globally well defined and formally symmetric
Statement
Assume Countable Choice. For a supplied graded Hermitian Clifford module and compatible connection as in Graded Hermitian Clifford modules and geometric Dirac operators, the local expression is independent of oriented orthonormal frame, is a smooth globally defined first-order differential operator, and is formally symmetric on a closed .
Facts & Assumptions
Given: Countable Choice, a smooth oriented Riemannian manifold, a graded Hermitian Clifford module , and a supplied graded Hermitian Clifford connection .
The Clifford relation, odd action and skew-Hermitian condition are exactly those in Graded Hermitian Clifford modules and geometric Dirac operators.
A Clifford connection obeys (Graded Hermitian Clifford modules and geometric Dirac operators, Complex-linear and metric-compatible bundle connections).
On a closed Riemannian manifold of dimension , the integral of the divergence of a smooth vector field is zero under countable choice (Riemannian divergence theorem).
This proof uses only through [F3]; it is declared in The Axiom of Countable Choice ().
Proof
Given: The stated module, connection and closed manifold.
On an overlap let be a change of oriented orthonormal frame, so is orthogonal. The dual coframe changes by the same orthogonal coefficient matrix with the corresponding inverse convention, while . Therefore by . Each chart expression has smooth coefficients, and these overlap equalities glue them to one global first-order operator.
If , the defining sum for is empty, so is formally symmetric. Now suppose . Define the complex vector field for smooth sections . At any chosen point take a local orthonormal frame with there. Using [F2], metric compatibility and at that point gives : the second term has this sign because and the Hermitian pairing is linear in its first variable. Since this is a pointwise identity independent of the chosen normal frame, it holds globally. Apply [F3] to real and imaginary parts of and integrate to get . Thus is formally symmetric. Oddness follows termwise because each is odd and preserves grading.
Depends on
- Graded Hermitian Clifford modules and geometric Dirac operators
- Universal Clifford algebra of a quadratic space
- Oriented real bundles and oriented frame bundles
- Complex-linear and metric-compatible bundle connections
- Fundamental theorem of riemannian geometry
- Riemannian divergence theorem
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
- Lichnerowicz formula for a geometric Dirac operator Lemma
- Spinor and geometric Clifford bundles and connections are well defined Lemma
- The maximal distributional domain of a geometric Dirac operator is H1 Lemma
- Atiyah–Singer index formula for a closed even-dimensional geometric Clifford module Theorem
Cited to discharge well-definedness by Graded Hermitian Clifford modules and geometric Dirac operators.
Dependency tree · two levels
34 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
- Liviu I. Nicolaescu, Notes on the Atiyah–Singer Index Theorem, revision 15 November 2013 (standard reference, not scraped)
- Konstantin Wernli, Lecture Notes on Spin Geometry (2019) (standard reference, not scraped)