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.
Derivation of an algebra
Definition
Let be a homomorphism of commutative rings (Commutative ring), so that is an -algebra, and let be a -module (Unital left and right modules over a ring; unqualified module means left module). An -derivation of into is a map satisfying, for all and all , the three laws
The first law says that is additive; the second that is -constant (it kills the image of ); the third is the Leibniz rule. The set of all such maps is written . It is a -module under the pointwise operations and : the sum and scalar multiples are again additive -constant maps satisfying Leibniz, because each law is linear in , and the zero map is a derivation.
Three conventions are part of the definition.
- No finiteness. Nothing is assumed about as an -algebra: it need not be finitely generated, finitely presented, or flat, and need not be Noetherian. The definitions used later on this page are the same ones used for the earlier algebraic-differentials interface of this track.
- -linearity, not -linearity. Every -derivation is -linear in the sense that for , : by Leibniz, and the second term vanishes. A derivation is in general not -linear, and this failure is exactly what the Leibniz rule measures; it also shows , since makes -constant.
- Functored variables. For a fixed ring map and a -linear map of -modules, composition is a -module map . Consequently is a functor from -modules to -modules, and the Leibniz rule is preserved by postcomposition with any module map.