LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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.

Invariant polynomials cancel connection commutators

Statement

Let $M$ be a finite-dimensional Hausdorff second-countable smooth manifold, possibly with boundary. Let $G$ be a real or complex matrix Lie group with Lie algebra $g$ , and let $P_{k} : g^{k} \to K$ be the symmetric multilinear polarization of a homogeneous $G$ -invariant polynomial, where $K = R$ or $C$ . Work in a supplied $G$ -frame chart with a connection compatible with that reduction, so its local connection form $ω$ is $g$ -valued. For each homogeneous $g$ -valued form $A_{j} \in Ω^{q_{j}} (U; g)$ , extend $P_{k}$ by applying it to the Lie-algebra coefficients and wedging the scalar-form coefficients in the displayed argument order. Define $D^{\nabla} A = d A + ω \land A - (- 1)^{q} A \land ω (A \in Ω^{q} (U; g)) .$ Then $d P_{k} (A_{1}, \dots, A_{k}) = \sum_{j = 1}^{k} (- 1)^{q_{1} + \dots + q_{j - 1}} P_{k} (A_{1}, \dots, D^{\nabla} A_{j}, \dots, A_{k}) .$ In particular, the signed sum of the graded connection-commutator terms is zero. For $k = 0$ , the assertion is $d P_{0} = 0$ . The identity is local and hence also holds in boundary charts by restriction of the same coefficient calculation.

Facts & Assumptions

Given: A smooth $G$ -frame chart, a compatible connection, the invariant polarization $P_{k}$ , and homogeneous $g$ -valued forms $A_{j}$ with degrees $q_{j} \geq 0$ .

[F1]

A compatible connection has a $g$ -valued local connection form, and invariant-polynomial evaluation uses the listed-order wedge extension (Evaluation of an invariant polynomial on curvature).

[F2]

The polarization is symmetric and satisfies $\sum_{j = 1}^{k} P_{k} (Y_{1}, \dots, [X, Y_{j}], \dots, Y_{k}) = 0 (X, Y_{j} \in g)$ (Invariant symmetric polynomials on a matrix Lie algebra).

[F3]

The covariant exterior derivative of an $End (E)$ -valued form is defined by alternating the induced covariant derivative (Second Bianchi identity for a bundle connection).

[F4]

The induced Hom connection satisfies $(\nabla_{X} A) (s) = \nabla_{X} (A (s)) - A (\nabla_{X} s)$ (Product connection on tensor and hom bundles).

[F5]

Exterior differentiation obeys the degree-one graded Leibniz rule (The exterior derivative is a graded derivation).

[F6]

On boundary charts, the exterior derivative is defined by locally extendible half-space coefficients, independently of the extension, and the graded Leibniz rule restricts to the boundary (The de Rham complex and pullback extend to manifolds with boundary).

Proof

Proof technique: expand the scalar-form extension of $P_{k}$ in one local frame and use infinitesimal invariance coefficient by coefficient.

1.1F1F5algebra

In a fixed basis write $A_{j} = \sum_{μ} α_{j μ} Y_{j μ}$ and extend $P_{k}$ by $P_{k} (A_{1}, \dots, A_{k}) = \sum_{μ_{1}, \dots, μ_{k}} P_{k} (Y_{1 μ_{1}}, \dots, Y_{k μ_{k}}) α_{1 μ_{1}} \land \dots \land α_{k μ_{k}}$ ; this finite tensor contraction is basis independent. Put $Q_{j - 1} = q_{1} + \dots + q_{j - 1}$ . The graded Leibniz rule [F5] gives $d P_{k} (A_{1}, \dots, A_{k}) = \sum_{j = 1}^{k} (- 1)^{Q_{j - 1}} P_{k} (A_{1}, \dots, d A_{j}, \dots, A_{k})$ .

2.1F1F3F4step 1.1algebra

The covariant exterior derivative is the alternation of the induced End $(E)$ connection by [F3]. From [F4], in this frame $\nabla_{X}^{End} B = X (B) + ω (X) B - B ω (X)$ , so alternation yields $D^{\nabla} A_{j} = d A_{j} + [ω, A_{j}]_{g r}$ , where $[ω, A_{j}]_{g r} = ω \land A_{j} - (- 1)^{q_{j}} A_{j} \land ω$ . Since $ω$ and $A_{j}$ are $g$ -valued and $g$ is closed under brackets, $D^{\nabla} A_{j}$ is $g$ -valued. Substituting $d A_{j} = D^{\nabla} A_{j} - [ω, A_{j}]_{g r}$ into step 1.1 reduces the claim to $C = \sum_{j = 1}^{k} (- 1)^{Q_{j - 1}} P_{k} (A_{1}, \dots, [ω, A_{j}]_{g r}, \dots, A_{k}) = 0$ .

3.1F2F6step 1.1step 2.1algebra

Write $ω$ as a sum of scalar 1-forms times Lie-algebra elements and each $A_{j}$ as a sum of scalar $q_{j}$ -forms times Lie-algebra elements; locally each scalar form is a sum of coefficient functions times coordinate wedges. Fix one resulting coefficient monomial. In the $j$ th graded commutator, reordering the scalar $q_{j}$ -form $α_{j} \land θ$ to $θ \land α_{j}$ contributes $(- 1)^{q_{j}}$ , canceling its commutator factor and leaving $[X, Y_{j}]$ . Moving $θ$ past the earlier scalar forms contributes $(- 1)^{Q_{j - 1}}$ , canceling the prefactor in $C$ . The common ordered coefficient is therefore $\sum_{j = 1}^{k} P_{k} (Y_{1}, \dots, [X, Y_{j}], \dots, Y_{k}) = 0$ by [F2], so every coefficient of $C$ vanishes. The same calculation holds in boundary charts by [F6]. For $k = 0$ the form is the constant $P_{0}$ and its derivative is zero; no simultaneous choice is made. $□$

Depends on

Used by

Dependency tree · two levels

25 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

John Milnor and James Stasheff, Characteristic Classes (standard reference, not scraped)
Stefan Haller, The Atiyah–Singer Index Theorem, Vienna lecture notes (2013) (standard reference, not scraped)