DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14

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.

Chevalley–Eilenberg differential

Definition

For $f \in C^{n} (g, M)$ define $d f \in C^{n + 1} (g, M)$ by

$\begin{aligned} (d f) (x_{0}, \dots, x_{n}) = & \sum_{i = 0}^{n} (- 1)^{i} x_{i} f (x_{0}, \dots, \hat{x_{i}}, \dots, x_{n}) \\ + \sum_{0 \leq i < j \leq n} (- 1)^{i + j} f ([x_{i}, x_{j}], x_{0}, \dots, \hat{x_{i}}, \dots, \hat{x_{j}}, \dots, x_{n}) . \end{aligned}$

This fixes a zero-based sign convention. A hat means omission, and in the second sum the bracket is inserted as the first argument. Empty sums are zero. Thus for $m \in C^{0} = M$ , $(d m) (x) = x m$ . Alternation of the formula makes it factor through $Λ^{n + 1} g$ ; the next theorem proves that successive differentials compose to zero.

Chevalley–Eilenberg differential

Definition

Depends on

Dependency tree · 2 levels

Sources