Alphabeta MathHow 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.
Related vector fields have related Lie brackets
Statement
If smooth vector fields X1,X2 on M are respectively F-related to smooth vector fields Y1,Y2 on N, then [X1,X2] is F-related to [Y1,Y2].
Facts & Assumptions
Given: A smooth map F:M→N, vector fields X1,X2 on M, and vector fields Y1,Y2 on N with each Xi F-related to Yi.
F-relatedness is equivalent to the intertwining identity on smooth functions (F-relatedness is equivalent to the derivation intertwining law).
The commutator of smooth vector fields is again a smooth vector field (Smooth vector fields form a Lie algebra under the Lie bracket).
Proof
For every f∈C∞(N), [L1] gives X2(f∘F)=(Y2f)∘FandX1(f∘F)=(Y1f)∘F.
Apply X1 to the first identity and X2 to the second. Using [L1] again on the resulting target functions yields X1X2(f∘F)=(Y1Y2f)∘F,X2X1(f∘F)=(Y2Y1f)∘F.
Subtracting the identities in step 2.1 gives [X1,X2](f∘F)=([Y1,Y2]f)∘F for every smooth f on N. By [L2] both brackets are smooth vector fields, and [L1] identifies this identity as their F-relatedness.
Therefore related vector fields have related Lie brackets.